awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : (n : ℕ) → Set α
hs₂ : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
hs₃ : ∀ (n : ℕ), (ν : (a : Set α) → ℝ≥0∞) (s n)ᶜ ≤ (1 / 2) ^ n
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), (s i)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [compl_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : (n : ℕ) → Set α
hs₂ : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
hs₃ : ∀ (n : ℕ), (ν : (a : Set α) → ℝ≥0∞) (s n)ᶜ ≤ (1 / 2) ^ n
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), (s i)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : ∀ (n : ℕ), (ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), (s i)ᶜ) ≤ (↑1 : ℝ≥0∞) * (1 / 2) ^ n
Tactic: refine eq_zero_of_le_mul_pow (ε := 1) (by simp : (1 / 2 : ℝ≥0∞) < 1) <| fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : (n : ℕ) → Set α
hs₂ : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
hs₃ : ∀ (n : ℕ), (ν : (a : Set α) → ℝ≥0∞) (s n)ᶜ ≤ (1 / 2) ^ n
n : ℕ
⊢ (ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), (s i)ᶜ) ≤ (↑1 : ℝ≥0∞) * (1 / 2) ^ n
have refine_1 : (ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), (s i)ᶜ) ≤ (1 / 2) ^ n
Tactic: rw [ENNReal.coe_one, one_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
s : (n : ℕ) → Set α
hs₂ : ∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (0 : ℝ≥0∞)
hs₃ : ∀ (n : ℕ), (ν : (a : Set α) → ℝ≥0∞) (s n)ᶜ ≤ (1 / 2) ^ n
⊢ Subset.{u_1} (α := Set α) univ ((⋃ (i : ℕ), s i) ∪ (⋃ (n : ℕ), s n)ᶜ)
have refine_2 : Subset.{u_1} (α := Set α) univ univ
Tactic: rw [union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
ξ : Measure α
⊢ ξ ≤ ⊥ ↔ ξ = 0
have rw : ξ = ⊥ ↔ ξ = 0
Tactic: rw [le_bot_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ Disjoint μ ν
have h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
Tactic: have h_bot_iff (ξ : Measure α) : ξ ≤ ⊥ ↔ ξ = 0 := by
    rw [le_bot_iff]
    rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
⊢ ξ ≤ ⊥
have rw : ξ = 0
Tactic: rw [h_bot_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
⊢ ξ = 0
have h₁ : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) (s ∩ h.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) (s ∩ h.nullSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← inter_union_compl s h.nullSet, measure_union, add_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
h₁ :
  Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) (s ∩ h.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) (s ∩ h.nullSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have h₂ : Disjoint (s ∩ h.nullSet) (s ∩ h.nullSetᶜ)
Tactic: rw [← inter_union_compl s h.nullSet, measure_union, add_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
h₁ :
  Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) (s ∩ h.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) (s ∩ h.nullSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
h₂ : Disjoint (s ∩ h.nullSet) (s ∩ h.nullSetᶜ)
⊢ Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have h₃ : MeasurableSet (s ∩ h.nullSetᶜ)
Tactic: rw [← inter_union_compl s h.nullSet, measure_union, add_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ Disjoint (ae μ) (ae ν)
have rw : ae μ ⊓ ae ν ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
⊢ s ∈ ae μ ⊓ ae ν
have refine_1 : s ∪ h.nullSetᶜ ∈ ae μ
Tactic: refine ⟨s ∪ h.nullSetᶜ, ?_, s ∪ h.nullSet, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
refine_1 : s ∪ h.nullSetᶜ ∈ ae μ
⊢ s ∈ ae μ ⊓ ae ν
have refine_2 : s ∪ h.nullSet ∈ ae ν
Tactic: refine ⟨s ∪ h.nullSetᶜ, ?_, s ∪ h.nullSet, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
refine_1 : s ∪ h.nullSetᶜ ∈ ae μ
refine_2 : s ∪ h.nullSet ∈ ae ν
⊢ s ∈ ae μ ⊓ ae ν
have refine_3 : s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
Tactic: refine ⟨s ∪ h.nullSetᶜ, ?_, s ∪ h.nullSet, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
⊢ s ∪ h.nullSetᶜ ∈ ae μ
have refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sᶜ ∩ h.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [mem_ae_iff, compl_union, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
⊢ s ∪ h.nullSet ∈ ae ν
have refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (sᶜ ∩ h.nullSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [mem_ae_iff, compl_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
have refine_3 : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (s ∪ h.nullSet)
Tactic: rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl,
      ← compl_union, compl_compl, inter_union_compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
refine_3 : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (s ∪ h.nullSet)
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
have refine_3₁ : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (sᶜ ∩ h.nullSetᶜ)ᶜ
Tactic: rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl,
      ← compl_union, compl_compl, inter_union_compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
refine_3 : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (s ∪ h.nullSet)
refine_3₁ : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (sᶜ ∩ h.nullSetᶜ)ᶜ
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
have refine_3₂ : s = (sᶜ ∩ h.nullSetᶜᶜ ∪ sᶜ ∩ h.nullSetᶜ)ᶜ
Tactic: rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl,
      ← compl_union, compl_compl, inter_union_compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
refine_3 : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (s ∪ h.nullSet)
refine_3₁ : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (sᶜ ∩ h.nullSetᶜ)ᶜ
refine_3₂ : s = (sᶜ ∩ h.nullSetᶜᶜ ∪ sᶜ ∩ h.nullSetᶜ)ᶜ
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
have refine_3₃ : s = (sᶜ ∩ h.nullSet ∪ sᶜ ∩ h.nullSetᶜ)ᶜ
Tactic: rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl,
      ← compl_union, compl_compl, inter_union_compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
refine_3 : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (s ∪ h.nullSet)
refine_3₁ : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (sᶜ ∩ h.nullSetᶜ)ᶜ
refine_3₂ : s = (sᶜ ∩ h.nullSetᶜᶜ ∪ sᶜ ∩ h.nullSetᶜ)ᶜ
refine_3₃ : s = (sᶜ ∩ h.nullSet ∪ sᶜ ∩ h.nullSetᶜ)ᶜ
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
have refine_3₄ : s = sᶜᶜ
Tactic: rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl,
      ← compl_union, compl_compl, inter_union_compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
refine_3 : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (s ∪ h.nullSet)
refine_3₁ : s = (sᶜ ∩ h.nullSetᶜᶜ)ᶜ ∩ (sᶜ ∩ h.nullSetᶜ)ᶜ
refine_3₂ : s = (sᶜ ∩ h.nullSetᶜᶜ ∪ sᶜ ∩ h.nullSetᶜ)ᶜ
refine_3₃ : s = (sᶜ ∩ h.nullSet ∪ sᶜ ∩ h.nullSetᶜ)ᶜ
refine_3₄ : s = sᶜᶜ
⊢ s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
have refine_3₅ : s = s
Tactic: rw [union_eq_compl_compl_inter_compl, union_eq_compl_compl_inter_compl,
      ← compl_union, compl_compl, inter_union_compl, compl_compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint (ae μ) (ae ν)
⊢ Disjoint μ ν
have h₁ : ∃ (s : Set α),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    ∃ (t : Set α), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ Disjoint s t
Tactic: simp_rw [Filter.disjoint_iff, mem_ae_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h :
  ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧
      ∃ (t : Set α), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ Disjoint s t
⊢ Disjoint μ ν
have obtain : ∀ (s : Set α) (hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)) (t : Set α)
  (ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)) (hst : Disjoint s t), Disjoint μ ν
Tactic: obtain ⟨s, hs, t, ht, hst⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hst : Disjoint s t
⊢ Disjoint μ ν
have rw : μ ⊓ ν ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hst : Disjoint s t
⊢ μ ⊓ ν ≤ ⊥
have this : Eq.{u_1 + 1} (α := Measure α) ⊥ 0
Tactic: have : (⊥ : Measure α) = 0 := rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hst : Disjoint s t
this : Eq.{u_1 + 1} (α := Measure α) ⊥ 0
⊢ μ ⊓ ν ≤ ⊥
have refine : ∀ (u : Set α) (hu : MeasurableSet u),
  u.Nonempty →
    LE.le (α := ℝ≥0∞) ((μ ⊓ ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (((⊥ : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
Tactic: refine Measure.le_intro fun u hu _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hst : Disjoint s t
this : Eq.{u_1 + 1} (α := Measure α) ⊥ 0
u : Set α
hu : MeasurableSet u
h : u.Nonempty
⊢ LE.le (α := ℝ≥0∞) ((μ ⊓ ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (((⊥ : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞)
  (sInf
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ u) : ℝ≥0∞)})
  0
Tactic: simp only [Measure.inf_apply hu, this, coe_zero, Pi.zero_apply, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hst : Disjoint s t
this : Eq.{u_1 + 1} (α := Measure α) ⊥ 0
u : Set α
hu : MeasurableSet u
h : u.Nonempty
⊢ Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
              ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ u) : ℝ≥0∞)})
    0
have refine : ⊥ =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ u) : ℝ≥0∞)
Tactic: refine csInf_eq_bot_of_bot_mem ⟨t, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE
have tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
Tactic: tfae_have 1 → 2
  | h => h.disjoint
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE
have tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
Tactic: tfae_have 2 → 1
  | h => mutuallySingular_of_disjoint h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE
have tfae_1_to_3 : ∀ (a : μ ⟂ₘ ν), Disjoint (ae μ) (ae ν)
Tactic: tfae_have 1 → 3
  | h => h.disjoint_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
tfae_1_to_3 : ∀ (a : μ ⟂ₘ ν), Disjoint (ae μ) (ae ν)
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE
have tfae_3_to_2 : ∀ (a : Disjoint (ae μ) (ae ν)), Disjoint μ ν
Tactic: tfae_have 3 → 2
  | h => disjoint_of_disjoint_ae h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃₀ s) μ
have rw : NullMeasurableSet (⋃ i ∈ s, i) μ
Tactic: rw [sUnion_eq_biUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
have rcases : ∀ (t : Set α) (htm : MeasurableSet t) (hst : s =ᶠ[ae μ] t), ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
Tactic: rcases h with ⟨t, htm, hst⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
have refine_1 : t ∪ toMeasurable μ (s \ t) ⊇ s
Tactic: refine ⟨t ∪ toMeasurable μ (s \ t), ?_, htm.union (measurableSet_toMeasurable _ _), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
refine_1 : t ∪ toMeasurable μ (s \ t) ⊇ s
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
have refine_2 : t ∪ toMeasurable μ (s \ t) =ᶠ[ae μ] s
Tactic: refine ⟨t ∪ toMeasurable μ (s \ t), ?_, htm.union (measurableSet_toMeasurable _ _), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (hypothesis)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ t ∪ toMeasurable μ (s \ t) =ᶠ[ae μ] s
have this : toMeasurable μ (s \ t) =ᶠ[ae μ] ∅
Tactic: have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ toMeasurable μ s =ᶠ[ae μ] s
have rw : sorry.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s) =ᶠ[ae μ] s
Tactic: rw [toMeasurable_def, dif_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
rw : ⋯.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s) =ᶠ[ae μ] s
⊢ toMeasurable μ s =ᶠ[ae μ] s
have hc : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
Tactic: rw [toMeasurable_def, dif_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
⊢ ∃ (t : ι → Set α),
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
have choose : ∀ (t : (i : ι) → Set α) (ht_sub : ∀ (i : ι), t i ⊆ s i) (htm : ∀ (i : ι), MeasurableSet (t i))
  (ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i),
  ∃ (t : ι → Set α),
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
Tactic: choose t ht_sub htm ht_eq using fun i => exists_measurable_subset_ae_eq (h i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : (i : ι) → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i
⊢ ∃ (t : ι → Set α),
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
have rcases : ∀ (u : ι → Set α) (hum : ∀ (i : ι), MeasurableSet (u i))
  (hu₀ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u i) : ℝ≥0∞) (0 : ℝ≥0∞))
  (hud : Pairwise.{u_1} (α := ι) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ s i \ u i)),
  ∃ (t : ι → Set α),
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
Tactic: rcases exists_null_pairwise_disjoint_diff hd with ⟨u, hum, hu₀, hud⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (∑' (i : ι), extend (P := MeasurableSet) (fun (t : Set α) (_ht : MeasurableSet t) ↦ (μ : (a : Set α) → ℝ≥0∞) t) (f i))
  (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i))
Tactic: rw [measure_eq_extend (MeasurableSet.iUnion h),
    extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
rw :
  Eq (α := ℝ≥0∞)
    (∑' (i : ι),
      extend (P := MeasurableSet) (fun (t : Set α) (_ht : MeasurableSet t) ↦ (μ : (a : Set α) → ℝ≥0∞) t) (f i))
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i))
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [measure_eq_extend (MeasurableSet.iUnion h),
    extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
rw :
  Eq (α := ℝ≥0∞)
    (∑' (i : ι),
      extend (P := MeasurableSet) (fun (t : Set α) (_ht : MeasurableSet t) ↦ (μ : (a : Set α) → ℝ≥0∞) t) (f i))
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i))
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have rw₂ : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
  Pairwise (Disjoint on f) →
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: rw [measure_eq_extend (MeasurableSet.iUnion h),
    extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
have rcases : ∀ (t : ι → Set α) (_ht_sub : ∀ (i : ι), t i ⊆ f i) (ht_eq : ∀ (i : ι), f i =ᶠ[ae μ] t i)
  (htm : ∀ (i : ι), MeasurableSet (t i)) (htd : Pairwise (Disjoint on t)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.NullMeasurable (goal)
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have hd₁ : Pairwise (α := Bool) (AEDisjoint μ on fun (b : Bool) ↦ bif b then s else t)
Tactic: rw [union_eq_iUnion, measure_iUnion₀, tsum_fintype, Fintype.sum_bool, cond, cond]