Theorem: toto (extend.lean)

State before:
f : ℝ → ℝ
a b : ℝ
hab : a < b
n : ℕ
h : ContDiffOn ℝ (↑n) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑n) g ∧ EqOn g f (Icc a b)
Tactic:
induction n generalizing f
State after:
case zero
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContDiffOn ℝ (↑Nat.zero) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑Nat.zero) g ∧ EqOn g f (Icc a b)

case succ
a b : ℝ
hab : a < b
n✝ : ℕ
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)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n✝)) g ∧ EqOn g f (Icc a b)

State before:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContDiffOn ℝ (↑Nat.zero) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑Nat.zero) g ∧ EqOn g f (Icc a b)
Tactic:
case zero =>
simp only [CharP.cast_eq_zero, contDiff_zero, contDiffOn_zero] at h ⊢
refine ⟨IccExtend hab.le (restrict (Icc a b) f), h.restrict.Icc_extend', ?_⟩
exact λ t ht => IccExtend_of_mem _ _ ht
State after:
no goals

State before:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContDiffOn ℝ (↑Nat.zero) f (Icc a b)
⊢ ∃ g, ContDiff ℝ (↑Nat.zero) g ∧ EqOn g f (Icc a b)
Tactic:
simp only [CharP.cast_eq_zero, contDiff_zero, contDiffOn_zero] at h ⊢
State after:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContinuousOn f (Icc a b)
⊢ ∃ g, Continuous g ∧ EqOn g f (Icc a b)

State before:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContinuousOn f (Icc a b)
⊢ ∃ g, Continuous g ∧ EqOn g f (Icc a b)
Tactic:
refine ⟨IccExtend hab.le (restrict (Icc a b) f), h.restrict.Icc_extend', ?_⟩
State after:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContinuousOn f (Icc a b)
⊢ EqOn (IccExtend ⋯ (restrict (Icc a b) f)) f (Icc a b)

State before:
a b : ℝ
hab : a < b
f : ℝ → ℝ
h : ContinuousOn f (Icc a b)
⊢ EqOn (IccExtend ⋯ (restrict (Icc a b) f)) f (Icc a b)
Tactic:
exact λ t ht => IccExtend_of_mem _ _ ht
State after:
no goals

State before:
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)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)
Tactic:
have h1 : ContDiffOn ℝ n (derivWithin f (Icc a b)) (Icc a b) :=
  h.derivWithin (uniqueDiffOn_Icc hab) le_rfl
State after:
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)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)

State before:
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)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)
Tactic:
obtain ⟨gg, h2, h3⟩ := ih h1
State after:
case intro.intro
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)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)

State before:
case intro.intro
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)
⊢ ∃ g, ContDiff ℝ (↑(Nat.succ n)) g ∧ EqOn g f (Icc a b)
Tactic:
refine ⟨λ t => f a + ∫ u in a..t, gg u, ?_, ?_⟩
State after:
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)
⊢ ContDiff ℝ ↑(Nat.succ n) fun t => f a + ∫ (u : ℝ) in a..t, gg u

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)
⊢ EqOn (fun t => f a + ∫ (u : ℝ) in a..t, gg u) f (Icc a b)

State before:
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)
⊢ ContDiff ℝ ↑(Nat.succ n) fun t => f a + ∫ (u : ℝ) in a..t, gg u
Tactic:
rw [contDiff_succ_iff_deriv]
State after:
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)

State before:
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)
Tactic:
constructor
State after:
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)

State before:
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
Tactic:
refine differentiableOn_univ.1 ((differentiableOn_integral_of_continuous ?_ h2.continuous).const_add _)
State after:
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)
⊢ ∀ x ∈ univ, IntervalIntegrable gg MeasureTheory.volume a x

State before:
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)
⊢ ∀ x ∈ univ, IntervalIntegrable gg MeasureTheory.volume a x
Tactic:
simp [h2.continuous.intervalIntegrable]
State after:
no goals

State before:
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)
Tactic:
convert h2
State after:
case h.e'_10
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)
⊢ (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u) = gg

State before:
case h.e'_10
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)
⊢ (deriv fun t => f a + ∫ (u : ℝ) in a..t, gg u) = gg
Tactic:
ext t
State after:
case h.e'_10.h
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 : ℝ
⊢ deriv (fun t => f a + ∫ (u : ℝ) in a..t, gg u) t = gg t

State before:
case h.e'_10.h
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 : ℝ
⊢ deriv (fun t => f a + ∫ (u : ℝ) in a..t, gg u) t = gg t
Tactic:
simp [deriv_const_add, h2.continuous.deriv_integral]
State after:
no goals

State before:
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)
⊢ EqOn (fun t => f a + ∫ (u : ℝ) in a..t, gg u) f (Icc a b)
Tactic:
intro t ht
State after:
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
⊢ (fun t => f a + ∫ (u : ℝ) in a..t, gg u) t = f t

State before:
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
⊢ (fun t => f a + ∫ (u : ℝ) in a..t, gg u) t = f t
Tactic:
dsimp
State after:
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
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t

State before:
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
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Tactic:
have l6 : Icc a t ⊆ Icc a b := Icc_subset_Icc_right ht.2
State after:
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
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t

State before:
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
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Tactic:
have l9 : EqOn gg (derivWithin f (Icc a b)) (uIcc a t) := h3.mono (by simp [uIcc, ht.1, l6])
State after:
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)
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t

State before:
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)
⊢ f a + ∫ (u : ℝ) in a..t, gg u = f t
Tactic:
have l10 := h.one_of_succ.integral_eq_sub'' hab.le ht
State after:
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

State before:
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
Tactic:
simp [integral_congr l9, l10]
State after:
no goals

State before:
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
⊢ uIcc a t ⊆ Icc a b
Tactic:
simp [uIcc, ht.1, l6]
State after:
no goals