## Stream: new members

### Topic: Reflexivity of equality

#### Filippo A. E. Nuccio (May 28 2020 at 12:09):

Playing with the complex number game (and having admittedly given a glance at Kevin Buzzard's solutions) I was trying to prove something to the effect that (x y : $\mathbb{R}$) :x*x+y*y > 0. Kevin has proven that (x y : R ) :x*x+y*y = 0 <-> x=0 and y=0 so I was happily using that (x y : R ) : x=0 and y=0 -> 0=x*x+y*y, but then Lean was not happy at all. It became happy again when I insisted that (x y : R ) : x=0 and y=0 -> x*x+y*y = 0  and then I fell in despair as I realised that even cc cannot convert a=b  into b=a. Is this true, that there is no hope?

Side question: how to type in LaTeX in Zulip?

#### Johan Commelin (May 28 2020 at 12:10):

Use $maths$

#### Johan Commelin (May 28 2020 at 12:11):

if h : a = b, then h.symm : b = a

#### Johan Commelin (May 28 2020 at 12:12):

Also rw [eq_comm] can be used to swap sides of an equality

#### Filippo A. E. Nuccio (May 28 2020 at 12:12):

Ah, ok; but can't cc do it on its own?

#### Johan Commelin (May 28 2020 at 12:12):

I would expect that it does... but I don't use it that much.

#### Filippo A. E. Nuccio (May 28 2020 at 12:12):

hmm... good sign I should not use it either.

#### Johan Commelin (May 28 2020 at 12:18):

Anyway, to prove x * x + y * y > 0 you need lemmas like add_pos and sq_pos.

#### Kevin Buzzard (May 28 2020 at 14:08):

Today on Twitch I'll be running through some of the complex number game. I just completely re-ordered everything, so the map $\mathbb{R}\to\mathbb{C}$ is level 1, and $\sqrt{-1}$ is now level 2. But I will stop (just) before all this $x^2\geq0$ stuff because it doesn't look sexy proving this stuff by hand.

Last updated: May 18 2021 at 16:25 UTC