awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
K : Set G
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst_1] L
⊢ r < (μ : (a : Set G) → ℝ≥0∞) L
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) L : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
Tactic: convert! hr using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.EverywherePos (goal)
Goal:
G : Type u_2
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : LocallyCompactSpace G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : μ.IsMulLeftInvariant
inst_7 : IsFiniteMeasureOnCompacts μ
inst_8 : μ.InnerRegularCompactLTTop
K : Set G
K_comp : IsCompact K
K_closed : IsClosed[inst_1] K
r : ℝ≥0∞
hr : r < (μ : (a : Set G) → ℝ≥0∞) K
L : Set G := μ.everywherePosSubset K
L_comp : IsCompact L
L_closed : IsClosed[inst_1] L
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) L : ℝ≥0∞) ((μ : (a : Set G) → ℝ≥0∞) K : ℝ≥0∞)
have h : L =ᶠ[ae μ] K
Tactic: apply measure_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : FiniteMeasure Ω
s : Set Ω
h : Eq (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = 0
Tactic: rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : FiniteMeasure Ω
s : Set Ω
h : Eq (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0) (0 : ℝ≥0)
rw : (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : (↑0 : ℝ≥0∞) = 0
Tactic: rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : FiniteMeasure Ω
s : Set Ω
h : Eq (α := ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0) (0 : ℝ≥0)
rw : (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = 0
rw₁ : (↑0 : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← ennreal_coeFn_eq_coeFn_toMeasure, h, ENNReal.coe_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
⊢ (μ : (a : Set Ω) → ℝ≥0) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
have this : ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)
Tactic: have := measure_union_le (μ := (μ : Measure Ω)) s₁ s₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
have apply : (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)).toNNReal =
  HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
Tactic: apply (ENNReal.toNNReal_mono (by finiteness) this).trans_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)
⊢ (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
        (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)).toNNReal =
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
have rw : ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁) +
    ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂) =
  HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
Tactic: rw [ENNReal.toNNReal_add (by finiteness) (by finiteness), coeFn_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s₁ s₂ : Set Ω
this :
  ((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s₁ ∪ s₂) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)
rw :
  ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁) +
      ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂) =
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
⊢ (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁ : ℝ≥0∞)
        (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂ : ℝ≥0∞)).toNNReal =
    HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₁ : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s₂ : ℝ≥0)
have rw₁ : ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₁) +
    ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s₂) =
  HAdd.hAdd (α := ℝ≥0) ((fun (s : Set Ω) ↦ ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)) s₁)
    ((fun (s : Set Ω) ↦ ENNReal.toNNReal (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s)) s₂)
