apply h6
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))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ (x - Real.pi / 4).tan < y' (Real.pi / 2)
case x
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))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ x ∈ Set.Icc 0 (Real.pi / 2)

case x
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))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ Real.pi / 2 ∈ Set.Icc 0 (Real.pi / 2)

case a
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))
h6 : StrictMonoOn y' (Set.Icc 0 (Real.pi / 2))
⊢ x < Real.pi / 2