constructor
case intro
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
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ y1 a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
case intro.left
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
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ -Real.pi / 4 ≤ y1 a

case intro.right
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
h5 : StrictMonoOn y1 (Set.Icc 0 (Real.pi / 2))
a : ℝ
ha1 : 0 ≤ a
ha2 : a ≤ Real.pi / 2
⊢ y1 a ≤ Real.pi / 4