Tactic (Lean)

Definition

Tactic ( Lean)

A tactic is a command that constructs a proof by working on the current goals and their local context. In a by block, tactics may close a goal, transform it or reduce it to new goals; a completed proof leaves no goals unresolved.

Tactics

exact

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.

Link to original

apply

Definition

apply ( Lean)

The tactic apply t works backwards from the conclusion of a proof or theorem t. If its conclusion matches the current goal, Lean infers the required arguments where possible and creates goals for the remaining ones. For , applying t to a goal leaves the goal .

Link to original

funext

Definition

funext ( Lean)

The tactic funext x applies function extensionality: to prove two functions equal, it suffices to prove for every . It introduces an arbitrary input x and replaces the function-equality goal with equality of the outputs at x.

Link to original

unfold

Definition

unfold ( Lean)

The tactic unfold d expands occurrences of the definition d in the goal using its defining equations. It exposes what the definition means without performing the broader simplification of simp. Use unfold d at h to expand it in an assumption.

Link to original

simp

Definition

simp ( Lean)

The tactic simp simplifies a goal using registered simplification lemmas and built-in reductions. It closes the goal when the simplified proposition is immediately provable; otherwise, it leaves a simpler goal.

simp [d] additionally unfolds the definition d or uses the lemma d. simp at h simplifies the assumption h instead of the goal.

Link to original