-- Library Import: Basic facts about real numbers and the root function
import Mathlib.Data.Real.Sqrt
open Real

-- In the following, x and y are real numbers
variable {x : ℝ} {y : ℝ}

-- Definition: Function (f : ℝ → ℝ) is continuous at (x₀ : ℝ)
def continuous (f : ℝ → ℝ) (x₀ : ℝ) :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| < δ → |f x - f x₀| < ε

-- Definition: The square function
def squareFct : ℝ → ℝ := fun x ↦ x ^ 2


-- Reminder: Three facts from the library that we will use.
example : 0 < x → 0 < √x := sqrt_pos.2

example : x ^ 2 < y  ↔  (-√y < x) ∧ (x < √y) := sq_lt

example : |x| < y  ↔  -y < x ∧ x < y := abs_lt


-- Theorem: The square function is continuous at x₀ = 0
theorem ContinuousAt_sq :
    continuous squareFct 0 := by

  unfold continuous

  intro ε hε
  use √ε

  constructor
  · apply sqrt_pos.2
    exact hε
  · intro x hx
    simp_all [squareFct]
    apply sq_lt.2
    exact abs_lt.1 hx