hard time with simple equality

Stream: general

[Bernd Losert]

example (n₁ n₂ : ℕ) : ℕ :=
begin
  let n := n₁ + n₂,
  have hn : n + 2 = n₁ + 1 + (n₂ + 1) := sorry,
  exact 0
end

I can't figure out how to prove hn. I've tried some combinations of rw and simp but I can't seem to get to to work. I think the problem is that my simp and rw are only acting on the lhs. I've tried using calc, but I also get stuck.

[Eric Wieser]

docs#add_add_add_comm

[Eric Wieser]

Rewriting by that will get you to the point where it's easy

[Bernd Losert]

Ah, that's handy.

[Bernd Losert]

Thanks.

[Bernd Losert]

How do you deal with something more complex like say n + 10 = n1 + 1 + (n2 + 2) + ... + (n10 + 1)?

[Patrick Johnson]

Try tactic#omega

[Bernd Losert]

If I just say by omega nat, it doesn't work in the n + 2 case.

[Riccardo Brasca]

omega should be avoided, it is super slow and it won't be ported to Lean 4.

[Patrick Johnson]

linarith also works:

import tactic

example {m n : ℕ} : m + n + 2 = m + 1 + (n + 1) := by linarith

[Anne Baanen]

This is precisely the kind of problem that tactic#ring is made for. I believe linarith solves this goal because it preprocesses using ring. Maybe also tactic#abel will work, depending on how well it knows that 2 = 1 + 1.