apply (Lean)

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 .

Example

Reducing a conclusion to a premise

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

apply h changes the goal from B to A. The tactic exact supplies its proof ha.