awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N) : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} x
hxN : x ∉ N
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Tactic:
exact ⟨x, hxN, hx⟩
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} : ℝ≥0∞)

Tactic:
simpa using
    measure_le_setLAverage_pos (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _) hf.restrict

Premises used: Iff.mpr, MeasureTheory.measure_le_setLAverage_pos, MeasureTheory.Measure.measure_univ_ne_zero, MeasureTheory.measure_ne_top, AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
⊢ ∃ (x : α), f x ≤ ⨍⁻ (a : α), f a ∂μ

Tactic:
let ⟨x, hx⟩ := nonempty_of_measure_ne_zero (measure_le_laverage_pos hμ hf).ne'
  ⟨x, hx⟩

Premises used: _private.0.MeasureTheory.exists_le_laverage.match_1, MeasureTheory.nonempty_of_measure_ne_zero, MeasureTheory.laverage, Exists, MeasureTheory.measure_le_laverage_pos, LE.le, LT.lt.ne', Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} : ℝ≥0∞)

Tactic:
have := measure_le_laverage_pos hμ hf
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N) : ℝ≥0∞)

Tactic:
rw [← measure_diff_null hN] at this

Premises used: MeasureTheory.measure_diff_null
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N) : ℝ≥0∞)
obtain :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} x) (hxN : x ∉ N),
    ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Tactic:
obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N) : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} x
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Tactic:
⟨x, hxN, hx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : AEMeasurable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N) : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} x
hxN : x ∉ N
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ

Tactic:
exact ⟨x, hxN, hx⟩
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst : IsProbabilityMeasure μ
hf : AEMeasurable f μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ∫⁻ (a : α), f a ∂μ} : ℝ≥0∞)

Tactic:
simpa only [laverage_eq_lintegral] using
    measure_le_laverage_pos (IsProbabilityMeasure.ne_zero μ) hf

Premises used: MeasureTheory.measure_le_laverage_pos, MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.laverage_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst : IsProbabilityMeasure μ
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ∫⁻ (a : α), f a ∂μ ≤ f x} : ℝ≥0∞)

Tactic:
simpa only [laverage_eq_lintegral] using
    measure_laverage_le_pos (IsProbabilityMeasure.ne_zero μ) hint

Premises used: MeasureTheory.measure_laverage_le_pos, MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.laverage_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst : IsProbabilityMeasure μ
hf : AEMeasurable f μ
⊢ ∃ (x : α), f x ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
simpa only [laverage_eq_lintegral] using exists_le_laverage (IsProbabilityMeasure.ne_zero μ) hf

Premises used: MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.exists_le_laverage, MeasureTheory.laverage_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
inst : IsProbabilityMeasure μ
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
⊢ ∃ (x : α), ∫⁻ (a : α), f a ∂μ ≤ f x

Tactic:
simpa only [laverage_eq_lintegral] using
    exists_laverage_le (IsProbabilityMeasure.ne_zero μ) hint

Premises used: MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.exists_laverage_le, MeasureTheory.laverage_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst : IsProbabilityMeasure μ
hf : AEMeasurable f μ
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ x ∉ N, f x ≤ ∫⁻ (a : α), f a ∂μ

Tactic:
simpa only [laverage_eq_lintegral] using
    exists_notMem_null_le_laverage (IsProbabilityMeasure.ne_zero μ) hf hN

Premises used: MeasureTheory.exists_notMem_null_le_laverage, MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.laverage_eq_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
inst : IsProbabilityMeasure μ
hint : ∫⁻ (a : α), f a ∂μ ≠ ∞
hN : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) N : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ x ∉ N, ∫⁻ (a : α), f a ∂μ ≤ f x

Tactic:
simpa only [laverage_eq_lintegral] using
    exists_notMem_null_laverage_le (IsProbabilityMeasure.ne_zero μ) hint hN

Premises used: MeasureTheory.IsProbabilityMeasure.ne_zero, MeasureTheory.exists_notMem_null_laverage_le, MeasureTheory.laverage_eq_lintegral
-- 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)
h : ∀ (i : ι) (hi : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)), Integrable (g i) μ
⊢ ∀ᶠ (i : ι) in l, Integrable (g i) μ

Tactic:
filter_upwards [(tendsto_order.1 hg).1 _ zero_lt_one] with i hi

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)
i : ι
hi : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
h : ∀ (hi : ¬Integrable (g i) μ), ¬LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
⊢ Integrable (g i) μ

