awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∂μ)
rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) 1⁻¹ μ) (∫ (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]
-- 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 ∂μ)
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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (⨍ (x : α), f x ∂μ) (∫ (x : α), f x ∂μ)
have rw₃ : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂μ) (∫ (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 : IsFiniteMeasure μ
f : α → E
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
have inl : ∀ (hμ : μ = 0), HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
Tactic: rcases eq_or_ne μ 0 with hμ | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
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 ∂μ
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
have inr : ∀ (hμ : μ ≠ 0), HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
Tactic: rcases eq_or_ne μ 0 with hμ | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Average (goal)
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure α
inst_2 : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
have inl : HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) (⨍ (x : α), f x ∂0) =
  @integral _ _ _ _ m0 0 fun (x : α) ↦ f x
Tactic: rw [hμ, integral_zero_measure, average_zero_measure, smul_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 α
inst_2 : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
inl :
  HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) (⨍ (x : α), f x ∂0) =
    @integral _ _ _ _ m0 0 fun (x : α) ↦ f x
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
have inl₁ : HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) (⨍ (x : α), f x ∂0) = 0
Tactic: rw [hμ, integral_zero_measure, average_zero_measure, smul_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 α
inst_2 : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
inl :
  HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) (⨍ (x : α), f x ∂0) =
    @integral _ _ _ _ m0 0 fun (x : α) ↦ f x
inl₁ : HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) (⨍ (x : α), f x ∂0) = 0
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
have inl₂ : HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) 0 = 0
Tactic: rw [hμ, integral_zero_measure, average_zero_measure, smul_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 α
inst_2 : IsFiniteMeasure μ
f : α → E
hμ : μ = 0
inl :
  HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) (⨍ (x : α), f x ∂0) =
    @integral _ _ _ _ m0 0 fun (x : α) ↦ f x
inl₁ : HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) (⨍ (x : α), f x ∂0) = 0
inl₂ : HSMul.hSMul (β := E) (Measure.real.{u_1} (α := α) (m := m0) 0 univ) 0 = 0
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
have inl₃ : Eq.{u_2 + 1} (α := E) 0 0
Tactic: rw [hμ, integral_zero_measure, average_zero_measure, smul_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 α
inst_2 : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ HSMul.hSMul (β := E) (μ.real univ) (⨍ (x : α), f x ∂μ) = ∫ (x : α), f x ∂μ
have inr : μ.real univ ≠ 0
Tactic: rw [average_eq, smul_inv_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 : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ μ.real univ ≠ 0
have inr : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine (ENNReal.toReal_pos ?_ <| measure_ne_top _ _).ne'
-- 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 : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [Ne, measure_univ_eq_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 α
inst_2 : IsFiniteMeasure μ
f : α → E
hμ : μ ≠ 0
inr : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have inr₁ : ¬μ = 0
Tactic: rwa [Ne, measure_univ_eq_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 α
f : α → E
s : Set α
⊢ ⨍ (x : α) in s, f x ∂μ = HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ)
have rw : HSMul.hSMul (β := E) ((μ.restrict s).real univ)⁻¹ (∫ (x : α) in s, f x ∂μ) =
  HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ)
Tactic: rw [average_eq, measureReal_restrict_apply_univ]
-- 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 : Set α
rw :
  HSMul.hSMul (β := E) ((μ.restrict s).real univ)⁻¹ (∫ (x : α) in s, f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ)
⊢ ⨍ (x : α) in s, f x ∂μ = HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ)
have rw₁ : HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ) = HSMul.hSMul (β := E) (μ.real s)⁻¹ (∫ (x : α) in s, f x ∂μ)
Tactic: rw [average_eq, measureReal_restrict_apply_univ]
-- 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 : IsFiniteMeasure μ
ν : Measure α
inst_3 : IsFiniteMeasure ν
f : α → E
hμ : Integrable f μ
hν : Integrable f ν
⊢ ⨍ (x : α), f x ∂(μ + ν) =
    HSMul.hSMul (β := E) (μ.real univ / (μ.real univ + ν.real univ)) (⨍ (x : α), f x ∂μ) +
      HSMul.hSMul (β := E) (ν.real univ / (μ.real univ + ν.real univ)) (⨍ (x : α), f x ∂ν)
have simp : ⨍ (x : α), f x ∂(μ + ν) = HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))
Tactic: simp only [div_eq_inv_mul, mul_smul, measure_smul_average, ← smul_add,
    ← integral_add_measure hμ hν]
-- 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 : IsFiniteMeasure μ
ν : Measure α
inst_3 : IsFiniteMeasure ν
f : α → E
hμ : Integrable f μ
hν : Integrable f ν
⊢ ⨍ (x : α), f x ∂(μ + ν) = HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))
have rw : HSMul.hSMul (β := E) ((μ + ν).real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν)) =
  HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))
Tactic: rw [average_eq, measureReal_add_apply]
-- 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 : IsFiniteMeasure μ
ν : Measure α
inst_3 : IsFiniteMeasure ν
f : α → E
hμ : Integrable f μ
hν : Integrable f ν
rw :
  HSMul.hSMul (β := E) ((μ + ν).real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν)) =
    HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))
⊢ ⨍ (x : α), f x ∂(μ + ν) = HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))
have rw₁ : HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν)) =
  HSMul.hSMul (β := E) (μ.real univ + ν.real univ)⁻¹ (∫ (x : α), f x ∂(μ + ν))
