exact (Lean)

Definition

exact ( Lean)

The tactic exact t closes the current goal by supplying a proof term . Lean checks that the term’s type matches the goal, allowing definitional equality and inferred implicit arguments. Unlike apply, it does not leave premises as new goals.

Example

Supplying an existing proof

example (A : Prop) (h : A) : A := by
  exact h
 
example (A B : Prop) (h : A → B) (ha : A) : B := by
  exact h ha

The first proof supplies the assumption h. In the second, applying the proof h : A → B to ha : A produces a proof h ha : B, which closes the goal directly.