intro a _ b _ hab
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)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
⊢ StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
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)
y1 : ℝ → ℝ := fun x => x - Real.pi / 4
a : ℝ
x✝¹ : a ∈ Set.Icc 0 (Real.pi / 2)
b : ℝ
x✝ : b ∈ Set.Icc 0 (Real.pi / 2)
hab : a < b
⊢ y1 a < y1 b