Tactic:
contrapose hi
-- 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)
i : ι
hi : ¬Integrable (g i) μ
⊢ ¬LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)

Tactic:
simp only [integral_undef hi, lt_self_iff_false, not_false_eq_true]

Premises used: MeasureTheory.integral_undef, lt_self_iff_false, not_false_eq_true
-- 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)
⊢ ∀ᶠ (i : ι) in l, Integrable (g i) μ

Tactic:
have g_int : ∀ᶠ i in l, Integrable (g i) μ := by
    filter_upwards [(tendsto_order.1 hg).1 _ zero_lt_one] with i hi
    contrapose hi
    simp only [integral_undef hi, lt_self_iff_false, not_false_eq_true]
-- 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) μ
h :
  ∀ (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)),
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
⊢ ∀ᶠ (i : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ

Tactic:
filter_upwards [f_int, g_int, g_supp, g_bound] with i hif hig hisupp hibound
-- 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)
h : Eq.{u_2 + 1} (α := E) (∫ (a : α), g i a • (f a - c) + g i a • c ∂μ) (∫ (y : α), g i y • f y ∂μ)
h₁ : Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • (f y - c)) μ
h₂ : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ g i x • c) μ
⊢ ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ

Tactic:
rw [← integral_smul_const, ← integral_add]

Premises used: integral_smul_const, MeasureTheory.integral_add
-- 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)
⊢ Eq.{u_2 + 1} (α := E) (∫ (a : α), g i a • (f a - c) + g i a • c ∂μ) (∫ (y : α), g i y • f y ∂μ)

Tactic:
simp only [smul_sub, sub_add_cancel]

Premises used: smul_sub, sub_add_cancel
-- 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)
h : Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • f y - g i y • c) μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • (f y - c)) μ

Tactic:
simp_rw [smul_sub]

Premises used: smul_sub
-- 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)
apply : Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • f y) μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • f y - g i y • c) μ

Tactic:
apply Integrable.sub _ (hig.smul_const _)

Premises used: MeasureTheory.Integrable.sub, 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)
apply : (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ support (g i)
⊢ (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i

Tactic:
apply Subset.trans _ hisupp

Premises used: Set.Subset.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 : ι
hif : IntegrableOn f (a i) μ
hig : Integrable (g i) μ
hisupp : support (g i) ⊆ a i
hibound : ∀ (x : α), |g i x| ≤ K / μ.real (a i)
⊢ (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ support (g i)

Tactic:
Function.support_smul_subset_left _ _

Premises used: Function.support_smul_subset_left
-- 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)
⊢ (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ support (g i)

Tactic:
exact Function.support_smul_subset_left _ _

Premises used: Function.support_smul_subset_left
-- 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)
⊢ (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i

Tactic:
have A : Function.support (fun y ↦ g i y • f y) ⊆ a i := by
        apply Subset.trans _ hisupp
        exact Function.support_smul_subset_left _ _
-- 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)
A : (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i
rw : IntegrableOn.{u_1, u_2} (ε := E) (fun (y : α) ↦ g i y • f y) (a i) μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • f y) μ

Tactic:
rw [← integrableOn_iff_integrable_of_support_subset A]

Premises used: MeasureTheory.integrableOn_iff_integrable_of_support_subset
-- 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)
A : (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i
apply : MemLp (g i) ∞ (μ.restrict (a i))
⊢ IntegrableOn.{u_1, u_2} (ε := E) (fun (y : α) ↦ g i y • f y) (a i) μ

Tactic:
apply Integrable.smul_of_top_right hif

Premises used: MeasureTheory.Integrable.smul_of_top_right
-- 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)
A : (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i
⊢ MemLp (g i) ∞ (μ.restrict (a i))

Tactic:
memLp_top_of_bound hig.aestronglyMeasurable.restrict
        (K / μ.real (a i)) (Eventually.of_forall hibound)

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.memLp_top_of_bound, MeasureTheory.Measure.real, HDiv.hDiv, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.restrict
-- 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)
A : (support.{u_1, u_2} (M := E) fun (y : α) ↦ g i y • f y) ⊆ a i
⊢ MemLp (g i) ∞ (μ.restrict (a i))

Tactic:
exact memLp_top_of_bound hig.aestronglyMeasurable.restrict
        (K / μ.real (a i)) (Eventually.of_forall hibound)

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.memLp_top_of_bound, MeasureTheory.Measure.real, HDiv.hDiv, Filter.Eventually.of_forall, MeasureTheory.AEStronglyMeasurable.restrict