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