test_irr_inline

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

theorem test_irr_inline : Irrational (Real.sqrt 2) := by sorry