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 :
  ∀ᶠ (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
⊢ x ∉ support (g i)

Tactic:
fun h ↦ hx (hi h)

Premises used: Not
-- 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
⊢ x ∉ support (g i)

Tactic:
exact fun h ↦ hx (hi h)
-- 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
⊢ g i x = 0

Tactic:
have : g i x = 0 := by rw [← Function.notMem_support]; exact fun h ↦ hx (hi h)
-- 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 : ∀ (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
this : g i x = 0
⊢ ‖g i x‖ * ‖f x - c‖ = 0

Tactic:
simp [this]
-- 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 ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0

Tactic:
have : ∀ x, x ∉ a i → ‖g i x‖ * ‖(f x - c)‖ = 0 := by
      intro x hx
      have : g i x = 0 := by rw [← Function.notMem_support]; exact fun h ↦ hx (hi h)
      simp [this]
-- 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 : ∀ (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∞)
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
h :
  LE.le (α := ℝ) (∫ (x : α) in a i, ‖g i x‖ * ‖f x - c‖ ∂μ)
    (∫ (a_1 : α) in a i, K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖ ∂μ)
⊢ LE.le (α := ℝ) (∫ (a : α), ‖g i a‖ * ‖f a - c‖ ∂μ)
    (∫ (a_1 : α) in a i, K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖ ∂μ)

Tactic:
rw [← setIntegral_eq_integral_of_forall_compl_eq_zero this (μ := μ)]

Premises used: MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_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_1 : 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∞)
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
x : α
⊢ LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ ‖g i x‖ * ‖f x - c‖) x)

Tactic:
positivity
-- 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 : ∀ (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∞)
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
h : Integrable (ε := ℝ) (fun (a_1 : α) ↦ K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖) (μ.restrict (a i))
h₁ :
  ∀ (x : α),
    LE.le (α := ℝ) ((fun (x : α) ↦ ‖g i x‖ * ‖f x - c‖) x)
      ((fun (a_1 : α) ↦ K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖) x)
⊢ LE.le (α := ℝ) (∫ (x : α) in a i, ‖g i x‖ * ‖f x - c‖ ∂μ)
    (∫ (a_1 : α) in a i, K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖ ∂μ)

Tactic:
refine integral_mono_of_nonneg (Eventually.of_forall (fun x ↦ by positivity)) ?_
      (Eventually.of_forall (fun x ↦ ?_))

Premises used: Filter.Eventually.of_forall, MeasureTheory.integral_mono_of_nonneg
-- 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 : ∀ (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∞)
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
apply : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ c) (μ.restrict (a i))
⊢ Integrable (ε := ℝ) (fun (a_1 : α) ↦ K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖) (μ.restrict (a i))

Tactic:
apply (Integrable.sub h''i _).norm.const_mul

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.Integrable.sub, MeasureTheory.Integrable.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_1 : 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∞)
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
⊢ IntegrableOn.{u_1, u_2} (ε := E) (fun (x : α) ↦ c) (a i) μ

Tactic:
simp [mu_ai]
-- 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 : ∀ (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∞)
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
x : α
h : |g i x| ≤ K / (μ.restrict (a i)).real univ
⊢ |g i x| * ‖f x - c‖ ≤ K / (μ.restrict (a i)).real univ * ‖f x - c‖

Tactic:
gcongr
-- 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 : ∀ (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∞)
this : ∀ x ∉ a i, ‖g i x‖ * ‖f x - c‖ = 0
x : α
⊢ |g i x| ≤ K / (μ.restrict (a i)).real univ

Tactic:
simpa using h'i x
-- 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.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)

