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

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