simpa
Summary
If you have a goal and a hypothesis h
, and if Lean’s simplifier simp
, if run on both of them, will turn them into the same thing, then you could solve the goal in three lines with simp
, simp at h
, exact h
, or even in two lines with simp at *
, exact h
. But you could also solve it in one line with simpa using h
. In fact h
doesn’t need to be a hypothesis, it can be any proof you like (e.g. a proof you made using some lemmas and some hypotheses).
Examples
import Mathlib.Tactic
example (x y z : ℝ) (h : x = y + z + 0) : x * 1 = y + z := by
-- Lean's simplifier knows that a + 0 = 0 and a * 1 = a
simpa using h
Here the simplifier can do some work on both the hypothesis h
(removing the + 0
) and on the goal (removing * 1
). Once this work is done, h
and the goal become equal.
Like with
simp
, you can also feedsimpa
a list of extra lemmas for the simplifier to use. For the example belowsimpa using h
won’t work because the simplifier doesn’t knowhxy
(the simplifier doesn’t use hypotheses in the tactic state).
import Mathlib.Tactic
example (x y z : ℕ) (hxy : x = y) (h : z = y + 0) : z = x * 1 := by
simpa [hxy] using h
Further notes
Easter egg: If your hypothesis is called this
then you don’t have to write using this
at all, you can just write simpa
.