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 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 ∂μ
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 ∂μ
⊢ ⨍⁻ (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∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥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∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥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]
-- 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 μ
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)
have s₁ : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) +
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) =
  1
Tactic: refine
    ⟨μ s / (μ s + μ t), μ t / (μ s + μ t), ENNReal.div_pos hs₀ <| add_ne_top.2 ⟨hsμ, htμ⟩,
      ENNReal.div_pos ht₀ <| add_ne_top.2 ⟨hsμ, htμ⟩, ?_, (laverage_union hd ht).symm⟩
-- 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 μ
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) =
    1
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) /
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
  1
Tactic: rw [← ENNReal.add_div,
    ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]
-- 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 μ
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) /
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    1
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) =
    1
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← ENNReal.add_div,
    ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]
-- 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 μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
have pos : ∀ (hs₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
Tactic: by_cases hs₀ : μ s = 0
-- 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 μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
pos :
  ∀ (hs₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
have neg : ∀ (hs₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
Tactic: by_cases hs₀ : μ s = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
hd : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
have hs₁ : s =ᶠ[ae μ] ∅
Tactic: rw [← ae_eq_empty] at hs₀
Cleared hypotheses: hs₀
-- 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 μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₀ : s =ᶠ[ae μ] ∅
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
have pos : ⨍⁻ (x : α) in t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
Tactic: rw [restrict_congr_set (hs₀.union EventuallyEq.rfl), empty_union]
-- 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 μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]
have neg : HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) +
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) =
  1
Tactic: refine
      ⟨μ s / (μ s + μ t), μ t / (μ s + μ t), zero_le, zero_le, ?_, (laverage_union hd ht).symm⟩
-- 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 μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) =
    1
have neg : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) /
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
  1
Tactic: rw [← ENNReal.add_div,
      ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]
-- 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 μ
hsμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
htμ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs₀ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) /
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    1
⊢ HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) +
      HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)) =
    1
have neg₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← ENNReal.add_div,
      ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]
-- 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 : α), f a ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = ∫⁻ (x : α), f x ∂μ
have inl : ∀ [IsFiniteMeasure.{u_1} (α := α) (m0 := m0) 0],
  HMul.hMul (β := ℝ≥0∞) (⨍⁻ (a : α), f a ∂0) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = ∫⁻ (x : α), f x ∂0
Tactic: obtain rfl | hμ := eq_or_ne μ 0
Cleared hypotheses: μ, inst
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
inl :
  ∀ [IsFiniteMeasure.{u_1} (α := α) (m0 := m0) 0],
    HMul.hMul (β := ℝ≥0∞) (⨍⁻ (a : α), f a ∂0) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = ∫⁻ (x : α), f x ∂0
⊢ HMul.hMul (β := ℝ≥0∞) (⨍⁻ (a : α), f a ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = ∫⁻ (x : α), f x ∂μ
have inr : ∀ (hμ : μ ≠ 0), HMul.hMul (β := ℝ≥0∞) (⨍⁻ (a : α), f a ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥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 α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
hμ : μ ≠ 0
⊢ HMul.hMul (β := ℝ≥0∞) (⨍⁻ (a : α), f a ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = ∫⁻ (x : α), f x ∂μ
have inr : HMul.hMul (β := ℝ≥0∞) (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞))
    ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
  ∫⁻ (x : α), f x ∂μ
Tactic: rw [laverage_eq, ENNReal.div_mul_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∞) (HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞))
      ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) =
    ∫⁻ (x : α), f x ∂μ