Tactic: rw [ENNReal.toNNReal_add (by finiteness) (by finiteness), coeFn_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ.mass = 0 ↔ μ = 0
have refine : ∀ (μ_mass : μ.mass = 0), μ = 0
Tactic: refine ⟨fun μ_mass => ?_, fun hμ => by simp only [hμ, zero_mass]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ μ = 0
have a : (↑μ : Measure Ω) = (↑0 : Measure Ω)
Tactic: apply toMeasure_injective
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ (↑μ : Measure Ω) = (↑0 : Measure Ω)
have a : Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: apply Measure.measure_univ_eq_zero.mp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
μ_mass : μ.mass = 0
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have a : (↑μ.mass : ℝ≥0∞) = 0
Tactic: rwa [← ennreal_mass, ENNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν
have a : (↑μ : Measure Ω) = (↑ν : Measure Ω)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h :
  ∀ (s : Set Ω),
    MeasurableSet s →
      Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
        (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (↑μ : Measure Ω) = (↑ν : Measure Ω)
have a : ∀ (s : Set Ω) (s_mble : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s s_mble
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
h : ∀ (s : Set Ω), MeasurableSet s → Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((ν : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
⊢ μ = ν
have h₁ : ∀ (s : Set Ω) (s_mble : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s s_mble
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
⊢ (⇑(μ + ν) : (a : Set Ω) → ℝ≥0) = HAdd.hAdd (α := (a : Set Ω) → ℝ≥0) (⇑μ : (a : Set Ω) → ℝ≥0) (⇑ν : (a : Set Ω) → ℝ≥0)
have h : ∀ (x : Set Ω),
  (μ + ν : (a : Set Ω) → ℝ≥0) x =
    HAdd.hAdd (α := (a : Set Ω) → ℝ≥0) (β := (a : Set Ω) → ℝ≥0) (⇑μ : (a : Set Ω) → ℝ≥0) (⇑ν : (a : Set Ω) → ℝ≥0) x
Tactic: funext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ ν : FiniteMeasure Ω
x : Set Ω
⊢ (μ + ν : (a : Set Ω) → ℝ≥0) x =
    HAdd.hAdd (α := (a : Set Ω) → ℝ≥0) (β := (a : Set Ω) → ℝ≥0) (⇑μ : (a : Set Ω) → ℝ≥0) (⇑ν : (a : Set Ω) → ℝ≥0) x
have h : ((↑(μ + ν) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) x =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) x : ℝ≥0∞)
    (((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) x : ℝ≥0∞)
Tactic: simp only [Pi.add_apply, ← ENNReal.coe_inj, ennreal_coeFn_eq_coeFn_toMeasure,
    ENNReal.coe_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
R : Type u_2
inst_1 : SMul R ℝ≥0
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
⊢ (⇑(c • μ) : (a : Set Ω) → ℝ≥0) = HSMul.hSMul (β := (a : Set Ω) → ℝ≥0) c (⇑μ : (a : Set Ω) → ℝ≥0)
have h : ∀ (x : Set Ω), (c • μ : (a : Set Ω) → ℝ≥0) x = HSMul.hSMul (β := (a : Set Ω) → ℝ≥0) c (⇑μ : (a : Set Ω) → ℝ≥0) x
Tactic: funext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
R : Type u_2
inst_1 : SMul R ℝ≥0
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
s : Set Ω
⊢ (c • μ : (a : Set Ω) → ℝ≥0) s = HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have rw : HSMul.hSMul (β := (a : Set Ω) → ℝ≥0) c (⇑μ : (a : Set Ω) → ℝ≥0) s =
  HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
Tactic: rw [coeFn_smul, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
R : Type u_2
inst_1 : SMul R ℝ≥0
inst_2 : SMul R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0 ℝ≥0∞
inst_4 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_5 : IsScalarTower R ℝ≥0 ℝ≥0
c : R
μ : FiniteMeasure Ω
s : Set Ω
rw :
  HSMul.hSMul (β := (a : Set Ω) → ℝ≥0) c (⇑μ : (a : Set Ω) → ℝ≥0) s =
    HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
⊢ (c • μ : (a : Set Ω) → ℝ≥0) s = HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
have rw₁ : HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0) = HSMul.hSMul (β := ℝ≥0) c ((μ : (a : Set Ω) → ℝ≥0) s : ℝ≥0)
Tactic: rw [coeFn_smul, Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A s : Set Ω
s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0) ((μ.restrict A : (a : Set Ω) → ℝ≥0) s : ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) (s ∩ A) : ℝ≥0)
have apply : Eq (α := ℝ≥0∞) (((↑(μ.restrict A) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
  (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (s ∩ A) : ℝ≥0∞)
Tactic: apply congr_arg ENNReal.toNNReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
⊢ μ.restrict univ = μ
have h : ∀ (s : Set Ω),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((↑(μ.restrict univ) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
s t : Set Ω
h : Disjoint s t
ht : MeasurableSet t
⊢ μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
have h₁ : ∀ (u : Set Ω) (hu : MeasurableSet u),
  Eq (α := ℝ≥0∞) (((↑(μ.restrict (s ∪ t)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) u : ℝ≥0∞)
    (((↑(μ.restrict s + μ.restrict t) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: ext u hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
⊢ μ.restrict (⋃ i ∈ T, s i) = ∑ i ∈ T, μ.restrict (s i)
have h : ∀ (t : Set Ω) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞) (((↑(μ.restrict (⋃ i ∈ T, s i)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
    ((((↑(∑ i ∈ T, μ.restrict (s i)) : Measure Ω) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((↑(μ.restrict (⋃ i ∈ T, s i)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
    ((((↑(∑ i ∈ T, μ.restrict (s i)) : Measure Ω) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (((↑μ : Measure Ω).restrict (⋃ i ∈ T, s i) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
  (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp only [restrict_measure_eq, toMeasure_sum, Measure.coe_finsetSum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (((↑μ : Measure Ω).restrict (⋃ i ∈ T, s i) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  (((Measure.sum fun (i : ↥T) ↦ (↑μ : Measure Ω).restrict (s (↑i : ι)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
  (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [Measure.restrict_biUnion_finset hd hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞)
    (((Measure.sum fun (i : ↥T) ↦ (↑μ : Measure Ω).restrict (s (↑i : ι)) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
  (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t)
Tactic: simp only [Measure.sum_fintype, Finset.univ_eq_attach, Measure.coe_finsetSum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
| ∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t
have rw : ∑ x ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑x : ι)) : (a : Set Ω) → ℝ≥0∞) t
Tactic: rw [← Finset.sum_attach]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t)
have conv_rhs : Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
  (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t)
Tactic: conv_rhs => rw [← Finset.sum_attach]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ι : Type u_3
μ : FiniteMeasure Ω
T : Finset ι
s : ι → Set Ω
hd : (↑T : Set ι).Pairwise (Disjoint on s)
hm : ∀ (i : ι), MeasurableSet (s i)
t : Set Ω
ht : MeasurableSet t
conv_rhs :
  Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t)
⊢ Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
    (∑ c ∈ T, ((↑μ : Measure Ω).restrict (s c) : (a : Set Ω) → ℝ≥0∞) t)
have h : Eq (α := ℝ≥0∞) (∑ c ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑c : ι)) : (a : Set Ω) → ℝ≥0∞) t)
  (∑ x ∈ T.attach, ((↑μ : Measure Ω).restrict (s (↑x : ι)) : (a : Set Ω) → ℝ≥0∞) t)
Tactic: conv_rhs => rw [← Finset.sum_attach]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
⊢ μ.restrict A = 0 ↔ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0)
have rw : (μ.restrict A).mass = 0 ↔ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0)
Tactic: rw [← mass_zero_iff, restrict_mass]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : FiniteMeasure Ω
A : Set Ω
rw : (μ.restrict A).mass = 0 ↔ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0)
⊢ μ.restrict A = 0 ↔ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0)
have rw₁ : Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0) ↔ Eq (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) A : ℝ≥0) (0 : ℝ≥0)
Tactic: rw [← mass_zero_iff, restrict_mass]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
this :
  Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))
⊢ MeasurableSet.{u_1} (α := Measure Ω) {μ : Measure Ω | IsFiniteMeasure μ}
have rw : MeasurableSet.{u_1} (α := Measure Ω)
  (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ MeasurableSet.{u_1} (α := Measure Ω) {μ : Measure Ω | IsFiniteMeasure μ}
have suffices : Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ}
  (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))
Tactic: suffices { μ : Measure Ω | IsFiniteMeasure μ } = (fun μ => μ univ) ⁻¹' (Set.Ico 0 ∞) by
    rw [this]
    exact Measure.measurable_coe MeasurableSet.univ measurableSet_Ico
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ Eq.{u_1 + 1} (α := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ}
    (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞))
have h : ∀ (μ : Measure Ω),
  Membership.mem (γ := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ} μ ↔
    Membership.mem (γ := Set (Measure Ω))
      (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞)) μ
Tactic: ext μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
μ : Measure Ω
⊢ Membership.mem (γ := Set (Measure Ω)) {μ : Measure Ω | IsFiniteMeasure μ} μ ↔
    Membership.mem (γ := Set (Measure Ω))
      (preimage (β := ℝ≥0∞) (fun (μ : Measure Ω) ↦ (μ : (a : Set Ω) → ℝ≥0∞) univ) (Ico 0 ∞)) μ
have h : IsFiniteMeasure μ ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [mem_setOf_eq, mem_preimage, mem_Ico, zero_le, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
⊢ Measurable (β := Measure (α × β)) fun (μ : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    (↑μ.1 : Measure α).prod (↑μ.2 : Measure β)
have Heval : ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
      (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
Tactic: have Heval {u v} (Hu : MeasurableSet u) (Hv : MeasurableSet v) :
      Measurable fun a : (FiniteMeasure α × FiniteMeasure β) ↦
      a.1.toMeasure u * a.2.toMeasure v :=
    Measurable.mul
      ((Measure.measurable_coe Hu).comp (measurable_subtype_coe.comp measurable_fst))
      ((Measure.measurable_coe Hv).comp (measurable_subtype_coe.comp measurable_snd))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
⊢ Measurable (β := Measure (α × β)) fun (μ : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    (↑μ.1 : Measure α).prod (↑μ.2 : Measure β)
have apply : Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
  ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) univ
Tactic: apply Measurable.measure_of_isPiSystem generateFrom_prod.symm isPiSystem_prod _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
α : Type u_3
β : Type u_4
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
Heval :
  ∀ {u : Set α} {v : Set β} (Hu : MeasurableSet u) (Hv : MeasurableSet v),
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((↑a.1 : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
        (((↑a.2 : Measure β) : (a : Set β) → ℝ≥0∞) v : ℝ≥0∞)
apply :
  Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) univ
⊢ Measurable (β := Measure (α × β)) fun (μ : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
    (↑μ.1 : Measure α).prod (↑μ.2 : Measure β)
have apply₁ : ∀ (s : Set (α × β)),
  Membership.mem (γ := Set (Set (α × β)))
      (image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
      s →
    Measurable (β := ℝ≥0∞) fun (a : Prod.{u_3, u_4} (FiniteMeasure α) (FiniteMeasure β)) ↦
      ((↑a.1 : Measure α).prod (↑a.2 : Measure β) : (a : Set (α × β)) → ℝ≥0∞) s
Tactic: apply Measurable.measure_of_isPiSystem generateFrom_prod.symm isPiSystem_prod _