Square_Root_of_2_is_Irrational

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

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