How to write this non-constructive proof in Lean?

Question

There is a theorem which says that there exists two irrationals $x, y$ such that $x^y$ is rational.

An interesting proof in classical logic is the following:

Consider $u = \sqrt{2}^{\sqrt{2}}$.
If $u$ is rational then we use $(x,y) = (\sqrt{2},\sqrt{2})$.
Otherwise, we notice that $u^\sqrt{2} = 2$ and use $(x,y) = (u,\sqrt{2})$.

I'd like to implement that proof in Lean (3) (the irrationality of $\sqrt{2}$ is already proven in mathlib).

I managed to write a signature of my theorem (execute):

import data.real.irrational
import analysis.special_functions.pow.real

open classical

theorem classical_logic_existence : ∃ x y : ℝ, irrational x ∧ irrational y ∧ ¬ (irrational (x.rpow y)) :=
sorry

My questions are:

• How can I use x^y instead of (x.rpow y)? (just replacing it produces an error)
• How would I implement my proof in Lean? I have no idea how to write the case disjunction and so on...

Answer 1

I eventually managed to write a proof (execute here).

What I was looking for was essentially the tactic by_cases for cases disjunction.

It is also longer than I expected because I couldn't fully automate proving things like ((sqrt 2)^(sqrt 2))^(sqrt 2) = 2 or ¬(irrational 2).

Note that, as pointed out in a comment, this proof is in Lean 3 and it is preferable to use Lean 4 as of today.

import data.real.irrational
import data.rat.sqrt
import analysis.special_functions.pow.real

open real

lemma simple_lemma: ((sqrt 2)^(sqrt 2))^(sqrt 2) = 2 :=
begin
  rw <-rpow_mul,
  rw <-pow_two,
  by simp,
  simp [sqrt_nonneg],
end

theorem existence_theorem:
  ∃ x y : ℝ, (irrational x) ∧ (irrational y) ∧ ¬(irrational (x^y)) :=
begin
  -- Technicality: we need to prove that 2 (as a real) is not irrational
  have not_irrat_2 : ¬(irrational 2),
  {
    convert rat.not_irrational 2,
    norm_cast,
  },
  by_cases h : irrational ((sqrt 2)^(sqrt 2)),
  -- h : irrational (sqrt 2 ^ sqrt 2)
  {
    existsi [(sqrt 2)^(sqrt 2), sqrt 2],
    simp [h, simple_lemma, irrational_sqrt_two, not_irrat_2],
  },
  -- h : ¬irrational (sqrt 2 ^ sqrt 2)
  {
    existsi [sqrt 2, sqrt 2],
    simp [h, irrational_sqrt_two],
  },
end