Theorem: strictConvexOn_cos_Icc (Carleson/Theorem1_1/Basic.lean)

State before:
⊢ StrictConvexOn ℝ (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2)) Real.cos
Tactic:
apply strictConvexOn_of_deriv2_pos (convex_Icc _ _) Real.continuousOn_cos fun x hx => ?_
State after:
x : ℝ
hx : x ∈ interior (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2))
⊢ 0 < deriv^[2] Real.cos x

State before:
x : ℝ
hx : x ∈ interior (Set.Icc (Real.pi / 2) (Real.pi + Real.pi / 2))
⊢ 0 < deriv^[2] Real.cos x
Tactic:
rw [interior_Icc] at hx
State after:
x : ℝ
hx : x ∈ Set.Ioo (Real.pi / 2) (Real.pi + Real.pi / 2)
⊢ 0 < deriv^[2] Real.cos x

State before:
x : ℝ
hx : x ∈ Set.Ioo (Real.pi / 2) (Real.pi + Real.pi / 2)
⊢ 0 < deriv^[2] Real.cos x
Tactic:
simp [Real.cos_neg_of_pi_div_two_lt_of_lt hx.1 hx.2]
State after:
no goals