search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 47 forks source link

tactics.rst: fix example #91

Closed dharmatech closed 4 years ago

dharmatech commented 4 years ago

The example as shown in the book:

example {m n : ℕ} (h : n = 1) (h' : 0 = m) : (f m n) * m = m := by simp [h, h'.symm, f]

doesn't actually require all three items passed to simp. It only requires two:

example {m n : ℕ} (h : n = 1) (h' : 0 = m) : (f m n) * m = m := by simp [h, h'.symm]

These two work as well:

example {m n : ℕ} (h : n = 1) (h' : 0 = m) : (f m n) * m = m := by simp [f, h'.symm]

If we change the goal as follows, all three appear to be required:

example {m n : ℕ} (h : n = 1) (h' : 0 = m) : (f m n) = n := by simp [h, h'.symm, f]