# How to write this non-constructive proof in Lean?

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...
• First of all I strongly suggest you to move to Lean4 (for this kind of question the answer is essentially the same, and Lean3 is end of life). The ^ is just notation introduced somewhere, try to import a less basic file and you should get it. Concerning the real question, have you read TPIL or any other basic reference? Sep 24, 2023 at 10:57
• @Ricky the default online interpreter on Lean's website is running on Lean 3. Do they also provide one on Lean 4? Sep 24, 2023 at 11:27
• Here
– Trebor
Sep 24, 2023 at 11:58
• A fine exercise in Lean, but a poor demonstration of excluded middle: $(\sqrt{2})^{\log_2 9} = \sqrt{2^{\log_2 9}} = \sqrt{9} = 3$. Sep 24, 2023 at 13:14
• Just use pow_mul and pow_two, (both backwards), then simp can probably do it. I don't see why simp should do it automatically, it's easy, but there is no reason to have pow_two as a simp lemma. Sep 24, 2023 at 18:29

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