awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
x : α
hx : x ∈ s \ u
⊢ ‖φ i x‖ ≤ δ

Tactic:
simpa only [Pi.zero_apply, dist_zero_left] using (hi x hx).le

Premises used: Pi.zero_apply, LT.lt.le, dist_zero_left
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
rw : δ * ∫ (a : α) in s \ u, ‖g a‖ ∂μ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
⊢ ∫ (x : α) in s \ u, δ * ‖g x‖ ∂μ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ

Tactic:
rw [integral_const_mul]

Premises used: MeasureTheory.integral_const_mul
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
apply : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖
apply₁ : s \ u ≤ᶠ[ae μ] s
⊢ δ * ∫ (a : α) in s \ u, ‖g a‖ ∂μ ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ

Tactic:
apply mul_le_mul_of_nonneg_left (setIntegral_mono_set hmg.norm _ _) δpos.le

Premises used: MeasureTheory.setIntegral_mono_set, LT.lt.le, MeasureTheory.Integrable.norm, mul_le_mul_of_nonneg_left
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
x : α
⊢ 0 x ≤ ‖g x‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ LE.le (α := ℝ) (0 x) ((fun (a : α) ↦ ‖g a‖) x)) x} a
h₁ h₂ : ∀ (x : α), 0 x ≤ ‖g x‖
⊢ (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ ‖g a‖

Tactic:
filter_upwards with x using norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
⊢ ∀ (a : α), (s \ u) a ≤ s a

Tactic:
diff_subset (s := s) (t := u)

Premises used: Set.diff_subset, Set.Mem, Set.diff, setOf, Set.Subset
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
h : ∀ (a : α), Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (s \ u) x ≤ s x) x} a
h₁ : ∀ (a : α), (s \ u) a ≤ s a
⊢ s \ u ≤ᶠ[ae μ] s

Tactic:
filter_upwards using diff_subset (s := s) (t := u)

