awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ)

Tactic:
⟨μ 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⟩

Premises used: Iff.mpr, Set.Mem, setOf, HDiv.hDiv, HAdd.hAdd, MeasureTheory.laverage_union, And.intro, Exists.intro, ENNReal.div_pos, openSegment, ENNReal.add_ne_top, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Average
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∞)
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
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in t, f x ∂μ)

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⟩
-- Module: Mathlib.MeasureTheory.Integral.Average
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
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 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

Tactic:
rw [← ENNReal.add_div,
    ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]

Premises used: Iff.mpr, Iff.not, ENNReal.add_div, ENNReal.div_self, And.left, And.intro, add_eq_zero, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ]
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 ∂μ]
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]

Tactic:
by_cases hs₀ : μ s = 0

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Average
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∞)
⊢ s =ᶠ[ae μ] ∅

Tactic:
rw [← ae_eq_empty] at hs₀

Premises used: MeasureTheory.ae_eq_empty
-- Module: Mathlib.MeasureTheory.Integral.Average
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 μ] ∅
pos : ⨍⁻ (x : α) in 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 ∂μ]

Tactic:
rw [restrict_congr_set (hs₀.union EventuallyEq.rfl), empty_union]

Premises used: MeasureTheory.Measure.restrict_congr_set, Set.empty_union, Filter.EventuallyEq.union, Filter.EventuallyEq.rfl
-- Module: Mathlib.MeasureTheory.Integral.Average
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 t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]

Tactic:
right_mem_segment _ _ _

Premises used: Set.Mem, right_mem_segment
-- Module: Mathlib.MeasureTheory.Integral.Average
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 t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]

Tactic:
exact right_mem_segment _ _ _

Premises used: right_mem_segment
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ]

Tactic:
⟨μ s / (μ s + μ t), μ t / (μ s + μ t), zero_le, zero_le, ?_, (laverage_union hd ht).symm⟩

Premises used: zero_le, Set.Mem, setOf, HDiv.hDiv, segment, HAdd.hAdd, MeasureTheory.laverage_union, And.intro, Exists.intro, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Average
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 :
  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
⊢ ⨍⁻ (x : α) in s ∪ t, f x ∂μ ∈ [⨍⁻ (x : α) in s, f x ∂μ -[ℝ≥0∞] ⨍⁻ (x : α) in t, f x ∂μ]

Tactic:
refine
      ⟨μ s / (μ s + μ t), μ t / (μ s + μ t), zero_le, zero_le, ?_, (laverage_union hd ht).symm⟩
-- Module: Mathlib.MeasureTheory.Integral.Average
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
neg₁ neg₂ : Eq (α := ℝ≥0∞) 1 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

Tactic:
rw [← ENNReal.add_div,
      ENNReal.div_self (add_eq_zero.not.2 fun h => hs₀ h.1) (add_ne_top.2 ⟨hsμ, htμ⟩)]

Premises used: Iff.mpr, Iff.not, ENNReal.add_div, ENNReal.div_self, And.left, And.intro, add_eq_zero, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
inst : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsc₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ⨍⁻ (x : α), f x ∂μ ∈ openSegment ℝ≥0∞ (⨍⁻ (x : α) in s, f x ∂μ) (⨍⁻ (x : α) in sᶜ, f x ∂μ)

Tactic:
simpa only [union_compl_self, restrict_univ] using
    laverage_union_mem_openSegment aedisjoint_compl_right hs.compl hs₀ hsc₀ (measure_ne_top _ _)
      (measure_ne_top _ _)

Premises used: MeasureTheory.aedisjoint_compl_right, MeasureTheory.NullMeasurableSet.compl, MeasureTheory.measure_ne_top, Set.union_compl_self, MeasureTheory.laverage_union_mem_openSegment, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
h : NeZero μ
c : ℝ≥0∞
⊢ ⨍⁻ (_x : α), c ∂μ = c

Tactic:
simp only [laverage, lintegral_const, measure_univ, mul_one]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.laverage, MeasureTheory.IsProbabilityMeasure.measure_univ, mul_one
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
c : ℝ≥0∞
⊢ ⨍⁻ (_x : α) in s, c ∂μ = c

