awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
h : ∀ (a_1 : ℝ) (hy : a_1 ∈ Ioo a b), F a_1 = f a_1
⊢ F =ᶠ[𝓝 x] f

Tactic:
filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy

Premises used: Ioo_mem_nhds, And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
a_1 : ℝ
hy : a_1 ∈ Ioo a b
h : update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb a_1 = f a_1
⊢ F a_1 = f a_1

Tactic:
unfold F
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
a_1 : ℝ
hy : a_1 ∈ Ioo a b
h : update (β := fun (a : ℝ) ↦ E) f a fa a_1 = f a_1
h₁ h₂ : f a_1 = f a_1
⊢ update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb a_1 = f a_1

Tactic:
rw [update_of_ne hy.2.ne, update_of_ne hy.1.ne']

Premises used: LT.lt.ne', And.right, And.left, LT.lt.ne, Function.update_of_ne
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
⊢ ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x

Tactic:
have Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x := by
    refine fun x hx => (hderiv x hx).congr_of_eventuallyEq ?_
    filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy
    unfold F
    rw [update_of_ne hy.2.ne, update_of_ne hy.1.ne']
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
rw :
  (ContinuousOn f (Ioo a b) ∧ (a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa))) ∧
    (b ∈ Icc a b → Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb))
⊢ ContinuousOn F (Icc a b)

Tactic:
rw [continuousOn_update_iff, continuousOn_update_iff, Icc_diff_right, Ico_diff_left]

Premises used: continuousOn_update_iff, Set.Icc_diff_right, Set.Ico_diff_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ (ContinuousOn f (Ioo a b) ∧ (a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa))) ∧
    (b ∈ Icc a b → Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb))

Tactic:
⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, ?_⟩, ?_⟩

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
refine_1 : a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)
refine_2 : b ∈ Icc a b → Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb)
⊢ (ContinuousOn f (Ioo a b) ∧ (a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa))) ∧
    (b ∈ Icc a b → Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb))

Tactic:
refine ⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, ?_⟩, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)

Tactic:
fun _ => ha.mono_left (nhdsWithin_mono _ Ioo_subset_Ioi_self)

Premises used: Filter.Tendsto.mono_left, Set.Ioo_subset_Ioi_self, nhdsWithin_mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)

Tactic:
exact fun _ => ha.mono_left (nhdsWithin_mono _ Ioo_subset_Ioi_self)

Premises used: Filter.Tendsto.mono_left, Set.Ioo_subset_Ioi_self, nhdsWithin_mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb)

