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 : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
htν₂ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
| ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
Tactic: rw [← inter_union_compl s t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
htν₂ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)
have conv_lhs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)
Tactic: conv_lhs => rw [← inter_union_compl s t]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
htν₂ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)
have hd : Disjoint (s ∩ t) (s ∩ tᶜ)
Tactic: rw [measure_union, measure_inter_null_of_null_right _ htμ, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
htν₂ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hd : Disjoint (s ∩ t) (s ∩ tᶜ)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)
have h₁ : MeasurableSet (s ∩ tᶜ)
Tactic: rw [measure_union, measure_inter_null_of_null_right _ htμ, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
htν₂ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)
Tactic: have : μ s = μ (s ∩ tᶜ) := by
    conv_lhs => rw [← inter_union_compl s t]
    rw [measure_union, measure_inter_null_of_null_right _ htμ, zero_add]
    · exact (disjoint_compl_right.inter_right' _).inter_left' _
    · exact hs.inter ht.compl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
htν₂ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
htν₂ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : Eq (α := ℝ≥0∞) ((ν₁ + ν₂ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine h ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
htν₂ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν₁ + ν₂ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
  Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [Measure.coe_add, Pi.add_apply, add_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ @MutuallySingular _ x (map f μ) (map f ν)
have refine_1 : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨f '' hμν.nullSet, hf.measurableSet_image' hμν.measurableSet_nullSet, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
refine_1 : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ @MutuallySingular _ x (map f μ) (map f ν)
have refine_2 : Eq (α := ℝ≥0∞) (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨f '' hμν.nullSet, hf.measurableSet_image' hμν.measurableSet_nullSet, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' hμν.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [hf.map_apply, hf.injective.preimage_image, hμν.measure_nullSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' hμν.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) hμν.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [hf.map_apply, hf.injective.preimage_image, hμν.measure_nullSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' hμν.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) hμν.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1₂ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [hf.map_apply, hf.injective.preimage_image, hμν.measure_nullSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ Eq (α := ℝ≥0∞) (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f ⁻¹' (f '' hμν.nullSet)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [hf.map_apply, Set.preimage_compl, hf.injective.preimage_image, hμν.measure_compl_nullSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f ⁻¹' (f '' hμν.nullSet)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [hf.map_apply, Set.preimage_compl, hf.injective.preimage_image, hμν.measure_compl_nullSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f ⁻¹' (f '' hμν.nullSet)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2₂ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) hμν.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [hf.map_apply, Set.preimage_compl, hf.injective.preimage_image, hμν.measure_compl_nullSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f ⁻¹' (f '' hμν.nullSet)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2₁ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2₂ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) hμν.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2₃ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [hf.map_apply, Set.preimage_compl, hf.injective.preimage_image, hμν.measure_compl_nullSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : Eq (α := ℝ≥0∞) ((μ ⊓ ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ 2 * (↑ε : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞)
  (sInf
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m = HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
  0
Tactic: simp_rw [Measure.inf_apply MeasurableSet.univ, inter_univ] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ :
  Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
    0
n : ℕ
⊢ ∃ (x : ℝ≥0∞),
    Membership.mem (γ := Set ℝ≥0∞)
        {m : ℝ≥0∞ |
          ∃ (t : Set α),
            m =
              HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
                ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)}
        x ∧
      x < (↑ε : ℝ≥0∞) * (1 / 2) ^ n
have refine : (↑ε : ℝ≥0∞) ≠ 0
Tactic: refine exists_lt_of_csInf_lt ⟨ν univ, ∅, by simp⟩ <| h₁ ▸ ENNReal.mul_pos ?_ (by simp)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ :
  Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
    0
n : ℕ
⊢ (↑ε : ℝ≥0∞) ≠ 0
have norm_cast : ¬ε = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ :
  Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
    0
n : ℕ
⊢ ∃ (t : Set α),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) <
      (↑ε : ℝ≥0∞) * (1 / 2) ^ n
have obtain : ∀ (t : Set α)
  (hm₂ :
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) <
      (↑ε : ℝ≥0∞) * (1 / 2) ^ n),
  ∃ (t : Set α),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) <
      (↑ε : ℝ≥0∞) * (1 / 2) ^ n
Tactic: obtain ⟨m, ⟨t, ht₁, rfl⟩, hm₂⟩ :
        ∃ x ∈ {m | ∃ t, m = μ t + ν tᶜ}, x < ε * (1 / 2 : ℝ≥0∞) ^ n := by
      refine exists_lt_of_csInf_lt ⟨ν univ, ∅, by simp⟩ <| h₁ ▸ ENNReal.mul_pos ?_ (by simp)
      norm_cast
      exact hε.ne.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ :
  Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
    0
⊢ ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ 2 * (↑ε : ℝ≥0∞)
have h₂ : ∀ (n : ℕ),
  ∃ (t : Set α),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) <
      (↑ε : ℝ≥0∞) * (1 / 2) ^ n
Tactic: have h₂ : ∀ n : ℕ, ∃ t, μ t + ν tᶜ < ε * (1 / 2) ^ n := by
    intro n
    obtain ⟨m, ⟨t, ht₁, rfl⟩, hm₂⟩ :
        ∃ x ∈ {m | ∃ t, m = μ t + ν tᶜ}, x < ε * (1 / 2 : ℝ≥0∞) ^ n := by
      refine exists_lt_of_csInf_lt ⟨ν univ, ∅, by simp⟩ <| h₁ ▸ ENNReal.mul_pos ?_ (by simp)
      norm_cast
      exact hε.ne.symm
    exact ⟨t, hm₂⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ :
  Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
    0
h₂ :
  ∀ (n : ℕ),
    ∃ (t : Set α),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) <
        (↑ε : ℝ≥0∞) * (1 / 2) ^ n
⊢ ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ 2 * (↑ε : ℝ≥0∞)
have choose : ∀ (t : (n : ℕ) → Set α)
  (ht₂ :
    ∀ (n : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞)
          ((ν : (a : Set α) → ℝ≥0∞) (t n)ᶜ : ℝ≥0∞) <
        (↑ε : ℝ≥0∞) * (1 / 2) ^ n),
  ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ 2 * (↑ε : ℝ≥0∞)
Tactic: choose t ht₂ using h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ :
  Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
    0
t : (n : ℕ) → Set α
ht₂ :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t n)ᶜ : ℝ≥0∞) <
      (↑ε : ℝ≥0∞) * (1 / 2) ^ n
⊢ ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ 2 * (↑ε : ℝ≥0∞)
have refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨⋂ n, t n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ :
  Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
    0
t : (n : ℕ) → Set α
ht₂ :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t n)ᶜ : ℝ≥0∞) <
      (↑ε : ℝ≥0∞) * (1 / 2) ^ n
refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ 2 * (↑ε : ℝ≥0∞)
have refine_2 : (ν : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n)ᶜ ≤ 2 * (↑ε : ℝ≥0∞)
Tactic: refine ⟨⋂ n, t n, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ :
  Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
    0
t : (n : ℕ) → Set α
ht₂ :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t n)ᶜ : ℝ≥0∞) <
      (↑ε : ℝ≥0∞) * (1 / 2) ^ n