Tactic:
simp only [setLAverage_eq, lintegral_const, Measure.restrict_apply, MeasurableSet.univ,
    univ_inter, div_eq_mul_inv, mul_assoc, ENNReal.mul_inv_cancel hs₀ hs, mul_one]

Premises used: MeasureTheory.lintegral_const, mul_assoc, MeasureTheory.Measure.restrict_apply, Set.univ_inter, div_eq_mul_inv, ENNReal.mul_inv_cancel, MeasureTheory.setLAverage_eq, mul_one, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
inst_1 : NeZero μ
⊢ ⨍⁻ (_x : α), 1 ∂μ = 1

Tactic:
laverage_const _ _

Premises used: MeasureTheory.laverage_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ⨍⁻ (_x : α) in s, 1 ∂μ = 1

Tactic:
setLAverage_const hs₀ hs _

Premises used: MeasureTheory.setLAverage_const
-- Module: Mathlib.MeasureTheory.Integral.Average
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
inr :
  ∀ (hμ : μ ≠ 0), HMul.hMul (β := ℝ≥0∞) (⨍⁻ (a : α), f a ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = ∫⁻ (x : α), f x ∂μ
⊢ HMul.hMul (β := ℝ≥0∞) (⨍⁻ (a : α), f a ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) = ∫⁻ (x : α), f x ∂μ

Tactic:
obtain rfl | hμ := eq_or_ne μ 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
inst : 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:
simp
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ
inr₁ inr₂ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
⊢ HMul.hMul (β := ℝ≥0∞) (⨍⁻ (a : α), f a ∂μ) ((μ : (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 _ _)]

Premises used: Iff.mpr, MeasureTheory.Measure.measure_univ_ne_zero, MeasureTheory.measure_ne_top, MeasureTheory.laverage_eq, ENNReal.div_mul_cancel
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
⊢ ∫⁻ (_x : α), ⨍⁻ (a : α), f a ∂μ ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
f : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (_x : α) in s, ⨍⁻ (a : α) in s, f a ∂μ ∂μ = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
lintegral_laverage _ _

Premises used: MeasureTheory.lintegral_laverage
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ ⨍⁻ (a : α), f a ∂μ ≤ ⨍⁻ (a : α), g a ∂μ

Tactic:
lintegral_mono_ae <| h.filter_mono <| Measure.ae_mono' Measure.smul_absolutelyContinuous

Premises used: Filter.Eventually.filter_mono, MeasureTheory.laverage, MeasureTheory.lintegral_mono_ae, MeasureTheory.Measure.smul_absolutelyContinuous, MeasureTheory.Measure.ae_mono'
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
s : Set α
h : ∀ᵐ (a : α) ∂μ, f a ≤ g a
⊢ ⨍⁻ (a : α) in s, f a ∂μ ≤ ⨍⁻ (a : α) in s, g a ∂μ

Tactic:
laverage_mono_ae <| h.filter_mono <| ae_mono Measure.restrict_le_self

Premises used: Filter.Eventually.filter_mono, MeasureTheory.ae_mono, MeasureTheory.Measure.restrict_le_self, MeasureTheory.laverage_mono_ae
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
pos : ∀ (hμ : IsFiniteMeasure (μ.restrict s)), ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
neg : ∀ (hμ : ¬IsFiniteMeasure (μ.restrict s)), ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

Tactic:
by_cases hμ : IsFiniteMeasure (μ.restrict s)

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure (μ.restrict s)
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

Tactic:
simp [laverage, not_isFiniteMeasure_iff.mp hμ]

Premises used: MeasureTheory.laverage, MeasureTheory.not_isFiniteMeasure_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.Average
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 μ
neg : ∀ (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 μ

Tactic:
by_cases hμ0 : μ s = 0

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.Average
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∞)
pos :
  ∫⁻ (x : α) in univ,
      f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ.restrict s : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.restrict s) ≤
    essSup f μ
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

Tactic:
rw [laverage, ← setLIntegral_univ]

Premises used: MeasureTheory.laverage, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.Integral.Average
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∞)
⊢ Eq (α := ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (((μ.restrict s : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set α) → ℝ≥0∞)
        univ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp [hμ0]
-- Module: Mathlib.MeasureTheory.Integral.Average
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 univ,
      f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ.restrict s : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (μ.restrict s) ≤
    essSup f μ

Tactic:
exact le_of_eq_of_le (setLIntegral_measure_zero univ f <| by simp [hμ0]) zero_le

Premises used: zero_le, Set.univ, le_of_eq_of_le, MeasureTheory.setLIntegral_measure_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
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∞)
neg : ⨍⁻ (a : α) in s, essSup f μ ∂μ = essSup f μ
⊢ ⨍⁻ (x : α) in s, f x ∂μ ≤ essSup f μ

Tactic:
apply le_of_le_of_eq (laverage_mono_ae <| Eventually.filter_mono ae_restrict_le ae_le_essSup)

Premises used: Filter.Eventually.filter_mono, le_of_le_of_eq, ae_le_essSup, MeasureTheory.ae_restrict_le, MeasureTheory.laverage_mono_ae
-- Module: Mathlib.MeasureTheory.Integral.Average
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∞)
⊢ NeZero (μ.restrict s)

