awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
rw : Integrable (f ∘ Neg.neg) (μ.restrict (Ici 0))
⊢ IntegrableOn f (Iic 0) μ

Tactic:
rw [IntegrableOn, ← h_map_neg, measurableEmbedding_neg.integrable_map_iff]

Premises used: MeasureTheory.IntegrableOn, MeasurableEmbedding.integrable_map_iff, measurableEmbedding_neg
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ Integrable (f ∘ Neg.neg) (μ.restrict (Ici 0))

Tactic:
h_int.congr' ?_ hsymm.restrict

Premises used: Filter.EventuallyEq.restrict, MeasureTheory.Integrable.congr'
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
refine : AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici 0))
⊢ Integrable (f ∘ Neg.neg) (μ.restrict (Ici 0))

Tactic:
refine h_int.congr' ?_ hsymm.restrict

Premises used: Filter.EventuallyEq.restrict, MeasureTheory.Integrable.congr'
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici 0))

Tactic:
AEStronglyMeasurable.comp_aemeasurable ?_ measurable_neg.aemeasurable

Premises used: Measurable.aemeasurable, MeasurableNeg.measurable_neg, MeasureTheory.AEStronglyMeasurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
refine : AEStronglyMeasurable (m₀ := inst_3) f (Measure.map Neg.neg (μ.restrict (Ici 0)))
⊢ AEStronglyMeasurable (f ∘ Neg.neg) (μ.restrict (Ici 0))

Tactic:
refine AEStronglyMeasurable.comp_aemeasurable ?_ measurable_neg.aemeasurable

Premises used: Measurable.aemeasurable, MeasurableNeg.measurable_neg, MeasureTheory.AEStronglyMeasurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ AEStronglyMeasurable (m₀ := inst_3) f (Measure.map Neg.neg (μ.restrict (Ici 0)))

Tactic:
h_map_neg ▸ hf.aestronglyMeasurable.restrict

Premises used: Eq.rec, MeasureTheory.AEStronglyMeasurable.restrict, Eq.symm, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : AddCommGroup α
inst_6 : LinearOrder α
inst_7 : IsOrderedAddMonoid α
inst_8 : CompactIccSpace α
inst_9 : IsMeasurablyGenerated.{u_1} (α := α) atTop
inst_10 : MeasurableNeg α
inst_11 : μ.IsNegInvariant
hf : LocallyIntegrable f μ
hsymm : norm ∘ f =ᶠ[ae μ] norm ∘ f ∘ Neg.neg
ho : f =O[atTop] g
hg : IntegrableAtFilter g atTop μ
h_int : IntegrableOn f (Ici 0) μ
h_map_neg : Measure.map Neg.neg (μ.restrict (Ici 0)) = μ.restrict (Iic 0)
⊢ AEStronglyMeasurable (m₀ := inst_3) f (Measure.map Neg.neg (μ.restrict (Ici 0)))

Tactic:
exact h_map_neg ▸ hf.aestronglyMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
rw : ∫⁻ (x : α), 0 ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ ⨍⁻ (_x : α), 0 ∂μ = 0

Tactic:
rw [laverage, lintegral_zero]

Premises used: MeasureTheory.laverage, MeasureTheory.lintegral_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂0 = 0

Tactic:
simp [laverage]

Premises used: MeasureTheory.laverage
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
⊢ ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ

Tactic:
rfl

Premises used: MeasureTheory.laverage, rfl
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ)
rw₃ rw₄ :
  HMul.hMul (α := ℝ≥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∞)

Tactic:
rw [laverage_eq', lintegral_smul_measure, ENNReal.div_eq_inv_mul, smul_eq_mul]

Premises used: MeasureTheory.lintegral_smul_measure, MeasureTheory.laverage_eq', smul_eq_mul, ENNReal.div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ
rw₃ rw₄ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
⊢ ⨍⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ

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

Premises used: MeasureTheory.laverage, inv_one, MeasureTheory.IsProbabilityMeasure.measure_univ, one_smul
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ
inr :
  ∀ (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 ∂μ

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

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.Average
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
inl₃ inl₄ : Eq (α := ℝ≥0∞) 0 0
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [hμ, lintegral_zero_measure, laverage_zero_measure, mul_zero]

Premises used: MeasureTheory.laverage_zero_measure, MulZeroClass.mul_zero, MeasureTheory.lintegral_zero_measure
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ
inr₁ inr₂ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), f x ∂μ
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (⨍⁻ (x : α), f x ∂μ) = ∫⁻ (x : α), f x ∂μ

Tactic:
rw [laverage_eq, ENNReal.mul_div_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.mul_div_cancel
-- Module: Mathlib.MeasureTheory.Integral.Average
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∞)
rw₁ 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∞)
⊢ ⨍⁻ (x : α) in s, f x ∂μ = HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α) in s, f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [laverage_eq, restrict_apply_univ]

