awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x : α | f x = ∞}) :
      ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
have inr : Subset.{u_1} (α := Set α) ({a : α | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x : α | f x = ∞})
  {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ}
Tactic: refine this.trans_le (measure_mono ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x : α | f x = ∞}) :
      ℝ≥0∞)
x : α
hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ
hx : x ∉ {x : α | f x = ∞}
⊢ Membership.mem (γ := Set α) {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ} x
have inr : ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
Tactic: rwa [← toReal_laverage hf, toReal_le_toReal hx (setLAverage_lt_top h).ne] at hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x : α | f x = ∞}) :
      ℝ≥0∞)
x : α
hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ
hx : x ∉ {x : α | f x = ∞}
⊢ ∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ∞
have inr : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [ae_iff, not_ne_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
have inl : ∀ (hμ₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
Tactic: obtain hμ₁ | hμ₁ := eq_or_ne (μ s) ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
inl :
  ∀ (hμ₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
have inr : ∀ (hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
Tactic: obtain hμ₁ | hμ₁ := eq_or_ne (μ s) ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
have inr : ∀ (g : α → ℝ≥0∞) (hg : Measurable g) (hgf : g ≤ f) (hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
Tactic: obtain ⟨g, hg, hgf, hfg⟩ := exists_measurable_le_lintegral_eq (μ.restrict s) f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
have simp_rw : HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (a : α) in s, f a ∂μ) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (a : α) in s, g a ∂μ) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: simp_rw [laverage_eq, hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
have hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
Tactic: have hfg' : ⨍⁻ a in s, f a ∂μ = ⨍⁻ a in s, g a ∂μ := by simp_rw [laverage_eq, hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hint : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
have hint₁ : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
Tactic: rw [hfg] at hint
Cleared hypotheses: hint, hg, hgf, hfg, hfg'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
have this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal} : ℝ≥0∞)
Tactic: have :=
    measure_setAverage_le_pos hμ hμ₁ (integrable_toReal_of_lintegral_ne_top hg.aemeasurable hint)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍⁻ (a : α) in s, f a ∂μ ≤ f x} : ℝ≥0∞)
have inr : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} : ℝ≥0∞)
Tactic: simp_rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀' hs, hfg']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} : ℝ≥0∞)
have this₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((μ.restrict s : (a : Set α) → ℝ≥0∞) ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
    ℝ≥0∞)
Tactic: rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀' hs, ←
    measure_diff_null (measure_eq_top_of_lintegral_ne_top hg.aemeasurable hint)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} : ℝ≥0∞)
have inr : Subset.{u_1} (α := Set α) ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞})
  {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a}
Tactic: refine this.trans_le (measure_mono ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x : α | g x = ∞}
⊢ Membership.mem (γ := Set α) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} x
have inr : ∀ (hfx : ⨍⁻ (x : α) in s, g x ∂μ ≤ g x) (hx : x ∉ {x : α | g x = ∞}),
  Membership.mem (γ := Set α) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} x
Tactic: rw [← toReal_laverage hg.aemeasurable, toReal_le_toReal (setLAverage_lt_top hint).ne hx] at hfx
Cleared hypotheses: hfx, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x : α | g x = ∞}
inr :
  ∀ (hfx : ⨍⁻ (x : α) in s, g x ∂μ ≤ g x) (hx : x ∉ {x : α | g x = ∞}),
    Membership.mem (γ := Set α) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} x
⊢ Membership.mem (γ := Set α) {a : α | ⨍⁻ (a : α) in s, g a ∂μ ≤ f a} x
have inr₁ : ∀ᵐ (x : α) ∂μ.restrict s, g x ≠ ∞
Tactic: rw [← toReal_laverage hg.aemeasurable, toReal_le_toReal (setLAverage_lt_top hint).ne hx] at hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : NullMeasurableSet s μ
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
g : α → ℝ≥0∞
hint : ∫⁻ (a : α) in s, g a ∂μ ≠ ∞
hg : Measurable g
hgf : g ≤ f
hfg : ∫⁻ (a : α) in s, f a ∂μ = ∫⁻ (a : α) in s, g a ∂μ
hfg' : ⨍⁻ (a : α) in s, f a ∂μ = ⨍⁻ (a : α) in s, g a ∂μ
this :
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ.restrict s : (a : Set α) → ℝ≥0∞)
        ({a : α | ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g a).toReal} \ {x : α | g x = ∞}) :
      ℝ≥0∞)
x : α
hfx : ⨍ (a : α) in s, (g a).toReal ∂μ ≤ (g x).toReal
hx : x ∉ {x : α | g x = ∞}
⊢ ∀ᵐ (x : α) ∂μ.restrict s, g x ≠ ∞
have inr : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | g a = ∞} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [ae_iff, not_ne_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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∞)
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
have this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} : ℝ≥0∞)
Tactic: have := measure_laverage_le_pos hμ hint
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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} : ℝ≥0∞)
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
have this₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N) : ℝ≥0∞)
Tactic: rw [← measure_diff_null hN] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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 ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
have obtain : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | ⨍⁻ (a : α), f a ∂μ ≤ f x} x) (hxN : x ∉ N),
  ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x
Tactic: obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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∞)
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
have this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} : ℝ≥0∞)
Tactic: have := measure_le_laverage_pos hμ hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
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∞)
⊢ ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
have this₁ : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} \ N) : ℝ≥0∞)
Tactic: rw [← measure_diff_null hN] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
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 ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
have obtain : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | f x ≤ ⨍⁻ (a : α), f a ∂μ} x) (hxN : x ∉ N),
  ∃ x ∉ N, f x ≤ ⨍⁻ (a : α), f a ∂μ
Tactic: obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'
-- 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)
⊢ ∀ᶠ (i : ι) in l, Integrable (g i) μ
have h : ∀ (i : ι) (hi : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)), Integrable (g i) μ
Tactic: filter_upwards [(tendsto_order.1 hg).1 _ zero_lt_one] with i hi
-- 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)
i : ι
hi : LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
⊢ Integrable (g i) μ
have h : ∀ (hi : ¬Integrable (g i) μ), ¬LT.lt (α := ℝ) 0 (∫ (y : α), g i y ∂μ)
Tactic: contrapose hi
Cleared hypotheses: hi
-- 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)
⊢ Tendsto (fun (i : ι) ↦ ∫ (y : α), g i y • f y ∂μ) l (𝓝 c)
have g_int : ∀ᶠ (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]
-- 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 : ι) in l,
    ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
have 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 ∂μ
Tactic: filter_upwards [f_int, g_int, g_supp, g_bound] with i hif hig hisupp hibound
-- 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 : ι
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 ∂μ
have h : Eq.{u_2 + 1} (α := E) (∫ (a : α), g i a • (f a - c) + g i a • c ∂μ) (∫ (y : α), g i y • f y ∂μ)
Tactic: rw [← integral_smul_const, ← integral_add]
-- 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 : ι
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 ∂μ)
⊢ ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
have h₁ : Integrable.{u_2, u_1} (ε := E) (fun (y : α) ↦ g i y • (f y - c)) μ
Tactic: rw [← integral_smul_const, ← integral_add]
-- 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 : ι
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)) μ
⊢ ∫ (y : α), g i y • (f y - c) ∂μ + HSMul.hSMul (α := ℝ) (∫ (y : α), g i y ∂μ) c = ∫ (y : α), g i y • f y ∂μ
have h₂ : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ g i x • c) μ
Tactic: rw [← integral_smul_const, ← integral_add]