awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ g i x • c) μ

Tactic:
hig.smul_const _

Premises used: MeasureTheory.Integrable.smul_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
i : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ g i x • c) μ

Tactic:
exact hig.smul_const _

Premises used: MeasureTheory.Integrable.smul_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
⊢ ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ

Tactic:
have I : ∀ᶠ i in l, ∫ y, g i y • (f y - c) ∂μ + (∫ y, g i y ∂μ) • c = ∫ y, g i y • f y ∂μ := by
    filter_upwards [f_int, g_int, g_supp, g_bound] with i hif hig hisupp hibound
    rw [← integral_smul_const, ← integral_add]
    · simp only [smul_sub, sub_add_cancel]
    · simp_rw [smul_sub]
      apply Integrable.sub _ (hig.smul_const _)
      have A : Function.support (fun y ↦ g i y • f y) ⊆ a i := by
        apply Subset.trans _ hisupp
        exact Function.support_smul_subset_left _ _
      rw [← integrableOn_iff_integrable_of_support_subset A]
      apply Integrable.smul_of_top_right hif
      exact memLp_top_of_bound hig.aestronglyMeasurable.restrict
        (K / μ.real (a i)) (Eventually.of_forall hibound)
    · exact hig.smul_const _
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
⊢ Tendsto (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 (K * 0))

Tactic:
have := hf.const_mul K
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 (K * 0))
⊢ Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)

Tactic:
simp only [mul_zero] at this

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
⊢ Tendsto.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)

Tactic:
squeeze_zero_norm' ?_ this

Premises used: squeeze_zero_norm'
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
refine : ∀ᶠ (n : ι) in l, norm.{u_2} (E := E) (∫ (y : α), g n y • (f y - c) ∂μ) ≤ K * ⨍ (y : α) in a n, ‖f y - c‖ ∂μ
⊢ Tendsto.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)

Tactic:
refine squeeze_zero_norm' ?_ this

Premises used: squeeze_zero_norm'
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
h :
  ∀ (i : ι) (hi : support (g i) ⊆ a i) (h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)) (h''i : IntegrableOn f (a i) μ)
    (hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)),
    norm.{u_2} (E := E) (∫ (y : α), g i y • (f y - c) ∂μ) ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ
⊢ ∀ᶠ (n : ι) in l, norm.{u_2} (E := E) (∫ (y : α), g n y • (f y - c) ∂μ) ≤ K * ⨍ (y : α) in a n, ‖f y - c‖ ∂μ

Tactic:
filter_upwards [g_supp, g_bound, f_int, (tendsto_order.1 hg).1 _ zero_lt_one]
      with i hi h'i h''i hi_int

Premises used: tendsto_order, zero_lt_one, And.left, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
rw : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (x : α), g i x = 0

Tactic:
simp only [h, ENNReal.toReal_top, _root_.div_zero, abs_nonpos_iff, measureReal_def] at h'i

Premises used: abs_nonpos_iff, MeasureTheory.measureReal_def, ENNReal.toReal_top, div_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h'i : ∀ (x : α), g i x = 0
e_f : Eq.{u_1 + 1} (α := α → ℝ) (fun (y : α) ↦ g i y) fun (y : α) ↦ 0
⊢ Eq (α := ℝ) (∫ (y : α), g i y ∂μ) (∫ (y : α), 0 ∂μ)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h'i : ∀ (x : α), g i x = 0
e_f : ∀ (y : α), g i y = 0
⊢ Eq.{u_1 + 1} (α := α → ℝ) (fun (y : α) ↦ g i y) fun (y : α) ↦ 0

Tactic:
ext y
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h'i : ∀ (x : α), g i x = 0
y : α
⊢ g i y = 0

Tactic:
h'i y
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h'i : ∀ (x : α), g i x = 0
y : α
⊢ g i y = 0

Tactic:
exact h'i y
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h'i : ∀ (x : α), g i x = 0
⊢ Eq (α := ℝ) (∫ (y : α), g i y ∂μ) (∫ (y : α), 0 ∂μ)

Tactic:
have : ∫ (y : α), g i y ∂μ = ∫ (y : α), 0 ∂μ := by congr; ext y; exact h'i y
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this_1 : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h'i : ∀ (x : α), g i x = 0
this : Eq (α := ℝ) (∫ (y : α), g i y ∂μ) (∫ (y : α), 0 ∂μ)
⊢ False

Tactic:
simp [this] at hi_int
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have mu_ai : μ (a i) < ∞ := by
      rw [lt_top_iff_ne_top]
      intro h
      simp only [h, ENNReal.toReal_top, _root_.div_zero, abs_nonpos_iff, measureReal_def] at h'i
      have : ∫ (y : α), g i y ∂μ = ∫ (y : α), 0 ∂μ := by congr; ext y; exact h'i y
      simp [this] at hi_int
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
mu_ai : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h : ∫ (a : α), ‖g i a • (f a - c)‖ ∂μ ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ
⊢ norm.{u_2} (E := E) (∫ (y : α), g i y • (f y - c) ∂μ) ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ

Tactic:
apply (norm_integral_le_integral_norm _).trans

Premises used: MeasureTheory.norm_integral_le_integral_norm, LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
mu_ai : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  LE.le (α := ℝ) (∫ (a : α), ‖g i a‖ * ‖f a - c‖ ∂μ)
    (∫ (a_1 : α) in a i, K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖ ∂μ)
⊢ ∫ (a : α), ‖g i a • (f a - c)‖ ∂μ ≤ K * ⨍ (y : α) in a i, ‖f y - c‖ ∂μ

Tactic:
simp_rw [average_eq, smul_eq_mul, ← integral_const_mul, norm_smul, ← mul_assoc,
      ← div_eq_mul_inv]

Premises used: MeasureTheory.integral_const_mul, norm_smul, mul_assoc, div_eq_mul_inv, smul_eq_mul, MeasureTheory.average_eq
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : CompleteSpace E
ι : Type u_4
a : ι → Set α
l : Filter ι
f : α → E
c : E
g : ι → α → ℝ
K : ℝ
hf : Tendsto (β := ℝ) (fun (i : ι) ↦ ⨍ (y : α) in a i, ‖f y - c‖ ∂μ) l (𝓝 0)
f_int : ∀ᶠ (i : ι) in l, IntegrableOn f (a i) μ
hg : Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (y : α), g i y ∂μ) l (𝓝 1)
g_supp : ∀ᶠ (i : ι) in l, support (g i) ⊆ a i
g_bound : ∀ᶠ (i : ι) in l, ∀ (x : α), |g i x| ≤ K / μ.real (a i)
g_int : ∀ᶠ (i : ι) in l, Integrable (g i) μ
I :
  ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
this : Tendsto (β := ℝ) (fun (x : ι) ↦ K * ⨍ (y : α) in a x, ‖f y - c‖ ∂μ) l (𝓝 0)
i : ι
hi : support (g i) ⊆ a i
h'i : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
h''i : IntegrableOn f (a i) μ
hi_int : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
mu_ai : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (a i) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : x ∉ a i
rw : x ∉ support (g i)
⊢ g i x = 0

Tactic:
rw [← Function.notMem_support]

Premises used: Function.notMem_support