simp [integral_congr l9, l10]
case intro.intro.refine_2
a b : ℝ
hab : a < b
n : ℕ
ih : ∀ {f : ℝ → ℝ}, ContDiffOn ℝ (↑n) f (Icc a b) → ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
f : ℝ → ℝ
h : ContDiffOn ℝ (↑(Nat.succ n)) f (Icc a b)
h1 : ContDiffOn ℝ (↑n) (derivWithin f (Icc a b)) (Icc a b)
gg : ℝ → ℝ
h2 : ContDiff ℝ (↑n) gg
h3 : EqOn gg (derivWithin f (Icc a b)) (Icc a b)
t : ℝ
ht : t ∈ Icc a b
l6 : Icc a t ⊆ Icc a b
l9 : EqOn gg (derivWithin f (Icc a b)) (uIcc a t)
l10 : ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = f t - f a
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
no goals