Tactic:
(hb.congr' ?_).mono_left (nhdsWithin_mono _ Ico_subset_Iio_self)

Premises used: Set.Ico_subset_Iio_self, Filter.Tendsto.mono_left, Filter.Tendsto.congr', nhdsWithin_mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
refine_2 : f =ᶠ[𝓝[<] b] update (β := fun (a : ℝ) ↦ E) f a fa
⊢ Tendsto (update (β := fun (a : ℝ) ↦ E) f a fa) (𝓝[Ico a b] b) (𝓝 fb)

Tactic:
refine (hb.congr' ?_).mono_left (nhdsWithin_mono _ Ico_subset_Iio_self)

Premises used: Set.Ico_subset_Iio_self, Filter.Tendsto.mono_left, Filter.Tendsto.congr', nhdsWithin_mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
a_1 : ℝ
hz : a_1 ∈ Ioo a b
⊢ f a_1 = update (β := fun (a : ℝ) ↦ E) f a fa a_1

Tactic:
(update_of_ne hz.1.ne' _ _).symm

Premises used: LT.lt.ne', And.left, Eq.symm, Function.update_of_ne
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
h :
  ∀ (a_1 : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        x ∈ Ioo a b →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ f x = update (β := fun (a : ℝ) ↦ E) f a fa x) x} x}
      a_1
h₁ h₂ : ∀ (a_1 : ℝ) (hz : a_1 ∈ Ioo a b), f a_1 = update (β := fun (a : ℝ) ↦ E) f a fa a_1
⊢ f =ᶠ[𝓝[<] b] update (β := fun (a : ℝ) ↦ E) f a fa

Tactic:
filter_upwards [Ioo_mem_nhdsLT hab] with _ hz using (update_of_ne hz.1.ne' _ _).symm

Premises used: Ioo_mem_nhdsLT
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
⊢ ContinuousOn F (Icc a b)

Tactic:
have hcont : ContinuousOn F (Icc a b) := by
    rw [continuousOn_update_iff, continuousOn_update_iff, Icc_diff_right, Ico_diff_left]
    refine ⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, ?_⟩, ?_⟩
    · exact fun _ => ha.mono_left (nhdsWithin_mono _ Ioo_subset_Ioi_self)
    · rintro -
      refine (hb.congr' ?_).mono_left (nhdsWithin_mono _ Ico_subset_Iio_self)
      filter_upwards [Ioo_mem_nhdsLT hab] with _ hz using (update_of_ne hz.1.ne' _ _).symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f f' : ℝ → E
hab : a < b
fa fb : E
hderiv : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[>] a) (𝓝 fa)
hb : Tendsto f (𝓝[<] b) (𝓝 fb)
F : ℝ → E := update (β := fun (a : ℝ) ↦ E) (update (β := fun (a : ℝ) ↦ E) f a fa) b fb
Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x
hcont : ContinuousOn F (Icc a b)
⊢ ∫ (y : ℝ) in a..b, f' y = fb - fa

Tactic:
simpa [F, hab.ne, hab.ne'] using integral_eq_sub_of_hasDerivAt_of_le hab.le hcont Fderiv hint

Premises used: LT.lt.le, LT.lt.ne', intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hderiv : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a

Tactic:
integral_eq_sub_of_hasDerivAt (fun x hx => (hderiv x hx).hasDerivAt) hint

Premises used: DifferentiableAt.hasDerivAt, intervalIntegral.integral_eq_sub_of_hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
rw : IntervalIntegrable (deriv f) volume a b
⊢ ∫ (y : ℝ) in a..b, f' y = f b - f a

Tactic:
rw [← hderiv, integral_deriv_eq_sub hdiff]

Premises used: intervalIntegral.integral_deriv_eq_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
rw : IntervalIntegrable f' volume a b
⊢ IntervalIntegrable (deriv f) volume a b

Tactic:
rw [hderiv]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable f' volume a b

Tactic:
hcont.intervalIntegrable

Premises used: ContinuousOn.intervalIntegrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f' f : ℝ → E
hderiv : deriv f = f'
hdiff : ∀ x ∈ [[a, b]], DifferentiableAt ℝ f x
hcont : ContinuousOn f' [[a, b]]
⊢ IntervalIntegrable f' volume a b

Tactic:
exact hcont.intervalIntegrable

Premises used: ContinuousOn.intervalIntegrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
inl : ∀ (hab : a ≤ b), ∫ (y : ℝ) in a..b, deriv f y = f b - f a
inr : ∀ (hab : b ≤ a), ∫ (y : ℝ) in a..b, deriv f y = f b - f a
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a

Tactic:
rcases le_total a b with hab | hab

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : a ≤ b
⊢ ContinuousOn f (Icc a b)

Tactic:
simp only [uIcc_of_le, hab, uIoo_of_le] at hcont hderiv

Premises used: Set.uIcc_of_le, Set.uIoo_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : a ≤ b
hcont₁ : ContinuousOn f (Icc a b)
⊢ ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x

Tactic:
simp only [uIcc_of_le, hab, uIoo_of_le] at hcont hderiv

Premises used: Set.uIcc_of_le, Set.uIoo_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : a ≤ b
hcont : ContinuousOn f (Icc a b)
hderiv : ∀ x ∈ Ioo a b, DifferentiableAt ℝ f x
inl inl₁ : f b - f a = f b - f a
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a

Tactic:
rw [integral_eq_sub_of_hasDerivAt_of_le hab hcont (fun x hx => (hderiv x hx).hasDerivAt) hint]

Premises used: DifferentiableAt.hasDerivAt, intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
⊢ ContinuousOn f (Icc b a)

Tactic:
simp only [uIcc_of_ge, hab, uIoo_of_ge] at hcont hderiv

Premises used: Set.uIoo_of_ge, Set.uIcc_of_ge
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hcont : ContinuousOn f [[a, b]]
hderiv : ∀ x ∈ uIoo a b, DifferentiableAt ℝ f x
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont₁ : ContinuousOn f (Icc b a)
⊢ ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x

Tactic:
simp only [uIcc_of_ge, hab, uIoo_of_ge] at hcont hderiv

Premises used: Set.uIoo_of_ge, Set.uIcc_of_ge
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
inst_2 : CompleteSpace E
f : ℝ → E
hint : IntervalIntegrable (deriv f) volume a b
hab : b ≤ a
hcont : ContinuousOn f (Icc b a)
hderiv : ∀ x ∈ Ioo b a, DifferentiableAt ℝ f x
inr : -∫ (x : ℝ) in b..a, deriv f x = f b - f a
inr₁ : -(f a - f b) = f b - f a
inr₂ inr₃ : f b - f a = f b - f a
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a

Tactic:
rw [integral_symm, integral_eq_sub_of_hasDerivAt_of_le hab hcont
        (fun x hx => (hderiv x hx).hasDerivAt) hint.symm, neg_sub]

Premises used: neg_sub, DifferentiableAt.hasDerivAt, intervalIntegral.integral_symm, IntervalIntegrable.symm, intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
⊢ IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1

Tactic:
have hint : IntervalIntegrable (z₁ • (f' ∘ γ)) MeasureTheory.volume 0 1 :=
    (ContinuousOn.const_smul hcont z₁).intervalIntegrable_of_Icc zero_le_one
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) [[0, 1]] t
⊢ HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t

Tactic:
(hderiv t <| (Set.uIcc_of_le (α := ℝ) zero_le_one).symm ▸ ht).scomp t <| .const_add _ ?_

Premises used: HasDerivAt.scomp, HasDerivAt.const_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) [[0, 1]] t
refine : HasDerivAt (fun (t : ℝ) ↦ t • z₁) z₁ t
⊢ HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t

Tactic:
refine (hderiv t <| (Set.uIcc_of_le (α := ℝ) zero_le_one).symm ▸ ht).scomp t <| .const_add _ ?_

Premises used: HasDerivAt.scomp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
t : ℝ
ht : Membership.mem (γ := Set ℝ) [[0, 1]] t
⊢ HasDerivAt (fun (t : ℝ) ↦ t • z₁) z₁ t

Tactic:
simp [hasDerivAt_iff_isLittleO, sub_smul]

Premises used: hasDerivAt_iff_isLittleO, sub_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
⊢ ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) [[0, 1]] t), HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t

Tactic:
have hderiv' (t) (ht : t ∈ Set.uIcc (0 : ℝ) 1) : HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t := by
    refine (hderiv t <| (Set.uIcc_of_le (α := ℝ) zero_le_one).symm ▸ ht).scomp t <| .const_add _ ?_
    simp [hasDerivAt_iff_isLittleO, sub_smul]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) [[0, 1]] t), HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
⊢ ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y = (f ∘ γ) 1 - (f ∘ γ) 0

Tactic:
(integral_eq_sub_of_hasDerivAt hderiv' hint)

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
f f' : 𝕜 → E
z₀ z₁ : 𝕜
hcont : ContinuousOn.{0, u_3} (Y := E) (fun (t : ℝ) ↦ f' (z₀ + t • z₁)) (Icc 0 1)
hderiv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)
γ : (t : ℝ) → 𝕜 := fun (t : ℝ) ↦ z₀ + t • z₁
hint : IntervalIntegrable (z₁ • f' ∘ γ) volume 0 1
hderiv' : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) [[0, 1]] t), HasDerivAt (f ∘ γ) (z₁ • (f' ∘ γ) t) t
h : HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = ∫ (y : ℝ) in 0..1, z₁ • (f' ∘ γ) y
h₁ : f (z₀ + z₁) - f z₀ = (f ∘ γ) 1 - (f ∘ γ) 0
⊢ HSMul.hSMul (β := E) z₁ (∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁)) = f (z₀ + z₁) - f z₀

Tactic:
convert! (integral_eq_sub_of_hasDerivAt hderiv' hint) using 1

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt