awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
refine : ∀ (y : E) (hy : y ∈ ball a ε), ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖
⊢ ∃ ε > 0, ∀ y ∈ ball a ε, ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖

Tactic:
refine ⟨ε, hε₀, fun y hy ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
⊢ 0 ≤ ‖y - a‖ ^ (r + 1)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
⊢ 0 ≤ ‖y - a‖

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
⊢ r + 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
rw : ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖
⊢ ‖f y - f a‖ ≤ C * ‖‖y - a‖ ^ (r + 1)‖

Tactic:
rw [Real.norm_of_nonneg (by positivity), Real.rpow_add_one' (by positivity) (by positivity),
    ← mul_assoc]

Premises used: mul_assoc, Real.rpow_add_one', Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
⊢ closedBall a ‖y - a‖ ⊆ ball a ε

Tactic:
have hsub : closedBall a ‖y - a‖ ⊆ ball a ε :=
    closedBall_subset_ball (mem_ball_iff_norm.mp hy)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
hf : ∀ x ∈ closedBall a ‖y - a‖, DifferentiableAt ℝ f x
bound : ∀ x ∈ closedBall a ‖y - a‖, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖y - a‖ ^ r
xs : a ∈ closedBall a ‖y - a‖
ys : y ∈ closedBall a ‖y - a‖
⊢ ‖f y - f a‖ ≤ C * ‖y - a‖ ^ r * ‖y - a‖

Tactic:
apply (convex_closedBall a ‖y - a‖).norm_image_sub_le_of_norm_fderiv_le (𝕜 := ℝ)

Premises used: Norm.norm, HSub.hSub, Convex.norm_image_sub_le_of_norm_fderiv_le, convex_closedBall
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
⊢ ∀ x ∈ closedBall a ‖y - a‖, DifferentiableAt ℝ f x

Tactic:
fun z hz ↦ (hε z <| hsub hz).1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
⊢ ∀ x ∈ closedBall a ‖y - a‖, DifferentiableAt ℝ f x

Tactic:
exact fun z hz ↦ (hε z <| hsub hz).1

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
z : E
hz : z ∈ closedBall a ‖y - a‖
⊢ 0 ≤ ‖z - a‖ ^ r

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
z : E
hz : z ∈ closedBall a ‖y - a‖
bound : C * ‖‖z - a‖ ^ r‖ ≤ C * ‖y - a‖ ^ r
bound₁ : C * ‖z - a‖ ^ r ≤ C * ‖y - a‖ ^ r
bound₂ bound₃ : C * ‖y - a‖ ^ r ≤ C * ‖y - a‖ ^ r
⊢ norm (E := E →L[ℝ] F) (fderiv ℝ f z) ≤ C * ‖y - a‖ ^ r

Tactic:
grw [(hε z <| hsub hz).2, Real.norm_of_nonneg (by positivity), mem_closedBall_iff_norm.mp hz]

Premises used: mem_closedBall_iff_norm, And.right, Iff.mp, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
⊢ a ∈ closedBall a ‖y - a‖

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
C : ℝ
hC₀ : C > 0
hC : ∀ᶠ (x : E) in 𝓝 a, norm (E := E →L[ℝ] F) (fderiv ℝ f x) ≤ C * ‖‖x - a‖ ^ r‖
ε : ℝ
hε₀ : ε > 0
hε : ∀ y ∈ ball a ε, DifferentiableAt ℝ f y ∧ norm (E := E →L[ℝ] F) (fderiv ℝ f y) ≤ C * ‖‖y - a‖ ^ r‖
y : E
hy : y ∈ ball a ε
hsub : closedBall a ‖y - a‖ ⊆ ball a ε
⊢ y ∈ closedBall a ‖y - a‖

Tactic:
simp [dist_eq_norm_sub]

Premises used: dist_eq_norm_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.DistLEIntegral
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f : E → F
a : E
r : ℝ
hr : 0 ≤ r
hdf : ∀ᶠ (x : E) in 𝓝 a, DifferentiableAt ℝ f x
hderiv : Asymptotics.IsBigO (E := E →L[ℝ] F) (F := ℝ) (𝓝 a) (fderiv ℝ f) fun (x : E) ↦ ‖x - a‖ ^ r
hf₀ : f a = 0
⊢ Asymptotics.IsBigO (F := ℝ) (𝓝 a) f fun (x : E) ↦ ‖x - a‖ ^ (r + 1)

Tactic:
simpa [hf₀] using sub_isBigO_norm_rpow_add_one_of_fderiv hr hdf hderiv

Premises used: sub_isBigO_norm_rpow_add_one_of_fderiv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : ℝ
rw : FTCFilter a (Pure.pure a) ⊥
⊢ FTCFilter a (𝓝[{a}] a) ⊥

Tactic:
rw [nhdsWithin, principal_singleton, inf_eq_right.2 (pure_le_nhds a)]

Premises used: Iff.mpr, pure_le_nhds, nhdsWithin, Filter.principal_singleton, inf_eq_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : ℝ
⊢ FTCFilter a (Pure.pure a) ⊥

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
a : ℝ
l l' : Filter ℝ
h : FTCFilter a l l'
μ : Measure ℝ
inst : IsLocallyFiniteMeasure μ
⊢ μ.FiniteAtFilter l'