Premises used: MeasureTheory.laverage_eq, MeasureTheory.Measure.restrict_apply_univ
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
s : Set α
⊢ ⨍⁻ (x : α) in s, f x ∂μ =
    ∫⁻ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)

Tactic:
simp only [laverage_eq', restrict_apply_univ]

Premises used: MeasureTheory.laverage_eq', MeasureTheory.Measure.restrict_apply_univ
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
⊢ ⨍⁻ (x : α), f x ∂μ = ⨍⁻ (x : α), g x ∂μ

Tactic:
simp only [laverage_eq, lintegral_congr_ae h]

Premises used: MeasureTheory.laverage_eq, MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
f : α → ℝ≥0∞
h : s =ᶠ[ae μ] t
⊢ ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in t, f x ∂μ

Tactic:
simp only [setLAverage_eq, setLIntegral_congr h, measure_congr h]

Premises used: MeasureTheory.measure_congr, MeasureTheory.setLAverage_eq, MeasureTheory.setLIntegral_congr
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hs : MeasurableSet s
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = g x
⊢ ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in s, g x ∂μ

Tactic:
simp only [laverage_eq, setLIntegral_congr_fun_ae hs h]

Premises used: MeasureTheory.laverage_eq, MeasureTheory.setLIntegral_congr_fun_ae
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f g : α → ℝ≥0∞
hs : MeasurableSet s
h : EqOn f g s
⊢ ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in s, g x ∂μ

Tactic:
simp only [laverage_eq, setLIntegral_congr_fun hs h]

Premises used: MeasureTheory.laverage_eq, MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
inl : ∀ (hf : ∫⁻ (x : α), f x ∂0 ≠ ∞), ⨍⁻ (x : α), f x ∂0 < ∞
inr : ∀ (hμ : μ ≠ 0), ⨍⁻ (x : α), f x ∂μ < ∞
⊢ ⨍⁻ (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∞
hf : ∫⁻ (x : α), f x ∂0 ≠ ∞
⊢ ⨍⁻ (x : α), f x ∂0 < ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hμ : μ ≠ 0
inr : HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
⊢ ⨍⁻ (x : α), f x ∂μ < ∞

Tactic:
rw [laverage_eq]

Premises used: MeasureTheory.laverage_eq
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ∞
hμ : μ ≠ 0
inr inr₁ inr₂ inr₃ :
  Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) →
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞
⊢ HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), f x ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) < ∞

Tactic:
finiteness [measure_univ_ne_zero.2 hμ]

Premises used: Iff.mpr, MeasureTheory.Measure.measure_univ_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
⊢ ∫⁻ (x : α) in s, f x ∂μ ≠ ∞ → ⨍⁻ (x : α) in s, f x ∂μ < ∞

Tactic:
laverage_lt_top

Premises used: MeasureTheory.laverage_lt_top
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂ν
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 ∂ν
⊢ ⨍⁻ (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 μ

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : ¬IsFiniteMeasure μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [not_isFiniteMeasure_iff] at hμ

Premises used: MeasureTheory.not_isFiniteMeasure_iff
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥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 ∂ν

Tactic:
simp [laverage_eq, hμ]

Premises used: MeasureTheory.laverage_eq
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂ν
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 ∂ν
⊢ ⨍⁻ (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 ν

Premises used: MeasureTheory.IsFiniteMeasure
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : ¬IsFiniteMeasure ν
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [not_isFiniteMeasure_iff] at hν

Premises used: MeasureTheory.not_isFiniteMeasure_iff
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
f : α → ℝ≥0∞
hμ : IsFiniteMeasure μ
hν : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥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 ∂ν

Tactic:
simp [laverage_eq, hν]

Premises used: MeasureTheory.laverage_eq
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂ν

Tactic:
simp only [← ENNReal.mul_div_right_comm, measure_mul_laverage, ← ENNReal.add_div,
    ← lintegral_add_measure, ← Measure.add_apply, ← laverage_eq]

Premises used: MeasureTheory.lintegral_add_measure, ENNReal.mul_div_right_comm, MeasureTheory.laverage_eq, MeasureTheory.Measure.add_apply, MeasureTheory.measure_mul_laverage, ENNReal.add_div
-- Module: Mathlib.MeasureTheory.Integral.Average
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have := Fact.mk h.lt_top
-- Module: Mathlib.MeasureTheory.Integral.Average
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 ∂μ)
rw₁ 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 ∂μ)
⊢ HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (⨍⁻ (x : α) in s, f x ∂μ) = ∫⁻ (x : α) in s, f x ∂μ

Tactic:
rw [← measure_mul_laverage, restrict_apply_univ]

Premises used: MeasureTheory.Measure.restrict_apply_univ, MeasureTheory.measure_mul_laverage