## Stream: general

### Topic: hard time with simple equality

#### Bernd Losert (Jul 15 2022 at 16:27):

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 (Jul 15 2022 at 16:28):

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

#### Bernd Losert (Jul 15 2022 at 16:29):

Ah, that's handy.

Thanks.

#### Bernd Losert (Jul 15 2022 at 16:31):

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

Try tactic#omega

#### Bernd Losert (Jul 15 2022 at 16:34):

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

#### Riccardo Brasca (Jul 15 2022 at 16:35):

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

#### Patrick Johnson (Jul 15 2022 at 16:36):

linarith also works:

import tactic

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

#### Anne Baanen (Jul 15 2022 at 16:39):

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.

Last updated: Aug 03 2023 at 10:10 UTC