test_irr_powers

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Data.Set.Basic
def Irrational (x : ℝ) : Prop := x ∉ Set.range ((↑) : ℚ → ℝ)

theorem test_irr_powers : ∃ a b : ℝ, Irrational a ∧ Irrational b ∧ ¬ Irrational (a ^ b) := by sorry