awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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∞)
⊢ LE.le (α := ℝ) (∫ (a : α), ‖g i a‖ * ‖f a - c‖ ∂μ)
    (∫ (a_1 : α) in a i, K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖ ∂μ)
have this₁ : ∀ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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
⊢ LE.le (α := ℝ) (∫ (a : α), ‖g i a‖ * ‖f a - c‖ ∂μ)
    (∫ (a_1 : α) in a i, K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖ ∂μ)
have 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‖ ∂μ)
Tactic: rw [← setIntegral_eq_integral_of_forall_compl_eq_zero this (μ := μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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
⊢ 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‖ ∂μ)
have h : Integrable (ε := ℝ) (fun (a_1 : α) ↦ K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖) (μ.restrict (a i))
Tactic: refine integral_mono_of_nonneg (Eventually.of_forall (fun x ↦ by positivity)) ?_
      (Eventually.of_forall (fun x ↦ ?_))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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))
⊢ 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‖ ∂μ)
have 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)
Tactic: refine integral_mono_of_nonneg (Eventually.of_forall (fun x ↦ by positivity)) ?_
      (Eventually.of_forall (fun x ↦ ?_))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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
⊢ Integrable (ε := ℝ) (fun (a_1 : α) ↦ K / (μ.restrict (a i)).real univ * ‖f a_1 - c‖) (μ.restrict (a i))
have apply : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ c) (μ.restrict (a i))
Tactic: apply (Integrable.sub h''i _).norm.const_mul
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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| * ‖f x - c‖ ≤ K / (μ.restrict (a i)).real univ * ‖f x - c‖
have h : |g i x| ≤ K / (μ.restrict (a i)).real univ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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 (i : ι) ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)
have L0 : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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 (i : ι) ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)
have this : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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 (i : ι) ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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}
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
have hS₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₁ : ℝ≥0∞)
Tactic: have hS₁ : 0 < μ S₁ := measure_le_setAverage_pos hμ0 hμfin hint
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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∞)
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
have hS₂ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) S₂ : ℝ≥0∞)
Tactic: have hS₂ : 0 < μ S₂ := measure_setAverage_le_pos hμ0 hμfin hint
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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∞)
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
have rcases : ∀ (c₁ : α) (hc₁ : c₁ ∈ S₁), ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
Tactic: rcases nonempty_of_measure_ne_zero hS₁.ne' with ⟨c₁, hc₁⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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∞)
c₁ : α
hc₁ : c₁ ∈ S₁
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
have rcases : ∀ (c₂ : α) (hc₂ : c₂ ∈ S₂), ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
Tactic: rcases nonempty_of_measure_ne_zero hS₂.ne' with ⟨c₂, hc₂⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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∞)
c₁ : α
hc₁ : c₁ ∈ S₁
c₂ : α
hc₂ : c₂ ∈ S₂
⊢ ∃ c ∈ s, f c = ⨍ (x : α) in s, f x ∂μ
have a : ⨍ (x : α) in s, f x ∂μ ∈ Icc (f c₁) (f c₂)
Tactic: apply hs.isPreconnected.intermediate_value hc₁.1 hc₂.1 hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
⊢ ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f
have pos : ∀ (hE : CompleteSpace E), ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) sorry f
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
pos : ∀ (hE : CompleteSpace E), ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f
⊢ ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f
have neg : ∀ (hE : ¬CompleteSpace E), ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) sorry f
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hE : CompleteSpace E
⊢ ∫ (a : α), f a ∂μ = setToFun μ (weightedSMul μ) ⋯ f
have pos : Eq.{u_2 + 1} (α := E)
  (if hf : Integrable.{u_2, u_1} (ε := E) (fun (a : α) ↦ f a) μ then
    (L1.integralCLM : (a : ↥(Lp E 1 μ)) → E) (Integrable.toL1 (fun (a : α) ↦ f a) hf)
  else 0)
  (if hf : Integrable f μ then (L1.setToL1 sorry : (a : ↥(Lp E 1 μ)) → E) (Integrable.toL1 f hf) else 0)
Tactic: simp only [integral, hE, ↓reduceDIte, L1.integral, setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral f = ∫ (a : α), (↑(↑f : α →ₘ[μ] E) : α → E) a ∂μ
have simp : (integralCLM : (a : ↥(Lp E 1 μ)) → E) f = setToFun μ (weightedSMul μ) sorry (↑(↑f : α →ₘ[μ] E) : α → E)
Tactic: simp only [integral, L1.integral, integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
h : ¬Integrable f μ
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), f a ∂μ) 0
have simp : setToFun μ (weightedSMul μ) sorry f = 0
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : α), 0 ∂μ) 0
have simp : Eq.{u_5 + 1} (α := G) (setToFun μ (weightedSMul μ) sorry fun (a : α) ↦ 0) 0
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
f : β → α → G
s : Set β
b : β
⊢ Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
    (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)
have pos : ∀ (hb : b ∈ s),
  Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
    (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)
Tactic: by_cases hb : b ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
f : β → α → G
s : Set β
b : β
pos :
  ∀ (hb : b ∈ s),
    Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
      (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)
⊢ Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
    (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)
have neg : ∀ (hb : b ∉ s),
  Eq.{u_5 + 1} (α := G) (∫ (y : α), s.indicator (fun (x : β) ↦ f x y) b ∂μ)
    (s.indicator (fun (x : β) ↦ ∫ (y : α), f x y ∂μ) b)
Tactic: by_cases hb : b ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫ (a : α), f a + g a ∂μ = HAdd.hAdd (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
have simp : (setToFun μ (weightedSMul μ) sorry fun (a : α) ↦ f a + g a) =
  setToFun μ (weightedSMul μ) sorry f + setToFun μ (weightedSMul μ) sorry g
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
ι : Type u_6
s : Finset ι
f : ι → α → G
hf : ∀ i ∈ s, Integrable (f i) μ
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), ∑ i ∈ s, f i a ∂μ) (∑ i ∈ s, ∫ (a : α), f i a ∂μ)
have simp : Eq.{u_5 + 1} (α := G) (setToFun μ (weightedSMul μ) sorry fun (a : α) ↦ ∑ i ∈ s, f i a)
  (∑ x ∈ s, setToFun μ (weightedSMul μ) sorry (f x))
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ Eq.{u_5 + 1} (α := G) (∫ (a : α), -f a ∂μ) (-∫ (a : α), f a ∂μ)
have simp : (setToFun μ (weightedSMul μ) sorry fun (a : α) ↦ -f a) = -setToFun μ (weightedSMul μ) sorry f
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
hf : Integrable f μ
hg : Integrable g μ
⊢ ∫ (a : α), f a - g a ∂μ = HSub.hSub (α := G) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
have simp : (setToFun μ (weightedSMul μ) sorry fun (a : α) ↦ f a - g a) =
  setToFun μ (weightedSMul μ) sorry f - setToFun μ (weightedSMul μ) sorry g
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
𝕜 : Type u_4
inst : NormedDivisionRing 𝕜
G : Type u_5
inst_1 : NormedAddCommGroup G
inst_2 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst_3 : Module 𝕜 G
inst_4 : NormSMulClass 𝕜 G
inst_5 : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
⊢ ∫ (a : α), c • f a ∂μ = HSMul.hSMul (β := G) c (∫ (a : α), f a ∂μ)
have simp : (setToFun μ (weightedSMul μ) sorry fun (a : α) ↦ c • f a) = c • setToFun μ (weightedSMul μ) sorry f
Tactic: simp only [integral_eq_setToFun]