Reflexivity of equality

Stream: new members

[Filippo A. E. Nuccio]

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]

Use $$ maths $$

[Johan Commelin]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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

[Johan Commelin]

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

[Filippo A. E. Nuccio]

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

[Johan Commelin]

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

[Kevin Buzzard]

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.