simp (Lean)

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.

Example

Simplifying a goal or an assumption

example (n : ℕ) : n + 0 = n := by
  simp
 
example (n : ℕ) (h : n + 0 = 3) : n = 3 := by
  simp at h
  exact h

In the second proof, simp at h changes h to n = 3. The tactic exact then closes the goal using that assumption.