Tactic: rw [average_eq, measureReal_add_apply]
-- 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 : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: haveI := Fact.mk h.lt_top
-- 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 : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
have rw : HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ) =
  HSMul.hSMul (β := E) ((μ.restrict s).real univ) (⨍ (x : α) in s, f x ∂μ)
Tactic: rw [← measure_smul_average, measureReal_restrict_apply_univ]
-- 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 : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
rw :
  HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ) =
    HSMul.hSMul (β := E) ((μ.restrict s).real univ) (⨍ (x : α) in s, f x ∂μ)
⊢ HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ) = ∫ (x : α) in s, f x ∂μ
have rw₁ : HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ) = HSMul.hSMul (β := E) (μ.real s) (⨍ (x : α) in s, f x ∂μ)
Tactic: rw [← measure_smul_average, measureReal_restrict_apply_univ]
-- 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 μ
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
have this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: haveI := Fact.mk hsμ.lt_top
-- 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 μ
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
have this₁ : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: haveI := Fact.mk htμ.lt_top
-- 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 μ
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
have rw : ⨍ (x : α), f x ∂(μ.restrict s + μ.restrict t) =
  HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
    HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
Tactic: rw [restrict_union₀ hd ht, average_add_measure hfs hft, measureReal_restrict_apply_univ,
    measureReal_restrict_apply_univ]
-- 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 μ
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
rw :
  ⨍ (x : α), f x ∂(μ.restrict s + μ.restrict t) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
have rw₁ : HSMul.hSMul (β := E) ((μ.restrict s).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ))
      (⨍ (x : α) in s, f x ∂μ) +
    HSMul.hSMul (β := E) ((μ.restrict t).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ))
      (⨍ (x : α) in t, f x ∂μ) =
  HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
    HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
Tactic: rw [restrict_union₀ hd ht, average_add_measure hfs hft, measureReal_restrict_apply_univ,
    measureReal_restrict_apply_univ]
-- 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 μ
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
rw :
  ⨍ (x : α), f x ∂(μ.restrict s + μ.restrict t) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
rw₁ :
  HSMul.hSMul (β := E) ((μ.restrict s).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ))
        (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) ((μ.restrict t).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ))
        (⨍ (x : α) in t, f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
have rw₂ : HSMul.hSMul (β := E) (μ.real s / (μ.real s + (μ.restrict t).real univ)) (⨍ (x : α) in s, f x ∂μ) +
    HSMul.hSMul (β := E) ((μ.restrict t).real univ / (μ.real s + (μ.restrict t).real univ)) (⨍ (x : α) in t, f x ∂μ) =
  HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
    HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
Tactic: rw [restrict_union₀ hd ht, average_add_measure hfs hft, measureReal_restrict_apply_univ,
    measureReal_restrict_apply_univ]
-- 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 μ
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
this : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
rw :
  ⨍ (x : α), f x ∂(μ.restrict s + μ.restrict t) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
rw₁ :
  HSMul.hSMul (β := E) ((μ.restrict s).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ))
        (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) ((μ.restrict t).real univ / ((μ.restrict s).real univ + (μ.restrict t).real univ))
        (⨍ (x : α) in t, f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
rw₂ :
  HSMul.hSMul (β := E) (μ.real s / (μ.real s + (μ.restrict t).real univ)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) ((μ.restrict t).real univ / (μ.real s + (μ.restrict t).real univ)) (⨍ (x : α) in t, f x ∂μ) =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
⊢ ⨍ (x : α) in s ∪ t, f x ∂μ =
    HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
      HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
have rw₃ : HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
    HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ) =
  HSMul.hSMul (β := E) (μ.real s / (μ.real s + μ.real t)) (⨍ (x : α) in s, f x ∂μ) +
    HSMul.hSMul (β := E) (μ.real t / (μ.real s + μ.real t)) (⨍ (x : α) in t, f x ∂μ)
Tactic: rw [restrict_union₀ hd ht, average_add_measure hfs hft, measureReal_restrict_apply_univ,
    measureReal_restrict_apply_univ]
-- 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 : ℝ≥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∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ Membership.mem (γ := Set E) (openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ))
    (⨍ (x : α) in s ∪ t, f x ∂μ)
have hs₁ : 0 < μ.real s
Tactic: replace hs₀ : 0 < μ.real s := ENNReal.toReal_pos hs₀ hsμ
Cleared hypotheses: hs₀
-- 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 μ
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∞)
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
hs₀ : 0 < μ.real s
⊢ Membership.mem (γ := Set E) (openSegment ℝ (⨍ (x : α) in s, f x ∂μ) (⨍ (x : α) in t, f x ∂μ))
    (⨍ (x : α) in s ∪ t, f x ∂μ)
have ht₁ : 0 < μ.real t
Tactic: replace ht₀ : 0 < μ.real t := ENNReal.toReal_pos ht₀ htμ
Cleared hypotheses: ht₀
-- 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 μ
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)
have pos : ∀ (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 ∂μ)
Tactic: by_cases hse : μ s = 0
-- 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 μ
pos :
  ∀ (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 ∂μ)
⊢ Membership.mem (γ := Set E) [⨍ (x : α) in s, f x ∂μ -[ℝ] ⨍ (x : α) in t, f x ∂μ] (⨍ (x : α) in s ∪ t, f x ∂μ)
have neg : ∀ (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 ∂μ)
Tactic: by_cases hse : μ s = 0