⊢ (ν : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n)ᶜ ≤ 2 * (↑ε : ℝ≥0∞)
have refine_2 : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (t i)ᶜ) : ℝ≥0∞) (∑' (n : ℕ), (↑ε : ℝ≥0∞) * (1 / 2) ^ n : ℝ≥0∞)
Tactic: rw [compl_iInter, (by simp [ENNReal.tsum_mul_left, mul_comm] :
      2 * (ε : ℝ≥0∞) = ∑' (n : ℕ), ε * (1 / 2 : ℝ≥0∞) ^ n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ :
  Eq (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)})
    0
t : (n : ℕ) → Set α
ht₂ :
  ∀ (n : ℕ),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t n) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t n)ᶜ : ℝ≥0∞) <
      (↑ε : ℝ≥0∞) * (1 / 2) ^ n
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (t i)ᶜ) : ℝ≥0∞) (∑' (n : ℕ), (↑ε : ℝ≥0∞) * (1 / 2) ^ n : ℝ≥0∞)
have refine_2 : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (ν : (a : Set α) → ℝ≥0∞) (t i)ᶜ) (∑' (n : ℕ), (↑ε : ℝ≥0∞) * (1 / 2) ^ n)
Tactic: refine (measure_iUnion_le _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
⊢ ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ (1 / 2) ^ n
have h₁ : ∀ (x : Set α), (1 / 2) ^ n = 2 * (↑((1 / 2) ^ (n + 1)) : ℝ≥0∞)
Tactic: convert!
      exists_null_set_measure_lt_of_disjoint h (ε := (1 / 2) ^ (n + 1)) <| pow_pos (by simp) (n + 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x : Set α
| (1 / 2) ^ n = 2 * (↑((1 / 2) ^ (n + 1)) : ℝ≥0∞)
have enter : 1 / 2
Tactic: enter [1, 1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x : Set α
| (1 / 2) ^ n = 2 * (↑((1 / 2) ^ (n + 1)) : ℝ≥0∞)
have enter : (1 / 2) ^ n
Tactic: enter [1, 1]
      equals ((1 : ℝ≥0) / (2 : ℝ≥0)) => rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x : Set α
enter : (1 / 2) ^ n
| (1 / 2) ^ n = 2 * (↑((1 / 2) ^ (n + 1)) : ℝ≥0∞)
have enter₁ : 1 / 2
Tactic: enter [1, 1]
      equals ((1 : ℝ≥0) / (2 : ℝ≥0)) => rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x : Set α
⊢ ((↑1 : ℝ≥0∞) / (↑2 : ℝ≥0∞)) ^ n = 2 * (↑((1 / 2) ^ (n + 1)) : ℝ≥0∞)
have h₁ : HDiv.hDiv (α := ℝ≥0) 1 2 ^ n = 2 * HDiv.hDiv (α := ℝ≥0) 1 2 ^ (n + 1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
⊢ μ ⟂ₘ ν
have h' : ∀ (n : ℕ),
  ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ (1 / 2) ^ n
Tactic: have h' (n : ℕ) : ∃ s, μ s = 0 ∧ ν sᶜ ≤ (1 / 2) ^ n := by
    convert!
      exists_null_set_measure_lt_of_disjoint h (ε := (1 / 2) ^ (n + 1)) <| pow_pos (by simp) (n + 1)
    conv =>
      -- this tweak is needed due to the known issue of `norm_cast` with numeric fractions
      enter [1, 1]
      equals ((1 : ℝ≥0) / (2 : ℝ≥0)) => rfl
    norm_cast
    ring
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
h' :
  ∀ (n : ℕ),
    ∃ (s : Set α),
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ (1 / 2) ^ n
⊢ μ ⟂ₘ ν
have choose : ∀ (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), μ ⟂ₘ ν
Tactic: choose s hs₂ hs₃ using h'
Cleared hypotheses: h'
-- 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
⊢ μ ⟂ₘ ν
have refine_1 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine Measure.MutuallySingular.mk (t := (⋃ n, s n)ᶜ) (measure_iUnion_null hs₂) ?_ ?_
-- 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
refine_1 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ⟂ₘ ν
have refine_2 : Subset.{u_1} (α := Set α) univ ((⋃ (i : ℕ), s i) ∪ (⋃ (n : ℕ), s n)ᶜ)
Tactic: refine Measure.MutuallySingular.mk (t := (⋃ n, s n)ᶜ) (measure_iUnion_null hs₂) ?_ ?_