simp [irrational_iff_ne_rational]
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ¬Irrational 2
case h
b : ℝ := Real.sqrt 2
c : Irrational (b ^ b)
a : ℝ := b ^ b
⊢ ∃ x x_1, 2 = ↑x / ↑x_1