Tactic:
have : NeZero (μ.restrict s) :=
    have : NeZero (μ s) := { out := hμ0 }
    restrict.neZero
-- Module: Mathlib.MeasureTheory.Integral.Average
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∞)
this : NeZero (μ.restrict s)
⊢ ⨍⁻ (a : α) in s, essSup f μ ∂μ = essSup f μ

Tactic:
laverage_const (μ.restrict s) _

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.laverage_const
-- Module: Mathlib.MeasureTheory.Integral.Average
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∞)
this : NeZero (μ.restrict s)
⊢ ⨍⁻ (a : α) in s, essSup f μ ∂μ = essSup f μ

Tactic:
exact laverage_const (μ.restrict s) _

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.laverage_const
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ ≤ essSup f μ

Tactic:
simpa using setLAverage_le_essSup univ f

Premises used: Set.univ, MeasureTheory.setLAverage_le_essSup
-- Module: Mathlib.MeasureTheory.Integral.Average
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
rw₁ rw₂ : Eq.{u_2 + 1} (α := E) 0 0
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), 0 ∂μ) 0

Tactic:
rw [average, integral_zero]

Premises used: MeasureTheory.average, MeasureTheory.integral_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
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
rw₂ rw₃ : Eq.{u_2 + 1} (α := E) 0 0
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂0) 0

Tactic:
rw [average, smul_zero, integral_zero_measure]

Premises used: smul_zero, MeasureTheory.average, MeasureTheory.integral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), -f x ∂μ) (-⨍ (x : α), f x ∂μ)

Tactic:
integral_neg f

Premises used: MeasureTheory.integral_neg, MeasureTheory.average
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂μ)
    (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)

Tactic:
rfl

Premises used: MeasureTheory.average, rfl
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ)
rw₃ 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 ∂μ)
⊢ ⨍ (x : α), f x ∂μ = HSMul.hSMul (β := E) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)

Tactic:
rw [average_eq', integral_smul_measure, ENNReal.toReal_inv, measureReal_def]

Premises used: ENNReal.toReal_inv, MeasureTheory.average_eq', MeasureTheory.measureReal_def, MeasureTheory.integral_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ)
rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) 1⁻¹ μ) (∫ (x : α), f x ∂μ)
rw₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) 1 μ) (∫ (x : α), f x ∂μ)
rw₃ rw₄ : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ)

Tactic:
rw [average, measure_univ, inv_one, one_smul]

Premises used: inv_one, MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.average, one_smul
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : IsFiniteMeasure μ
f : α → E
inl : ∀ (hμ : μ = 0), HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
inr : ∀ (hμ : μ ≠ 0), HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ

Tactic:
rcases eq_or_ne μ 0 with hμ | hμ

Premises used: eq_or_ne, OfNat.ofNat