Premises used: Set.diff_subset
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
⊢ norm.{u_2} (E := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ

Tactic:
have C : ‖∫ x in s \ u, φ i x • g x ∂μ‖ ≤ δ * ∫ x in s, ‖g x‖ ∂μ :=
    calc
      ‖∫ x in s \ u, φ i x • g x ∂μ‖ ≤ ∫ x in s \ u, ‖φ i x • g x‖ ∂μ :=
        norm_integral_le_integral_norm _
      _ ≤ ∫ x in s \ u, δ * ‖g x‖ ∂μ := by
        refine setIntegral_mono_on ?_ ?_ (hs.diff u_open.measurableSet) fun x hx => ?_
        · exact IntegrableOn.mono_set h''i.norm diff_subset
        · exact IntegrableOn.mono_set (hmg.norm.const_mul _) diff_subset
        rw [norm_smul]
        gcongr
        simpa only [Pi.zero_apply, dist_zero_left] using (hi x hx).le
      _ ≤ δ * ∫ x in s, ‖g x‖ ∂μ := by
        rw [integral_const_mul]
        apply mul_le_mul_of_nonneg_left (setIntegral_mono_set hmg.norm _ _) δpos.le
        · filter_upwards with x using norm_nonneg _
        · filter_upwards using diff_subset (s := s) (t := u)
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
C : norm.{u_2} (E := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
rw : norm.{u_2} (E := E) (∫ (x : α) in s \ u ∪ s ∩ u, φ i x • g x ∂μ)
| norm.{u_2} (E := E) (∫ (x : α) in s, φ i x • g x ∂μ)

Tactic:
rw [← diff_union_inter s u]

Premises used: Set.diff_union_inter
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
C : norm.{u_2} (E := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
conv_lhs :
  norm.{u_2} (E := E) (∫ (x : α) in s \ u ∪ s ∩ u, φ i x • g x ∂μ) =
    ‖HAdd.hAdd (α := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ)‖
⊢ norm.{u_2} (E := E) (∫ (x : α) in s, φ i x • g x ∂μ) =
    ‖HAdd.hAdd (α := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ)‖

Tactic:
conv_lhs => rw [← diff_union_inter s u]

Premises used: Set.diff_union_inter
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
C : norm.{u_2} (E := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
rw rw₁ :
  ‖HAdd.hAdd (α := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ)‖ =
    ‖HAdd.hAdd (α := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ)‖
⊢ norm.{u_2} (E := E) (∫ (x : α) in s \ u ∪ s ∩ u, φ i x • g x ∂μ) =
    ‖HAdd.hAdd (α := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ)‖

Tactic:
rw [setIntegral_union disjoint_sdiff_inter (hs.inter u_open.measurableSet)
          (h''i.mono_set diff_subset) (h''i.mono_set inter_subset_left)]

Premises used: MeasureTheory.setIntegral_union, Set.diff_subset, Set.disjoint_sdiff_inter, IsOpen.measurableSet, Set.inter_subset_left, MeasureTheory.IntegrableOn.mono_set, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
C : norm.{u_2} (E := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
⊢ ‖HAdd.hAdd (α := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ)‖ ≤
    norm.{u_2} (E := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) + norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ)

Tactic:
norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
C : norm.{u_2} (E := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
⊢ norm.{u_2} (E := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) + norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤
    δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ

Tactic:
add_le_add C B

Premises used: add_le_add
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s t : Set α
φ : ι → α → ℝ
hs : MeasurableSet s
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 0)
ε : ℝ
εpos : ε > 0
δ : ℝ
hδ : δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ < ε
δpos : 0 < δ
δone : δ < 1
u : Set α
u_open : IsOpen[inst] u
x₀u : x₀ ∈ u
ut : s ∩ u ⊆ t
hu : ∀ x ∈ u ∩ s, Membership.mem (γ := Set E) (ball 0 δ) (g x)
i : ι
hi : ∀ x ∈ s \ u, dist (0 x) (φ i x) < δ
h'i : ‖HSub.hSub (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) 1‖ < δ
hφpos : ∀ x ∈ s, 0 ≤ φ i x
h''i : IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ φ i x • g x) s μ
I : IntegrableOn (φ i) t μ
B : norm.{u_2} (E := E) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ) ≤ 2 * δ
C : norm.{u_2} (E := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ
x :
  norm.{u_2} (E := E) (∫ (x : α) in s, φ i x • g x ∂μ) =
    ‖HAdd.hAdd (α := E) (∫ (x : α) in s \ u, φ i x • g x ∂μ) (∫ (x : α) in s ∩ u, φ i x • g x ∂μ)‖
⊢ norm.{u_2} (E := E) (∫ (x : α) in s, φ i x • g x ∂μ) ≤ δ * ∫ (x : α) in s, ‖g x‖ ∂μ + 2 * δ

Tactic:
calc
    ‖∫ x in s, φ i x • g x ∂μ‖ =
      ‖(∫ x in s \ u, φ i x • g x ∂μ) + ∫ x in s ∩ u, φ i x • g x ∂μ‖ := by
      conv_lhs => rw [← diff_union_inter s u]
      rw [setIntegral_union disjoint_sdiff_inter (hs.inter u_open.measurableSet)
          (h''i.mono_set diff_subset) (h''i.mono_set inter_subset_left)]
    _ ≤ ‖∫ x in s \ u, φ i x • g x ∂μ‖ + ‖∫ x in s ∩ u, φ i x • g x ∂μ‖ := norm_add_le _ _
    _ ≤ (δ * ∫ x in s, ‖g x‖ ∂μ) + 2 * δ := add_le_add C B

Premises used: Norm.norm, HMul.hMul, add_le_add, MeasureTheory.Measure.restrict, norm_add_le, SDiff.sdiff, MeasureTheory.integral, HSMul.hSMul
-- Module: Mathlib.MeasureTheory.Integral.PeakFunction
Goal:
α : Type u_1
E : Type u_2
ι : Type u_3
hm : MeasurableSpace α
μ : Measure α
inst : TopologicalSpace α
inst_1 : BorelSpace α
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
g : α → E
l : Filter ι
x₀ : α
s : Set α
φ : ι → α → ℝ
a : E
inst_4 : CompleteSpace E
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
hts : t ⊆ s
h'ts : t ∈ 𝓝[s] x₀
h't : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hnφ : ∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x
hlφ : ∀ (u : Set α), IsOpen[inst] u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)
hiφ : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : α) in t, φ i x ∂μ) l (𝓝 1)
h'iφ : ∀ᶠ (i : ι) in l, AEStronglyMeasurable (φ i) (μ.restrict s)
hmg : IntegrableOn g s μ
hcg : Tendsto g (𝓝[s] x₀) (𝓝 a)
h : α → E := g - t.indicator fun (x : α) ↦ a
⊢ Tendsto (fun (i : ι) ↦ ∫ (x : α) in s, φ i x • h x ∂μ + HSMul.hSMul (α := ℝ) (∫ (x : α) in t, φ i x ∂μ) a) l
    (𝓝 (0 + HSMul.hSMul (α := ℝ) 1 a))

Tactic:
Tendsto.add ?_ (Tendsto.smul hiφ tendsto_const_nhds)

Premises used: tendsto_const_nhds, Filter.Tendsto.smul, Filter.Tendsto.add