constructor
case intro.intro.refine_1
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)
⊢ (Differentiable ℝ fun t => f a + ∫ (u : ℝ) in a..t, gg u) ∧
    ContDiff ℝ (↑n) (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u)
case intro.intro.refine_1.left
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)
⊢ Differentiable ℝ fun t => f a + ∫ (u : ℝ) in a..t, gg u

case intro.intro.refine_1.right
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)
⊢ ContDiff ℝ (↑n) (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u)