awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
f : ι → Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm ?_ (le_sum_apply _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
f : ι → Measure α
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rcases : ∀ (t : Set α) (hst : s ⊆ t) (htm : MeasurableSet t)
  (ht : ∀ (i : ι), Eq (α := ℝ≥0∞) ((f i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
  LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases exists_measurable_superset_forall_eq f s with ⟨t, hst, htm, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Countable ι
f : ι → Measure α
s t : Set α
hst : s ⊆ t
htm : MeasurableSet t
ht : ∀ (i : ι), Eq (α := ℝ≥0∞) ((f i : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((sum f : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have sum : Eq (α := ℝ≥0∞) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) t) (∑' (i : ι), (f i : (a : Set α) → ℝ≥0∞) s)
Tactic: calc
  sum f s ≤ sum f t := measure_mono hst
  _ = ∑' i, f i t := sum_apply _ htm
  _ = ∑' i, f i s := by simp [ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (x : ι) ↦ 0) 0
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((sum fun (x : ι) ↦ 0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (n : ι) ↦ sum (μ n)) (sum fun (p : ι × ι') ↦ μ p.1 p.2)
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((sum fun (n : ι) ↦ sum (μ n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (p : ι × ι') ↦ μ p.1 p.2 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (n : ι) ↦ sum (μ n)) (sum fun (m : ι') ↦ sum fun (n : ι) ↦ μ n m)
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((sum fun (n : ι) ↦ sum (μ n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (m : ι') ↦ sum fun (n : ι) ↦ μ n m : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((sum fun (n : ι) ↦ sum (μ n) : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (m : ι') ↦ sum fun (n : ι) ↦ μ n m : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (∑' (i : ι) (i_1 : ι'), (μ i i_1 : (a : Set α) → ℝ≥0∞) s)
  (∑' (i : ι') (i_1 : ι), (μ i_1 i : (a : Set α) → ℝ≥0∞) s)
Tactic: simp_rw [sum_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
ι' : Type u_8
μ : ι → ι' → Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι) (i_1 : ι'), (μ i i_1 : (a : Set α) → ℝ≥0∞) s)
    (∑' (i : ι') (i_1 : ι), (μ i_1 i : (a : Set α) → ℝ≥0∞) s)
have h : Eq (α := ℝ≥0∞) (∑' (b : ι') (a : ι), (μ a b : (a : Set α) → ℝ≥0∞) s)
  (∑' (i : ι') (i_1 : ι), (μ i_1 i : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [ENNReal.tsum_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : Fintype ι
μ : ι → Measure α
⊢ sum μ = ∑ i : ι, μ i
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((∑ i : ι, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Finset ι
μ : ι → Measure α
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (i : ↥s) ↦ μ (↑i : ι)) (∑ i ∈ s, μ i)
have rw : Eq.{u_1 + 1} (α := Measure α) (∑ i : ↥s, μ (↑i : ι)) (∑ i ∈ s, μ i)
Tactic: rw [sum_fintype, Finset.sum_coe_sort s μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Finset ι
μ : ι → Measure α
rw : Eq.{u_1 + 1} (α := Measure α) (∑ i : ↥s, μ (↑i : ι)) (∑ i ∈ s, μ i)
⊢ Eq.{u_1 + 1} (α := Measure α) (sum fun (i : ↥s) ↦ μ (↑i : ι)) (∑ i ∈ s, μ i)
have rw₁ : Eq.{u_1 + 1} (α := Measure α) (∑ i ∈ s, μ i) (∑ i ∈ s, μ i)
Tactic: rw [sum_fintype, Finset.sum_coe_sort s μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : Bool → Measure α
⊢ sum f = f true + f false
have rw : ∑ i : Bool, f i = f true + f false
Tactic: rw [sum_fintype, Fintype.sum_bool]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
f : Bool → Measure α
rw : ∑ i : Bool, f i = f true + f false
⊢ sum f = f true + f false
have rw₁ : f true + f false = f true + f false
Tactic: rw [sum_fintype, Fintype.sum_bool]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : IsEmpty ι
μ : ι → Measure α
⊢ sum μ = 0
have rw : Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← measure_univ_eq_zero, sum_apply _ MeasurableSet.univ, tsum_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : IsEmpty ι
μ : ι → Measure α
rw : Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ sum μ = 0
have rw₁ : Eq (α := ℝ≥0∞) (∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) univ) 0
Tactic: rw [← measure_univ_eq_zero, sum_apply _ MeasurableSet.univ, tsum_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
inst : IsEmpty ι
μ : ι → Measure α
rw : Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) (∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) univ) 0
⊢ sum μ = 0
have rw₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← measure_univ_eq_zero, sum_apply _ MeasurableSet.univ, tsum_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
⊢ HAdd.hAdd (α := Measure α) (sum fun (i : (↑s : Type u_5)) ↦ μ (↑i : ι))
      (sum fun (i : (↑sᶜ : Type u_5)) ↦ μ (↑i : ι)) =
    sum μ
have h : ∀ (t : Set α) (ht : MeasurableSet t),
  Eq (α := ℝ≥0∞)
    ((HAdd.hAdd (α := Measure α) (sum fun (i : (↑s : Type u_5)) ↦ μ (↑i : ι))
            (sum fun (i : (↑sᶜ : Type u_5)) ↦ μ (↑i : ι)) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((sum μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: ext1 t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞)
    ((HAdd.hAdd (α := Measure α) (sum fun (i : (↑s : Type u_5)) ↦ μ (↑i : ι))
            (sum fun (i : (↑sᶜ : Type u_5)) ↦ μ (↑i : ι)) :
          (a : Set α) → ℝ≥0∞)
        t :
      ℝ≥0∞)
    ((sum μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h : HAdd.hAdd (α := ℝ≥0∞) (∑' (i : (↑s : Type u_5)), (μ (↑i : ι) : (a : Set α) → ℝ≥0∞) t)
    (∑' (i : (↑sᶜ : Type u_5)), (μ (↑i : ι) : (a : Set α) → ℝ≥0∞) t) =
  ∑' (i : ι), (μ i : (a : Set α) → ℝ≥0∞) t
Tactic: simp only [add_apply, sum_apply _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
μ ν : ι → Measure α
⊢ sum μ + sum ν = sum fun (n : ι) ↦ μ n + ν n
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((sum μ + sum ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((sum fun (n : ι) ↦ μ n + ν n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
e : ι' ≃ ι
m : ι → Measure α
⊢ sum.{u_1, u_9} (ι := ι') (m ∘ (⇑e : (a : ι') → ι)) = sum m
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((sum.{u_1, u_9} (ι := ι') (m ∘ (⇑e : (a : ι') → ι)) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((sum m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ι : Type u_8
ι' : Type u_9
f : ι → ι'
hf : Injective f
m : ι → Measure α
⊢ sum (Function.extend f m 0) = sum m
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((sum (Function.extend f m 0) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sum m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ sᶜ ∈ μ.cofinite ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜᶜ : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [mem_cofinite, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
rw :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜᶜ : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ sᶜ ∈ μ.cofinite ↔ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [mem_cofinite, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
⊢ ∃ t ∈ μ.cofinite, MeasurableSet t ∧ t ⊆ s
have refine_1 : (toMeasurable μ sᶜ)ᶜ ∈ μ.cofinite
Tactic: refine ⟨(toMeasurable μ sᶜ)ᶜ, ?_, (measurableSet_toMeasurable _ _).compl, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
refine_1 : (toMeasurable μ sᶜ)ᶜ ∈ μ.cofinite
⊢ ∃ t ∈ μ.cofinite, MeasurableSet t ∧ t ⊆ s
have refine_2 : (toMeasurable μ sᶜ)ᶜ ⊆ s
Tactic: refine ⟨(toMeasurable μ sᶜ)ᶜ, ?_, (measurableSet_toMeasurable _ _).compl, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
⊢ (toMeasurable μ sᶜ)ᶜ ∈ μ.cofinite
have refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ sᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [compl_mem_cofinite, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ sᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (toMeasurable μ sᶜ)ᶜ ∈ μ.cofinite
have refine_1₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [compl_mem_cofinite, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t s : Set α
hs : s ∈ μ.cofinite
⊢ (toMeasurable μ sᶜ)ᶜ ⊆ s
have refine_2 : sᶜ ⊆ toMeasurable μ sᶜ
Tactic: rw [compl_subset_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ ae μ = ⊥ ↔ μ = 0
have rw : ∅ ∈ ae μ ↔ μ = 0
Tactic: rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
rw : ∅ ∈ ae μ ↔ μ = 0
⊢ ae μ = ⊥ ↔ μ = 0
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ μ = 0
Tactic: rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
rw : ∅ ∈ ae μ ↔ μ = 0
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ μ = 0
⊢ ae μ = ⊥ ↔ μ = 0
have rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ μ = 0
Tactic: rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
rw : ∅ ∈ ae μ ↔ μ = 0
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ μ = 0
rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ↔ μ = 0
⊢ ae μ = ⊥ ↔ μ = 0
have rw₃ : μ = 0 ↔ μ = 0
Tactic: rw [← empty_mem_iff_bot, mem_ae_iff, compl_empty, measure_univ_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Eq (α := ℝ≥0∞) (⨆ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (Iic x) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, Iic i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← measure_biUnion_eq_iSup hsc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, Iic i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ x ∈ s, (μ : (a : Set α) → ℝ≥0∞) (Iic x) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have rw₁ : DirectedOn ((fun (x1 x2 : Set α) ↦ x1 ⊆ x2) on Iic) s
Tactic: rw [← measure_biUnion_eq_iSup hsc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, Iic i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
have h : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iic i) univ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Preorder α
s : Set α
hsc : s.Countable
hst : ∀ (x : α), ∃ y ∈ s, x ≤ y
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iic i) univ
have hst₁ : ∀ (x : α), ∃ (x_1 : α) (_ : x_1 ∈ s), x ≤ x_1
Tactic: simp only [← bex_def] at hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : NoMaxOrder α
inst_2 : IsCountablyGenerated.{u_1} (α := α) atTop
μ : Measure α
a : α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ico a x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (Ici a)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ico a x) : ℝ≥0∞)) atTop
  (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : α), Ico a b)) : Filter ℝ≥0∞)
Tactic: rw [← iUnion_Ico_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : NoMinOrder α
inst_2 : IsCountablyGenerated.{u_1} (α := α) atBot
μ : Measure α
a : α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ioc x a) : ℝ≥0∞)) atBot
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (Iic a)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Ioc x a) : ℝ≥0∞)) atBot
  (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : α), Ioc b a)) : Filter ℝ≥0∞)
Tactic: rw [← iUnion_Ioc_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
inst : Preorder α
inst_1 : IsCountablyGenerated.{u_1} (α := α) atTop
μ : Measure α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Iic x) : ℝ≥0∞)) atTop
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Iic x) : ℝ≥0∞)) atTop
  (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋃ (a : α), Iic a)) : Filter ℝ≥0∞)
Tactic: rw [← iUnion_Iic]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Iio a =ᶠ[ae μ] Iic a
have rw : Iic a \ {a} =ᶠ[ae μ] Iic a
Tactic: rw [← Iic_diff_right, diff_ae_eq_self, measure_mono_null Set.inter_subset_right ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Iic a \ {a} =ᶠ[ae μ] Iic a
⊢ Iio a =ᶠ[ae μ] Iic a
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a ∩ {a}) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← Iic_diff_right, diff_ae_eq_self, measure_mono_null Set.inter_subset_right ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : PartialOrder α
a : α
ha : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Iic a \ {a} =ᶠ[ae μ] Iic a
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Iic a ∩ {a}) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Iio a =ᶠ[ae μ] Iic a
have rw₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← Iic_diff_right, diff_ae_eq_self, measure_mono_null Set.inter_subset_right ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ Eq (α := ℝ≥0∞) ((inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (iUnion f) : ℝ≥0∞)
    (∑' (i : ℕ), (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (f i) sorry)
  (∑' (i : ℕ), (inducedOuterMeasure (P := MeasurableSet) m sorry m0 : (a : Set α) → ℝ≥0∞) (f i))
Tactic: rw [inducedOuterMeasure_eq m0 mU (MeasurableSet.iUnion hf), mU hf hd]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), m (f i) ⋯)
    (∑' (i : ℕ), (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f i))
have e_f : Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ m (f i) sorry) fun (i : ℕ) ↦
  (inducedOuterMeasure (P := MeasurableSet) m sorry m0 : (a : Set α) → ℝ≥0∞) (f i)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ m (f i) ⋯) fun (i : ℕ) ↦
    (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f i)
have e_f : ∀ (n : ℕ), m (f n) sorry = (inducedOuterMeasure (P := MeasurableSet) m sorry m0 : (a : Set α) → ℝ≥0∞) (f n)
Tactic: funext n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
n : ℕ
⊢ m (f n) ⋯ = (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f n)
have e_f : m (f n) sorry = m (f n) sorry
Tactic: rw [inducedOuterMeasure_eq m0 mU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
f : ℕ → Set α
hf : ∀ (i : ℕ), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
n : ℕ
e_f : m (f n) ⋯ = m (f n) ⋯
⊢ m (f n) ⋯ = (inducedOuterMeasure (P := MeasurableSet) m ⋯ m0 : (a : Set α) → ℝ≥0∞) (f n)
have e_f₁ : MeasurableSet (f n)
Tactic: rw [inducedOuterMeasure_eq m0 mU]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Sort u_5
inst : MeasurableSpace α
μ μ₁ μ₂ : Measure α
s_1 s₁ s₂ t : Set α
m : (s : Set α) → MeasurableSet s → ℝ≥0∞
m0 : m ∅ ⋯ = 0
mU :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
s : Set α
hs : MeasurableSet s
⊢ ((inducedOuterMeasure (P := MeasurableSet) m ⋯ m0).trim : (a : Set α) → ℝ≥0∞) s ≤ m s hs
have rw : (inducedOuterMeasure (P := MeasurableSet) m sorry m0 : (a : Set α) → ℝ≥0∞) s ≤ m s hs
Tactic: rw [OuterMeasure.trim_eq _ hs, inducedOuterMeasure_eq m0 mU hs]