awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (hypothesis)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
f : α → E
s t : Set α
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∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)
have hse₁ : s =ᶠ[ae μ] ∅
Tactic: rw [← ae_eq_empty] at hse
Cleared hypotheses: hse
-- 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
s t : Set α
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∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : s =ᶠ[ae μ] ∅
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)
have pos : Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in t, f x ∂μ)
Tactic: rw [restrict_congr_set (hse.union EventuallyEq.rfl), empty_union]
-- 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
s t : Set α
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∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hse : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)
have neg : 0 < μ.real s + μ.real t
Tactic: refine
      mem_segment_iff_div.mpr
        ⟨μ.real s, μ.real t, ENNReal.toReal_nonneg, ENNReal.toReal_nonneg, ?_,
          (average_union hd ht hsμ htμ hfs hft).symm⟩
-- 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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
h : NeZero μ
c : E
⊢ ⨍ (_x : α), c ∂μ = c
have rw : ∫ (x : α), c ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = c
Tactic: rw [average, integral_const, measureReal_def, measure_univ, ENNReal.toReal_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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
h : NeZero μ
c : E
rw : ∫ (x : α), c ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = c
⊢ ⨍ (_x : α), c ∂μ = c
have rw₁ : (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ).real univ • c = c
Tactic: rw [average, integral_const, measureReal_def, measure_univ, ENNReal.toReal_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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
h : NeZero μ
c : E
rw : ∫ (x : α), c ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = c
rw₁ : (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ).real univ • c = c
⊢ ⨍ (_x : α), c ∂μ = c
have rw₂ : ENNReal.toReal ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ : (a : Set α) → ℝ≥0∞) univ) • c =
  c
Tactic: rw [average, integral_const, measureReal_def, measure_univ, ENNReal.toReal_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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
h : NeZero μ
c : E
rw : ∫ (x : α), c ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = c
rw₁ : (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ).real univ • c = c
rw₂ :
  ENNReal.toReal ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ : (a : Set α) → ℝ≥0∞) univ) •
      c =
    c
⊢ ⨍ (_x : α), c ∂μ = c
have rw₃ : ENNReal.toReal 1 • c = c
Tactic: rw [average, integral_const, measureReal_def, measure_univ, ENNReal.toReal_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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
h : NeZero μ
c : E
rw : ∫ (x : α), c ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = c
rw₁ : (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ).real univ • c = c
rw₂ :
  ENNReal.toReal ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ : (a : Set α) → ℝ≥0∞) univ) •
      c =
    c
rw₃ : ENNReal.toReal 1 • c = c
⊢ ⨍ (_x : α), c ∂μ = c
have rw₄ : HSMul.hSMul (α := ℝ) 1 c = c
Tactic: rw [average, integral_const, measureReal_def, measure_univ, ENNReal.toReal_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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
h : NeZero μ
c : E
rw : ∫ (x : α), c ∂HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = c
rw₁ : (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ).real univ • c = c
rw₂ :
  ENNReal.toReal ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ : (a : Set α) → ℝ≥0∞) univ) •
      c =
    c
rw₃ : ENNReal.toReal 1 • c = c
rw₄ : HSMul.hSMul (α := ℝ) 1 c = c
⊢ ⨍ (_x : α), c ∂μ = c
have rw₅ : c = c
Tactic: rw [average, integral_const, measureReal_def, measure_univ, ENNReal.toReal_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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
have pos : ∀ (hf : Integrable f μ), Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
Tactic: by_cases hf : Integrable f μ
-- 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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
pos : ∀ (hf : Integrable f μ), Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
have neg : ∀ (hf : ¬Integrable f μ), Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
Tactic: by_cases hf : Integrable f μ
-- 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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : Integrable f μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
have pos : HSub.hSub (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), ⨍ (a : α), f a ∂μ ∂μ) = 0
Tactic: rw [integral_sub hf (integrable_const _), integral_average, sub_self]
-- 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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : Integrable f μ
pos : HSub.hSub (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), ⨍ (a : α), f a ∂μ ∂μ) = 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
have pos₁ : HSub.hSub (α := E) (∫ (a : α), f a ∂μ) (∫ (x : α), f x ∂μ) = 0
Tactic: rw [integral_sub hf (integrable_const _), integral_average, sub_self]
-- 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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : Integrable f μ
pos : HSub.hSub (α := E) (∫ (a : α), f a ∂μ) (∫ (a : α), ⨍ (a : α), f a ∂μ ∂μ) = 0
pos₁ : HSub.hSub (α := E) (∫ (a : α), f a ∂μ) (∫ (x : α), f x ∂μ) = 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
have pos₂ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [integral_sub hf (integrable_const _), integral_average, sub_self]
-- 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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ) 0
have neg : ∀ (h : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) μ), Integrable f μ
Tactic: refine integral_undef fun h => hf ?_
-- 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
inst_2 : CompleteSpace E
μ : Measure α
inst_3 : IsFiniteMeasure μ
f : α → E
hf : ¬Integrable f μ
h : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) μ
⊢ Integrable f μ
have h₁ : f = HAdd.hAdd (α := α → E) (fun (x : α) ↦ f x - ⨍ (a : α), f a ∂μ) fun (x : α) ↦ ⨍ (a : α), f a ∂μ
Tactic: convert! h.add (integrable_const (⨍ a, f a ∂μ))
-- 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
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
hf : Integrable f μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), ⨍ (a : α), f a ∂μ - f x ∂μ) 0
have rw : HSub.hSub (α := E) (∫ (a : α), ⨍ (a : α), f a ∂μ ∂μ) (∫ (a : α), f a ∂μ) = 0
Tactic: rw [integral_sub (integrable_const _) hf, integral_average, sub_self]
-- 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
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
hf : Integrable f μ
rw : HSub.hSub (α := E) (∫ (a : α), ⨍ (a : α), f a ∂μ ∂μ) (∫ (a : α), f a ∂μ) = 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), ⨍ (a : α), f a ∂μ - f x ∂μ) 0
have rw₁ : HSub.hSub (α := E) (∫ (x : α), f x ∂μ) (∫ (a : α), f a ∂μ) = 0
Tactic: rw [integral_sub (integrable_const _) hf, integral_average, sub_self]
-- 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
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
hf : Integrable f μ
rw : HSub.hSub (α := E) (∫ (a : α), ⨍ (a : α), f a ∂μ ∂μ) (∫ (a : α), f a ∂μ) = 0
rw₁ : HSub.hSub (α := E) (∫ (x : α), f x ∂μ) (∫ (a : α), f a ∂μ) = 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), ⨍ (a : α), f a ∂μ - f x ∂μ) 0
have rw₂ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [integral_sub (integrable_const _) hf, integral_average, sub_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inl : ∀ (hf : @Integrable _ _ _ _ m0 f 0) (hf₀ : 0 ≤ᶠ[ae (F := Measure α) 0] f),
  ENNReal.ofReal (⨍ (x : α), f x ∂0) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂0) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: obtain rfl | hμ := eq_or_ne μ 0
Cleared hypotheses: μ, hf, hf₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
inl :
  ∀ (hf : @Integrable _ _ _ _ m0 f 0) (hf₀ : 0 ≤ᶠ[ae (F := Measure α) 0] f),
    ENNReal.ofReal (⨍ (x : α), f x ∂0) =
      HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂0) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr : ∀ (hμ : μ ≠ 0),
  ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
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 : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr : ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
inr :
  ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr₁ : ENNReal.ofReal ((μ.real univ)⁻¹ * ∫ (x : α), f x ∂μ) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
inr :
  ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₁ :
  ENNReal.ofReal ((μ.real univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr₂ : ENNReal.ofReal ((ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (x : α), f x ∂μ) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
inr :
  ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₁ :
  ENNReal.ofReal ((μ.real univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₂ :
  ENNReal.ofReal ((ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr₃ : ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ * ∫ (x : α), f x ∂μ) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
inr :
  ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₁ :
  ENNReal.ofReal ((μ.real univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₂ :
  ENNReal.ofReal ((ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₃ :
  ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr₄ : ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹) * ENNReal.ofReal (∫ (x : α), f x ∂μ) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
inr :
  ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₁ :
  ENNReal.ofReal ((μ.real univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₂ :
  ENNReal.ofReal ((ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₃ :
  ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₄ :
  ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹) * ENNReal.ofReal (∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr₅ : HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (ENNReal.ofReal (∫ (x : α), f x ∂μ)) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hf₀ : 0 ≤ᶠ[ae μ] f
hμ : μ ≠ 0
inr :
  ENNReal.ofReal (HSMul.hSMul (β := ℝ) (μ.real univ)⁻¹ (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₁ :
  ENNReal.ofReal ((μ.real univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₂ :
  ENNReal.ofReal ((ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ))⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₃ :
  ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ * ∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₄ :
  ENNReal.ofReal (ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹) * ENNReal.ofReal (∫ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
inr₅ :
  HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (ENNReal.ofReal (∫ (x : α), f x ∂μ)) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.ofReal (⨍ (x : α), f x ∂μ) =
    HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have inr₆ : HMul.hMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) =
  HDiv.hDiv (β := ℝ≥0∞) (∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [average_eq, smul_eq_mul, measureReal_def, ← toReal_inv, ofReal_mul toReal_nonneg,
      ofReal_toReal (inv_ne_top.2 <| measure_univ_ne_zero.2 hμ),
      ofReal_integral_eq_lintegral_ofReal hf hf₀, ENNReal.div_eq_inv_mul]