I am experimenting with my own "natural numbers" (Peano), so I don't want to use Lean 4's natural number tactics (such as add_comm or cancellation). How can the following be proved? It should have an obvious proof (using only logic and equality), but I have not found relevant examples - a Cheatsheet does indicate "apply" or "specialize".

example (a b c x y : Peano) (h1: a = b → a + c = c + b) (h2: x = y) : x + c = c + y := by sorry
  • $\begingroup$ I’m glad you found an answer. Please use backticks for code in the future. It makes it easier for everyone to read. $\endgroup$
    – Jason Rute
    Dec 28, 2023 at 19:25
  • $\begingroup$ Also please include all relevant background definitions or imports. I guess in this particular case it doesn’t matter what Peano is, but that isn’t always clear. Also the way most people help is by copy and pasting your code into Lean, so it is important to provide a complete “minimal working example”. $\endgroup$
    – Jason Rute
    Dec 28, 2023 at 19:28
  • $\begingroup$ Thanks for your suggestions. I will try to use MWE when appropriate. $\endgroup$ Jan 3 at 23:18

1 Answer 1


After realizing that h1 needs to be quantified, I found a proof:

example (x y z : Peano) (h1: ∀ a b c:Peano, a = b → a + c = c + b) (h2: x = y) : x + z = z + y := by 
  apply h1
  apply h2

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.