Tactic:
have L0 : Tendsto (fun i ↦ ∫ y, g i y • (f y - c) ∂μ) l (𝓝 0) := by
    have := hf.const_mul K
    simp only [mul_zero] at this
    refine squeeze_zero_norm' ?_ this
    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
    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
    apply (norm_integral_le_integral_norm _).trans
    simp_rw [average_eq, smul_eq_mul, ← integral_const_mul, norm_smul, ← mul_assoc,
      ← div_eq_mul_inv]
    have : ∀ x, x ∉ a i → ‖g i x‖ * ‖(f x - c)‖ = 0 := by
      intro x hx
      have : g i x = 0 := by rw [← Function.notMem_support]; exact fun h ↦ hx (hi h)
      simp [this]
    rw [← setIntegral_eq_integral_of_forall_compl_eq_zero this (μ := μ)]
    refine integral_mono_of_nonneg (Eventually.of_forall (fun x ↦ by positivity)) ?_
      (Eventually.of_forall (fun x ↦ ?_))
    · apply (Integrable.sub h''i _).norm.const_mul
      change IntegrableOn (fun _ ↦ c) (a i) μ
      simp [mu_ai]
    · dsimp; gcongr; simpa using h'i x
-- 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 ∂μ
L0 : Tendsto.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
⊢ Tendsto (fun (x : ι) ↦ ∫ (y : α), g x y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g x y ∂μ) c) l
    (𝓝 (0 + HSMul.hSMul (α := ℝ) 1 c))

Tactic:
have := L0.add (hg.smul_const c)
-- 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 ∂μ
L0 : Tendsto.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
this :
  Tendsto (fun (x : ι) ↦ ∫ (y : α), g x y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g x y ∂μ) c) l
    (𝓝 (0 + HSMul.hSMul (α := ℝ) 1 c))
⊢ Tendsto (fun (x : ι) ↦ ∫ (y : α), g x y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g x y ∂μ) c) l (𝓝 c)

Tactic:
simp only [one_smul, zero_add] at this

Premises used: zero_add, one_smul
-- 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 ∂μ
L0 : Tendsto.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
this : Tendsto (fun (x : ι) ↦ ∫ (y : α), g x y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g x y ∂μ) c) l (𝓝 c)
⊢ Tendsto (fun (i : ι) ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)

Tactic:
Tendsto.congr' I this

Premises used: Filter.Tendsto.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 ∂μ
L0 : Tendsto.{u_4, u_2} (β := E) (fun (i : ι) ↦ ∫ (y : α), g i y • (f y - c) ∂μ) l (𝓝 0)
this : Tendsto (fun (x : ι) ↦ ∫ (y : α), g x y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g x y ∂μ) c) l (𝓝 c)
⊢ Tendsto (fun (i : ι) ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)

Tactic:
exact Tendsto.congr' I this

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : TopologicalSpace α
f : α → ℝ
hs : IsConnected s
hf : ContinuousOn f s
hint : IntegrableOn f s μ
hμfin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ave : ℝ := ⨍ (x : α) in s, f x ∂μ
S₁ : Set α := {x : α | x ∈ s ∧ f x ≤ ave}
S₂ : Set α := {x : α | x ∈ s ∧ ave ≤ f x}
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₁ : ℝ≥0∞)

Tactic:
have hS₁ : 0 < μ S₁ := measure_le_setAverage_pos hμ0 hμfin hint
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : TopologicalSpace α
f : α → ℝ
hs : IsConnected s
hf : ContinuousOn f s
hint : IntegrableOn f s μ
hμfin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ave : ℝ := ⨍ (x : α) in s, f x ∂μ
S₁ : Set α := {x : α | x ∈ s ∧ f x ≤ ave}
S₂ : Set α := {x : α | x ∈ s ∧ ave ≤ f x}
hS₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₁ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₂ : ℝ≥0∞)

Tactic:
have hS₂ : 0 < μ S₂ := measure_setAverage_le_pos hμ0 hμfin hint
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : TopologicalSpace α
f : α → ℝ
hs : IsConnected s
hf : ContinuousOn f s
hint : IntegrableOn f s μ
hμfin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ0 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ave : ℝ := ⨍ (x : α) in s, f x ∂μ
S₁ : Set α := {x : α | x ∈ s ∧ f x ≤ ave}
S₂ : Set α := {x : α | x ∈ s ∧ ave ≤ f x}
hS₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₁ : ℝ≥0∞)
hS₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₂ : ℝ≥0∞)
rcases : ∀ (c₁ : α) (hc₁ : c₁ ∈ S₁), ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ

Tactic:
rcases nonempty_of_measure_ne_zero hS₁.ne' with ⟨c₁, hc₁⟩

Premises used: MeasureTheory.nonempty_of_measure_ne_zero, LT.lt.ne'