let a := b ^ b
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)
case pos
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ a b, Irrational a ∧ Irrational b ∧ ¬Irrational (a ^ b)