## Stream: new members

### Topic: It's just add and sub?

#### Anders Larsson (Jan 02 2022 at 12:04):

Hi,
I'm a software guy trying to learn Lean.

I think I have missed something obvious here. I would expect simp or some similar command do be able to
fix the example below or fail and prove that the equality is incorrect. What is a reasonable path forward?
(What tutorial to read? How to reason with big but seemingly obvious reshuffle of add/sub?).

import data.complex.basic

example (a b c : ℂ) :  a.re * b.im - c.re * b.im + (c.im * b.re - a.im * b.re) =
a.re * b.im + -(a.im * b.re) - (c.re * b.im + -(c.im * b.re)) :=
begin
sorry
end


#### Patrick Johnson (Jan 02 2022 at 12:07):

docs#tactic.linarith

example (a b c : ℂ) :
a.re * b.im - c.re * b.im + (c.im * b.re - a.im * b.re) =
a.re * b.im + -(a.im * b.re) - (c.re * b.im + -(c.im * b.re)) :=
begin
linarith,
end


#### Anders Larsson (Jan 02 2022 at 12:10):

Patrick Johnson said:

Awesome! I had only seen linarith in the context of inequalities so far.

#### Alex J. Best (Jan 02 2022 at 12:56):

tactic#ring and tactic#abel can also both prove this. Fun fact: linarith indeed does "only" do inequalities and proves this goal by showing both the the left hand side is \le the right hand side, and vice-versa.

#### Alex J. Best (Jan 02 2022 at 13:02):

tactic#abel is probably the right answer to the question of how to deal with a seemingly obvious reshuffle of add and sub, indeed abel can prove this when we set up a similar goal over an arbitrary ring, not just the reals/complexes:

example {C : Type*} [ring C] (a_re b_re c_re a_im b_im c_im : C) :
a_re * b_im - c_re * b_im + (c_im * b_re - a_im * b_re) =
a_re * b_im + -(a_im * b_re) - (c_re * b_im + -(c_im * b_re)) :=
begin
abel,
end


The other two mentioned tactics don't manage this one, as linarith wants an ordering on the ring, and ring likes rings to be commutative.

#### Kevin Buzzard (Jan 02 2022 at 13:08):

I don't know what you're interested in but maybe this https://github.com/ImperialCollegeLondon/complex-number-game might show you some techniques?

#### Anders Larsson (Jan 02 2022 at 14:58):

Kevin Buzzard said:

I don't know what you're interested in but maybe this https://github.com/ImperialCollegeLondon/complex-number-game might show you some techniques?

Sure, i found it some days ago. I'm working on level 03 now.

#### Kyle Miller (Jan 02 2022 at 15:13):

@Anders Larsson simp can do this if you give it enough lemmas:

example (a b c : ℂ) :  a.re * b.im - c.re * b.im + (c.im * b.re - a.im * b.re) =
a.re * b.im + -(a.im * b.re) - (c.re * b.im + -(c.im * b.re)) :=

Even though repeat { rw mul_comm } would run forever, simp is smarter and chooses some sort of normal form.