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 : α → ℝ≥0∞
rw :
  ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ :
  HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (a : α), f a ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
rw₂ :
  HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (a : α), f a ∂μ) =
    HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), f x ∂μ)
⊢ ⨍⁻ (x : α), f x ∂μ = HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₃ : HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (a : α), f a ∂μ) =
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), f x ∂μ)
Tactic: rw [laverage_eq', lintegral_smul_measure, ENNReal.div_eq_inv_mul, smul_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
have rw : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = ∫⁻ (x : α), f x ∂μ
Tactic: rw [laverage, measure_univ, inv_one, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
f : α → ℝ≥0∞
rw : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = ∫⁻ (x : α), f x ∂μ
⊢ ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
have rw₁ : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) 1⁻¹ μ = ∫⁻ (x : α), f x ∂μ
Tactic: rw [laverage, measure_univ, inv_one, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
f : α → ℝ≥0∞
rw : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = ∫⁻ (x : α), f x ∂μ
rw₁ : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) 1⁻¹ μ = ∫⁻ (x : α), f x ∂μ
⊢ ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
have rw₂ : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) 1 μ = ∫⁻ (x : α), f x ∂μ
Tactic: rw [laverage, measure_univ, inv_one, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
f : α → ℝ≥0∞
rw : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = ∫⁻ (x : α), f x ∂μ
rw₁ : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) 1⁻¹ μ = ∫⁻ (x : α), f x ∂μ
rw₂ : ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) 1 μ = ∫⁻ (x : α), f x ∂μ
⊢ ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
have rw₃ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
Tactic: rw [laverage, measure_univ, inv_one, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
have inl : ∀ (hμ : μ = 0), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
Tactic: rcases eq_or_ne μ 0 with hμ | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
inl :
  ∀ (hμ : μ = 0), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
have inr : ∀ (hμ : μ ≠ 0), HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
Tactic: rcases eq_or_ne μ 0 with hμ | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ = 0
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
have inl : HMul.hMul (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂0) = ∫⁻ (x : α), f x ∂0
Tactic: rw [hμ, lintegral_zero_measure, laverage_zero_measure, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ = 0
inl :
  HMul.hMul (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂0) = ∫⁻ (x : α), f x ∂0
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
have inl₁ : HMul.hMul (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂0) = 0
Tactic: rw [hμ, lintegral_zero_measure, laverage_zero_measure, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ = 0
inl :
  HMul.hMul (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂0) = ∫⁻ (x : α), f x ∂0
inl₁ : HMul.hMul (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂0) = 0
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
have inl₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) = 0
Tactic: rw [hμ, lintegral_zero_measure, laverage_zero_measure, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ = 0
inl :
  HMul.hMul (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂0) = ∫⁻ (x : α), f x ∂0
inl₁ : HMul.hMul (α := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂0) = 0
inl₂ : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) = 0
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
have inl₃ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [hμ, lintegral_zero_measure, laverage_zero_measure, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
have inr : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
    (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) =
  ∫⁻ (x : α), f x ∂μ
Tactic: rw [laverage_eq, ENNReal.mul_div_cancel (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
inr :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) =
    ∫⁻ (x : α), f x ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ
have inr₁ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
Tactic: rw [laverage_eq, ENNReal.mul_div_cancel (measure_univ_ne_zero.2 hμ) (measure_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ⨍⁻ (x : α) in s, f x ∂μ = HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, f x ∂μ) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [laverage_eq, restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
rw :
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, f x ∂μ) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ⨍⁻ (x : α) in s, f x ∂μ = HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [laverage_eq, restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ⨍⁻ (x : α), f x ∂μ < ∞
have inl : ∀ (hf : ∫⁻ (x : α), f x ∂0 ≠ ∞), ⨍⁻ (x : α), f x ∂0 < ∞
Tactic: obtain rfl | hμ := eq_or_ne μ 0
Cleared hypotheses: μ, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
inl : ∀ (hf : ∫⁻ (x : α), f x ∂0 ≠ ∞), ⨍⁻ (x : α), f x ∂0 < ∞
⊢ ⨍⁻ (x : α), f x ∂μ < ∞
have inr : ∀ (hμ : μ ≠ 0), ⨍⁻ (x : α), f x ∂μ < ∞
Tactic: obtain rfl | hμ := eq_or_ne μ 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hμ : μ ≠ 0
⊢ ⨍⁻ (x : α), f x ∂μ < ∞
have inr : HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
Tactic: rw [laverage_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hμ : μ ≠ 0
⊢ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
have inr : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) →
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
Tactic: finiteness [measure_univ_ne_zero.2 hμ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
have pos : ∀ (hμ : IsFiniteMeasure μ),
  ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
Tactic: by_cases hμ : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
pos :
  ∀ (hμ : IsFiniteMeasure μ),
    ⨍⁻ (x : α), f x ∂(μ + ν) =
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
              ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
          ⨍⁻ (x : α), f x ∂μ +
        HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
              ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
          ⨍⁻ (x : α), f x ∂ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
have neg : ∀ (hμ : ¬IsFiniteMeasure μ),
  ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
Tactic: by_cases hμ : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
have hμ₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [not_isFiniteMeasure_iff] at hμ
Cleared hypotheses: hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
have pos : ∀ (hν : IsFiniteMeasure ν),
  ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
Tactic: by_cases hν : IsFiniteMeasure ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
pos :
  ∀ (hν : IsFiniteMeasure ν),
    ⨍⁻ (x : α), f x ∂(μ + ν) =
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
              ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
          ⨍⁻ (x : α), f x ∂μ +
        HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
              ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
          ⨍⁻ (x : α), f x ∂ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
have neg : ∀ (hν : ¬IsFiniteMeasure ν),
  ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
Tactic: by_cases hν : IsFiniteMeasure ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ¬IsFiniteMeasure ν
⊢ ⨍⁻ (x : α), f x ∂(μ + ν) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
        ⨍⁻ (x : α), f x ∂ν
have hν₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [not_isFiniteMeasure_iff] at hν
Cleared hypotheses: hν
-- 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∞)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ) = ∫⁻ (x : α) in s, f x ∂μ
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have := 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 : α → ℝ≥0∞
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ) = ∫⁻ (x : α) in s, f x ∂μ
have rw : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ) =
  HMul.hMul (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ)
Tactic: rw [← measure_mul_laverage, restrict_apply_univ]
-- 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∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
rw :
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ) =
    HMul.hMul (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ) = ∫⁻ (x : α) in s, f x ∂μ
have rw₁ : HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ) =
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ)
Tactic: rw [← measure_mul_laverage, restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
        ⨍⁻ (x : α) in s, f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
        ⨍⁻ (x : α) in t, f x ∂μ
have rw : ⨍⁻ (x : α), f x ∂(μ.restrict s + μ.restrict t) =
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
      ⨍⁻ (x : α) in s, f x ∂μ +
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
      ⨍⁻ (x : α) in t, f x ∂μ
Tactic: rw [restrict_union₀ hd ht, laverage_add_measure, restrict_apply_univ, restrict_apply_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
rw :
  ⨍⁻ (x : α), f x ∂(μ.restrict s + μ.restrict t) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
        ⨍⁻ (x : α) in s, f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
        ⨍⁻ (x : α) in t, f x ∂μ
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
        ⨍⁻ (x : α) in s, f x ∂μ +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
          (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
        ⨍⁻ (x : α) in t, f x ∂μ
have rw₁ : HDiv.hDiv (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          ((μ.restrict t : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
      ⨍⁻ (x : α) in s, f x ∂μ +
    HDiv.hDiv (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
          ((μ.restrict t : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) *
      ⨍⁻ (x : α) in t, f x ∂μ =
  HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
      ⨍⁻ (x : α) in s, f x ∂μ +
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) *
      ⨍⁻ (x : α) in t, f x ∂μ
Tactic: rw [restrict_union₀ hd ht, laverage_add_measure, restrict_apply_univ, restrict_apply_univ]