have h4 : Real.tan (Real.pi / 4) = y' (Real.pi / 2) := by
  dsimp only [y']
  rw [Real.tan_pi_div_two_sub, Real.tan_pi_div_four, one_eq_inv]
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
⊢ (x - Real.pi / 4).tan < 1
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
⊢ (x - Real.pi / 4).tan < 1