funext (Lean)

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.

Example

Comparing functions pointwise

example : (fun n : ℕ => n + 0) = (fun n => n) := by
  funext n
  simp

funext n changes the goal to n + 0 = n for an arbitrary n : ℕ. The tactic simp proves that pointwise equality.