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 μ
⊢ IntegrableOn (φ i) t μ

Tactic:
have I : IntegrableOn (φ i) t μ := by
    apply Integrable.of_integral_ne_zero (fun h ↦ ?_)
    simp [h] at h'i
    linarith
-- 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 μ
⊢ LE.le (α := ℝ) (∫ (x : α) in s ∩ u, ‖φ i x • g x‖ ∂μ) (∫ (x : α) in s ∩ u, ‖φ i x‖ * δ ∂μ)

Tactic:
setIntegral_mono_on ?_ ?_ (hs.inter u_open.measurableSet) fun x hx => ?_

Premises used: IsOpen.measurableSet, MeasureTheory.setIntegral_mono_on, 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 μ
refine_1 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x • g x‖) (s ∩ u) μ
refine_2 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x‖ * δ) (s ∩ u) μ
refine_3 : ∀ (x : α) (hx : x ∈ s ∩ u), ‖φ i x • g x‖ ≤ ‖φ i x‖ * δ
⊢ LE.le (α := ℝ) (∫ (x : α) in s ∩ u, ‖φ i x • g x‖ ∂μ) (∫ (x : α) in s ∩ u, ‖φ i x‖ * δ ∂μ)

Tactic:
refine setIntegral_mono_on ?_ ?_ (hs.inter u_open.measurableSet) fun x hx => ?_

Premises used: IsOpen.measurableSet, MeasureTheory.setIntegral_mono_on, 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 μ
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x • g x‖) (s ∩ u) μ

Tactic:
IntegrableOn.mono_set h''i.norm inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.Integrable.norm
-- 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 μ
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x • g x‖) (s ∩ u) μ

Tactic:
exact IntegrableOn.mono_set h''i.norm inter_subset_left

Premises used: Set.inter_subset_left, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.Integrable.norm
-- 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 μ
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x‖ * δ) (s ∩ u) μ

Tactic:
IntegrableOn.mono_set (I.norm.mul_const _) ut

Premises used: MeasureTheory.IntegrableOn.mono_set, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm
-- 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 μ
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x‖ * δ) (s ∩ u) μ

Tactic:
exact IntegrableOn.mono_set (I.norm.mul_const _) ut

Premises used: MeasureTheory.IntegrableOn.mono_set, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm
-- 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 μ
x : α
hx : x ∈ s ∩ u
refine_3 : ‖φ i x‖ * ‖g x‖ ≤ ‖φ i x‖ * δ
⊢ ‖φ i x • g x‖ ≤ ‖φ i x‖ * δ

Tactic:
rw [norm_smul]

Premises used: norm_smul
-- 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 μ
x : α
hx : x ∈ s ∩ u
refine_3 : ‖g x‖ ≤ δ
⊢ ‖φ i x‖ * ‖g x‖ ≤ ‖φ i x‖ * δ

Tactic:
gcongr
-- 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 μ
x : α
hx : x ∈ s ∩ u
refine_3 :
  ∀ (hu : ∀ x ∈ s ∩ u, 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 μ) (x : α)
    (hx : x ∈ s ∩ u), ‖g x‖ ≤ δ
⊢ ‖g x‖ ≤ δ

Tactic:
rw [inter_comm] at hu

Premises used: Set.inter_comm
-- 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 ∈ s ∩ u, 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 μ
x : α
hx : x ∈ s ∩ u
⊢ ‖g x‖ ≤ δ

Tactic:
(mem_ball_zero_iff.1 (hu x hx)).le

Premises used: LT.lt.le, Iff.mp, mem_ball_zero_iff
-- 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 ∈ s ∩ u, 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 μ
x : α
hx : x ∈ s ∩ u
⊢ ‖g x‖ ≤ δ

Tactic:
exact (mem_ball_zero_iff.1 (hu x hx)).le

Premises used: LT.lt.le, Iff.mp, mem_ball_zero_iff
-- 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 μ
hfi : IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x‖ * δ) t μ
hf : (ae (μ.restrict t)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖φ i x‖ * δ
hst : s ∩ u ≤ᶠ[ae μ] t
⊢ LE.le (α := ℝ) (∫ (x : α) in s ∩ u, ‖φ i x‖ * δ ∂μ) (∫ (x : α) in t, ‖φ i x‖ * δ ∂μ)

Tactic:
apply setIntegral_mono_set

Premises used: MeasureTheory.setIntegral_mono_set
-- 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 μ
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x‖ * δ) t μ

Tactic:
I.norm.mul_const _

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm
-- 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 μ
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ ‖φ i x‖ * δ) t μ

Tactic:
exact I.norm.mul_const _

Premises used: MeasureTheory.Integrable.mul_const, MeasureTheory.Integrable.norm
-- 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 μ
⊢ (ae (μ.restrict t)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖φ i x‖ * δ

Tactic:
Eventually.of_forall fun x => mul_nonneg (norm_nonneg _) δpos.le

Premises used: mul_nonneg, LT.lt.le, Filter.Eventually.of_forall, Filter.EventuallyLE, 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 μ
⊢ (ae (μ.restrict t)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ ‖φ i x‖ * δ

Tactic:
exact Eventually.of_forall fun x => mul_nonneg (norm_nonneg _) δpos.le

Premises used: mul_nonneg, LT.lt.le, Filter.Eventually.of_forall, norm_nonneg