have lLeU : l ≤ u := LE.le.trans lLeT tLeU
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
⊢ t.exp ≤ secant
case intro
d : ℕ
l u t : ℝ
p : ℝ → ℝ := taylorWithinEval Real.exp d (Set.Ioo l u) 0
secant : ℝ := (p l - p u) / (l - u) * (t - l) + p l
p_conv : StrictConvexOn ℝ (Set.Icc l u) p
t_neg : t < 0
l_bound : t > l
u_bound : t < u
lLeT : l ≤ t
tLeU : t ≤ u
lLeU : l ≤ u
⊢ t.exp ≤ secant