Cannot convert this Lean 3 lemma to Lean 4

Stream: new members

[ElCondor]

Hi everybody!

I recently learnt Lean and started with a simple theorem theorem existence_theorem: ∃ x y : ℝ, (irrational x) ∧ (irrational y) ∧ ¬(irrational (x^y)).

Here it is implemented in Lean 3.

Now I'm trying to convert it to Lean 4 and I'm stuck with the simple lemma ((sqrt 2)^(sqrt 2))^(sqrt 2) = 2 (see there), whereas I would expect this lemma to be trivial.

It looks like I have to prove 0 ≤ 2 which I expected simp would solve but it doesn't.

Questions:

• Why can't I proceed just like in Lean 3?
• How would you write it?

Thanks

[Kevin Buzzard]

norm_num is the tactic whose job it is to prove equalities and inequalities between numerals. simp is a tactic which rewrites equalities. simp doesn't mean "prove anything simple"

[ElCondor]

Thanks Kevin, I was able to solve it (see here).

I know it's WIP, but it's a bit hard to find the right tactic in the doc right now (I looked at https://lean-lang.org/theorem_proving_in_lean4/tactics.html?search=norm_num)

[Kevin Buzzard]

Yeah I don't know the solution to "look up which tactic is the right one for this goal". In the end I just learnt what all the big tactics did.