Tactic:
(μ.finiteAt_nhds a).filter_mono h.le_nhds

Premises used: MeasureTheory.Measure.finiteAt_nhds, intervalIntegral.FTCFilter.le_nhds, MeasureTheory.Measure.FiniteAtFilter.filter_mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : ℝ
rw : FTCFilter a (𝓝 a) (𝓝 a)
⊢ FTCFilter a (𝓝[univ] a) (𝓝 a)

Tactic:
rw [nhdsWithin_univ]

Premises used: nhdsWithin_univ
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a : ℝ
⊢ FTCFilter a (𝓝 a) (𝓝 a)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x a b : ℝ
h : Fact (x ∈ [[a, b]])
⊢ FTCFilter x (𝓝[[[a, b]]] x) (𝓝[[[a, b]]] x)

Tactic:
.nhdsIcc (h := h)

Premises used: intervalIntegral.FTCFilter.nhdsIcc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
pos :
  ∀ (hE : CompleteSpace E),
    IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
      (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
      ∫ (x : ℝ) in u t..v t, 1 ∂μ
neg :
  ∀ (hE : ¬CompleteSpace E),
    IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
      (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
      ∫ (x : ℝ) in u t..v t, 1 ∂μ
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
by_cases hE : CompleteSpace E

Premises used: CompleteSpace
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : ¬CompleteSpace E
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
simp [intervalIntegral, integral, hE]

Premises used: intervalIntegral, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))

Tactic:
have A := hf.integral_sub_linear_isLittleO_ae hfm hl (hu.Ioc hv)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))

Tactic:
have B := hf.integral_sub_linear_isLittleO_ae hfm hl (hv.Ioc hu)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
pos :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c))
    fun (t : ι) ↦ HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ HSub.hSub (α := E) (∫ (x : ℝ) in u t..v t, f x ∂μ) (∫ (x : ℝ) in u t..v t, c ∂μ)) fun (t : ι) ↦
    ∫ (x : ℝ) in u t..v t, 1 ∂μ

Tactic:
simp_rw [integral_const', sub_smul]

Premises used: sub_smul, intervalIntegral.integral_const'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c))
    fun (t : ι) ↦ HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1

Tactic:
((A.trans_le fun t ↦ ?_).sub (B.trans_le fun t ↦ ?_)).congr_left fun t ↦ ?_

Premises used: Asymptotics.IsLittleO.congr_left, Asymptotics.IsLittleO.trans_le, Asymptotics.IsLittleO.sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
pos :
  ∀ (t : ι),
    ‖μ.real (Ioc (u t) (v t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
pos₁ :
  ∀ (t : ι),
    ‖μ.real (Ioc (v t) (u t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
pos₂ :
  ∀ (t : ι),
    ∫ (x : ℝ) in Ioc (u t) (v t), f x ∂μ - μ.real (Ioc (u t) (v t)) • c -
        (∫ (x : ℝ) in Ioc (v t) (u t), f x ∂μ - μ.real (Ioc (v t) (u t)) • c) =
      ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c)
⊢ IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (t : ι) ↦ ∫ (x : ℝ) in u t..v t, f x ∂μ - (μ.real (Ioc (u t) (v t)) • c - μ.real (Ioc (v t) (u t)) • c))
    fun (t : ι) ↦ HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1

Tactic:
refine ((A.trans_le fun t ↦ ?_).sub (B.trans_le fun t ↦ ?_)).congr_left fun t ↦ ?_

Premises used: Asymptotics.IsLittleO.congr_left, Asymptotics.IsLittleO.trans_le, Asymptotics.IsLittleO.sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
pos :
  u t ≤ v t →
    ‖μ.real (Ioc (u t) (v t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
pos₁ :
  v t ≤ u t →
    ‖μ.real (Ioc (u t) (v t))‖ ≤
      ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖
⊢ ‖μ.real (Ioc (u t) (v t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖

Tactic:
cases le_total (u t) (v t)

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
ι : Type u_1
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
c : E
l l' : Filter ℝ
lt : Filter ι
μ : Measure ℝ
u v : ι → ℝ
inst_2 : l'.IsMeasurablyGenerated
inst_3 : TendstoIxxClass Ioc l l'
hfm : StronglyMeasurableAtFilter f l' μ
hf : Tendsto f (l' ⊓ ae μ) (𝓝 c)
hl : μ.FiniteAtFilter l'
hu : Tendsto u lt l
hv : Tendsto v lt l
hE : CompleteSpace E
A :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (u i) (v i), f x ∂μ - μ.real (Ioc (u i) (v i)) • c) fun (i : ι) ↦
    μ.real (Ioc (u i) (v i))
B :
  IsLittleO.{u_1, u_3, 0} (E := E) (F := ℝ) lt
    (fun (i : ι) ↦ ∫ (x : ℝ) in Ioc (v i) (u i), f x ∂μ - μ.real (Ioc (v i) (u i)) • c) fun (i : ι) ↦
    μ.real (Ioc (v i) (u i))
t : ι
h : u t ≤ v t
⊢ ‖μ.real (Ioc (u t) (v t))‖ ≤
    ‖HSMul.hSMul (β := ℝ) (μ.real (Ioc (u t) (v t))) 1 - HSMul.hSMul (β := ℝ) (μ.real (Ioc (v t) (u t))) 1‖

Tactic:
simp [*]