simpa

Summary

If you have a goal and a hypothesis h, and 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 tactic
import data.real.basic

example (x y z : ℝ) (h : x = y + z + 0) : x * 1 = y + z :=
begin
  -- Lean's simplifier knows that a + 0 = 0 and a * 1 = a
  simpa using h,
end

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.

2. Like with simp, you can also feed simpa a list of extra lemmas for the simplifier to use. For example here simpa using h won’t work because the simplifier doesn’t know hxy (the simplifier doesn’t use hypotheses in the tactic state).

import tactic

example (x y z : ℕ) (hxy : x = y) (h : z = y + 0) : z = x * 1 :=
begin
  simpa [hxy] using h,
end

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.