linarith [ht.1]
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
hh : t < u ∧ u ≤ a
⊢ u ∈ Ι a b \ {a, b}
no goals