awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
inr :
  ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₁ :
  ENNReal.ofReal ((μ.real univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₂ :
  ENNReal.ofReal ((ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₃ :
  ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₄ :
  ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹) * ENNReal.ofReal (∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₅ :
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (ENNReal.ofReal (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₆ :
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr₇ : HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) =
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ)
Tactic: rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
⊢ (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
have rw : (⨍⁻ (x : α), f x ∂μ).toReal = HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
Tactic: rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
      integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2), measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
rw : (⨍⁻ (x : α), f x ∂μ).toReal = HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
⊢ (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
have rw₁ : (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
  HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
Tactic: rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
      integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2), measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
rw : (⨍⁻ (x : α), f x ∂μ).toReal = HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₁ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
⊢ (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
have rw₂ : (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
  (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
Tactic: rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
      integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2), measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
rw : (⨍⁻ (x : α), f x ∂μ).toReal = HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₁ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₂ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
⊢ (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
have rw₃ : (∫⁻ (x : α), f x ∂μ).toReal / ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) =
  (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
Tactic: rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
      integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2), measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
rw : (⨍⁻ (x : α), f x ∂μ).toReal = HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₁ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₂ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₃ :
  (∫⁻ (x : α), f x ∂μ).toReal / ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
⊢ (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
have rw₄ : (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * (∫⁻ (x : α), f x ∂μ).toReal =
  (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
Tactic: rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
      integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2), measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
rw : (⨍⁻ (x : α), f x ∂μ).toReal = HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₁ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₂ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₃ :
  (∫⁻ (x : α), f x ∂μ).toReal / ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₄ :
  (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * (∫⁻ (x : α), f x ∂μ).toReal =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
⊢ (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
have rw₅ : (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (a : α), (f a).toReal ∂μ =
  (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
Tactic: rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
      integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2), measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf' : ∀ᵐ (x : α) ∂μ, f x ≠ ∞
rw : (⨍⁻ (x : α), f x ∂μ).toReal = HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₁ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), (f x).toReal ∂μ)
rw₂ :
  (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)).toReal =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₃ :
  (∫⁻ (x : α), f x ∂μ).toReal / ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₄ :
  (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * (∫⁻ (x : α), f x ∂μ).toReal =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
rw₅ :
  (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (a : α), (f a).toReal ∂μ =
    (μ.real univ)⁻¹ * ∫ (x : α), (f x).toReal ∂μ
⊢ (⨍⁻ (x : α), f x ∂μ).toReal = ⨍ (x : α), (f x).toReal ∂μ
have rw₆ : (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (a : α), (f a).toReal ∂μ =
  (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (x : α), (f x).toReal ∂μ
Tactic: rw [average_eq, laverage_eq, smul_eq_mul, toReal_div, div_eq_inv_mul, ←
      integral_toReal hf (hf'.mono fun _ => lt_top_iff_ne_top.2), measureReal_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞)
have refine : ∀ (H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)),
  False
Tactic: refine pos_iff_ne_zero.2 fun H => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
have rwa : NullMeasurableSet {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} (μ.restrict s)
Tactic: rwa [restrict_apply₀, inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False
have H₁ : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: replace H : (μ.restrict s) {x | f x ≤ ⨍ a in s, f a ∂μ} = 0 := by
    rwa [restrict_apply₀, inter_comm]
    exact AEStronglyMeasurable.nullMeasurableSet_le hf.1 aestronglyMeasurable_const
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: haveI := Fact.mk hμ₁.lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ False
have refine : LT.lt (α := ℝ) 0 (∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ)
Tactic: refine (integral_sub_average (μ.restrict s) f).not_gt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ LT.lt (α := ℝ) 0 (∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ)
have refine_1 : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ
Tactic: refine (setIntegral_pos_iff_support_of_nonneg_ae ?_ ?_).2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
refine_1 : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ)
have refine_2 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) s μ
Tactic: refine (setIntegral_pos_iff_support_of_nonneg_ae ?_ ?_).2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
refine_1 : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ
refine_2 : IntegrableOn (ε := ℝ) (fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) s μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : α) in s, f x - ⨍ (a : α) in s, f a ∂μ ∂μ)
have refine_3 : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) ((support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) ∩ s) : ℝ≥0∞)
Tactic: refine (setIntegral_pos_iff_support_of_nonneg_ae ?_ ?_).2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ
have refine_1 : ∀ (x : α)
  (hx :
    Membership.mem (γ := Set α)
      {x : α | (fun (x : α) ↦ LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) x)) x}ᶜ x),
  Membership.mem (γ := Set α) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} x
Tactic: refine measure_mono_null (fun x hx ↦ ?_) H
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
x : α
hx :
  Membership.mem (γ := Set α)
    {x : α | (fun (x : α) ↦ LE.le (α := ℝ) (0 x) ((fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) x)) x}ᶜ x
⊢ Membership.mem (γ := Set α) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} x
have hx₁ : f x < ⨍ (a : α) in s, f a ∂μ
Tactic: simp only [Pi.zero_apply, sub_nonneg, mem_compl_iff, mem_setOf_eq, not_le] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ) ∩ s) : ℝ≥0∞)
have refine_3 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rwa [pos_iff_ne_zero, inter_comm, ← diff_compl, ← diff_inter_self_eq_diff, measure_diff_null]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ
hμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : IntegrableOn f s μ
H : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} : ℝ≥0∞) (0 : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s) : ℝ≥0∞)
    (0 : ℝ≥0∞)
have refine_3 : (support (M := ℝ) fun (x : α) ↦ f x - ⨍ (a : α) in s, f a ∂μ)ᶜ ∩ s ⊆ {x : α | f x ≤ ⨍ (a : α) in s, f a ∂μ} ∩ s
Tactic: refine measure_mono_null ?_ (measure_inter_eq_zero_of_restrict H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable 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_average_pos hμ hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable 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 : α → ℝ
inst : IsFiniteMeasure μ
hμ : μ ≠ 0
hf : Integrable 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
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)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
have inl : ∀ (h : ∫⁻ (a : α) in s, f a ∂μ = ∞),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
Tactic: obtain h | h := eq_or_ne (∫⁻ a in s, f a ∂μ) ∞
-- 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)
inl :
  ∀ (h : ∫⁻ (a : α) in s, f a ∂μ = ∞),
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
have inr : ∀ (h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞),
  LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
Tactic: obtain h | h := eq_or_ne (∫⁻ a in s, f a ∂μ) ∞
-- 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∞)
hμ₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ∞
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
have this : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} : ℝ≥0∞)
Tactic: have := measure_le_setAverage_pos hμ hμ₁ (integrable_toReal_of_lintegral_ne_top hf h)
-- 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∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
have inr : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
Tactic: rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀
    (hf.aestronglyMeasurable.nullMeasurableSet_le aestronglyMeasurable_const)]
-- 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∞)
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∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | x ∈ s ∧ (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) {a : α | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ} : ℝ≥0∞)
have 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∞)
Tactic: rw [← setOf_inter_eq_sep, ← Measure.restrict_apply₀
    (hf.ennreal_toReal.aestronglyMeasurable.nullMeasurableSet_le aestronglyMeasurable_const),
    ← measure_diff_null (measure_eq_top_of_lintegral_ne_top hf h)] at this
Cleared hypotheses: this