⊢ HMul.hMul (β := ℝ≥0∞) (⨍⁻ (a : α), f a ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = ∫⁻ (x : α), f x ∂μ
have inr₁ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
Tactic: rw [laverage_eq, ENNReal.div_mul_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 α
s : Set α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
have pos : ∀ (hμ : IsFiniteMeasure (μ.restrict s)), ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
Tactic: by_cases hμ : IsFiniteMeasure (μ.restrict s)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
pos : ∀ (hμ : IsFiniteMeasure (μ.restrict s)), ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
have neg : ∀ (hμ : ¬IsFiniteMeasure (μ.restrict s)), ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
Tactic: by_cases hμ : IsFiniteMeasure (μ.restrict s)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
have pos : ∀ (hμ0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
Tactic: by_cases hμ0 : μ s = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
pos : ∀ (hμ0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
have neg : ∀ (hμ0 : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)), ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
Tactic: by_cases hμ0 : μ s = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
hμ0 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
have pos : ∫⁻ (x : α) in univ, f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ.restrict s : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.restrict s) ≤
  essSup f μ
Tactic: rw [laverage, ← setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
hμ0 : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
have neg : ⨍⁻ (a : α) in s, essSup f μ ∂μ = essSup f μ
Tactic: apply le_of_le_of_eq (laverage_mono_ae <| Eventually.filter_mono ae_restrict_le ae_le_essSup)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure (μ.restrict s)
hμ0 : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ⨍⁻ (a : α) in s, essSup f μ ∂μ = essSup f μ
have this : NeZero (μ.restrict s)
Tactic: have : NeZero (μ.restrict s) :=
    have : NeZero (μ s) := { out := hμ0 }
    restrict.neZero
-- 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 α
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), 0 ∂μ) 0
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : α), 0 ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ) 0
Tactic: rw [average, integral_zero]
-- 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 α
rw : Eq.{u_2 + 1} (α := E) (∫ (x : α), 0 ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ) 0
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), 0 ∂μ) 0
have rw₁ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [average, integral_zero]
-- 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
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂0) 0
have rw : Eq.{u_2 + 1} (α := E)
  (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
  0
Tactic: rw [average, smul_zero, integral_zero_measure]
-- 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
f : α → E
rw :
  Eq.{u_2 + 1} (α := E)
    (∫ (x : α),
      f x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
    0
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂0) 0
have rw₁ : Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ m0 0 fun (x : α) ↦ f x) 0
Tactic: rw [average, smul_zero, integral_zero_measure]
-- 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
f : α → E
rw :
  Eq.{u_2 + 1} (α := E)
    (∫ (x : α),
      f x ∂HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
    0
rw₁ : Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ m0 0 fun (x : α) ↦ f x) 0
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂0) 0
have rw₂ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [average, smul_zero, integral_zero_measure]
-- 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 α
f : α → E
⊢ ⨍ (x : α), f x ∂μ = HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
have rw : ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ =
  HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
Tactic: rw [average_eq', integral_smul_measure, ENNReal.toReal_inv, measureReal_def]
-- 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 α
f : α → E
rw :
  ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ =
    HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
⊢ ⨍ (x : α), f x ∂μ = HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
have rw₁ : HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹) (∫ (x : α), f x ∂μ) =
  HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
Tactic: rw [average_eq', integral_smul_measure, ENNReal.toReal_inv, measureReal_def]
-- 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 α
f : α → E
rw :
  ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ =
    HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
rw₁ :
  HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹) (∫ (x : α), f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
⊢ ⨍ (x : α), f x ∂μ = HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
have rw₂ : HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ (∫ (x : α), f x ∂μ) =
  HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
Tactic: rw [average_eq', integral_smul_measure, ENNReal.toReal_inv, measureReal_def]
-- 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 α
f : α → E
rw :
  ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ =
    HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
rw₁ :
  HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹) (∫ (x : α), f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
rw₂ :
  HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ (∫ (x : α), f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
⊢ ⨍ (x : α), f x ∂μ = HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)
have rw₃ : HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ (∫ (x : α), f x ∂μ) =
  HSMul.hSMul (β := E) (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ (∫ (x : α), f x ∂μ)
Tactic: rw [average_eq', integral_smul_measure, ENNReal.toReal_inv, measureReal_def]
-- 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 : IsProbabilityMeasure μ
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ)
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
  (∫ (x : α), f x ∂μ)
Tactic: rw [average, measure_univ, inv_one, one_smul]
-- 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 : IsProbabilityMeasure μ
f : α → E
rw :
  Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
    (∫ (x : α), f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ)
have rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) 1⁻¹ μ) (∫ (x : α), f x ∂μ)
Tactic: rw [average, measure_univ, inv_one, one_smul]