awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)

Tactic:
h ?_
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)
refine : Eq (α := ℝ≥0∞) ((ν₁ + ν₂ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine h ?_
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)
simp :
  Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    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]

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply, add_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞) ∧
    Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨measure_inter_null_of_null_left _ hs_zero, measure_inter_null_of_null_right _ htν₂⟩

Premises used: MeasureTheory.measure_inter_null_of_null_right, And.intro, MeasureTheory.measure_inter_null_of_null_left
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞) ∧
    Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ⟨measure_inter_null_of_null_left _ hs_zero, measure_inter_null_of_null_right _ htν₂⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
hμν : μ ⟂ₘ ν
⊢ @MutuallySingular _ x (map f μ) (map f ν)

Tactic:
⟨f '' hμν.nullSet, hf.measurableSet_image' hμν.measurableSet_nullSet, ?_, ?_⟩

Premises used: MeasurableEmbedding.measurableSet_image', MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet, MeasureTheory.Measure.MutuallySingular.nullSet, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro, Set.image
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)
refine_2 : Eq (α := ℝ≥0∞) (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ @MutuallySingular _ x (map f μ) (map f ν)

Tactic:
refine ⟨f '' hμν.nullSet, hf.measurableSet_image' hμν.measurableSet_nullSet, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)
refine_1₂ refine_1₃ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [hf.map_apply, hf.injective.preimage_image, hμν.measure_nullSet]

Premises used: MeasureTheory.Measure.MutuallySingular.measure_nullSet, MeasurableEmbedding.injective, MeasurableEmbedding.map_apply, Function.Injective.preimage_image
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)
refine_2₃ refine_2₄ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) (((map f ν : Measure β) : (a : Set β) → ℝ≥0∞) (f '' hμν.nullSet)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [hf.map_apply, Set.preimage_compl, hf.injective.preimage_image, hμν.measure_compl_nullSet]

Premises used: MeasurableEmbedding.injective, MeasurableEmbedding.map_apply, Function.Injective.preimage_image, MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet, Set.preimage_compl
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
ε : ℝ≥0
hε : 0 < ε
h₁ : Eq (α := ℝ≥0∞) ((μ ⊓ ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 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₁

Premises used: Set.inter_univ, MeasureTheory.Measure.inf_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 : ℕ
⊢ (ν : (a : Set α) → ℝ≥0∞) univ =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ᶜ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 : ℕ
⊢ (1 / 2) ^ n ≠ 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 : ℕ
refine : (↑ε : ℝ≥0∞) ≠ 0
⊢ ∃ (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

Tactic:
refine exists_lt_of_csInf_lt ⟨ν univ, ∅, by simp⟩ <| h₁ ▸ ENNReal.mul_pos ?_ (by simp)
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 : ℕ
norm_cast : ¬ε = 0
⊢ (↑ε : ℝ≥0∞) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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

Tactic:
hε.ne.symm

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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

Tactic:
exact hε.ne.symm

Premises used: Ne.symm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 : ℕ
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
⊢ ∃ (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

Premises used: HDiv.hDiv, OfNat.ofNat, rfl
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 α
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:
⟨t, hm₂⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 α
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:
exact ⟨t, hm₂⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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

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₂⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
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∞)
⊢ ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ 2 * (↑ε : ℝ≥0∞)

Tactic:
choose t ht₂ using h₂
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)

Tactic:
⟨⋂ n, t n, ?_, ?_⟩

Premises used: Set.iInter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)
refine_2 : (ν : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n)ᶜ ≤ 2 * (↑ε : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ 2 * (↑ε : ℝ≥0∞)

Tactic:
refine ⟨⋂ n, t n, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
⊢ 1 / 2 < 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine eq_zero_of_le_mul_pow (by simp)
      fun n ↦ ((measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans
      (le_add_right le_rfl)).trans (ht₂ n).le

Premises used: le_rfl, LT.lt.le, ENNReal.eq_zero_of_le_mul_pow, Set.iInter_subset_of_subset, MeasureTheory.measure_mono, LE.le.trans, le_add_right
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
⊢ 2 * (↑ε : ℝ≥0∞) = ∑' (n : ℕ), (↑ε : ℝ≥0∞) * (1 / 2) ^ n

Tactic:
simp [ENNReal.tsum_mul_left, mul_comm]

Premises used: ENNReal.tsum_mul_left, mul_comm
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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_2 :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (t i)ᶜ) : ℝ≥0∞) (∑' (n : ℕ), (↑ε : ℝ≥0∞) * (1 / 2) ^ n : ℝ≥0∞)
⊢ (ν : (a : Set α) → ℝ≥0∞) (⋂ (n : ℕ), t n)ᶜ ≤ 2 * (↑ε : ℝ≥0∞)

Tactic:
rw [compl_iInter, (by simp [ENNReal.tsum_mul_left, mul_comm] :
      2 * (ε : ℝ≥0∞) = ∑' (n : ℕ), ε * (1 / 2 : ℝ≥0∞) ^ n)]

Premises used: Set.compl_iInter
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)

Tactic:
(measure_iUnion_le _).trans ?_

Premises used: MeasureTheory.measure_iUnion_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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_2 : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), (ν : (a : Set α) → ℝ≥0∞) (t i)ᶜ) (∑' (n : ℕ), (↑ε : ℝ≥0∞) * (1 / 2) ^ n)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), (t i)ᶜ) : ℝ≥0∞) (∑' (n : ℕ), (↑ε : ℝ≥0∞) * (1 / 2) ^ n : ℝ≥0∞)

Tactic:
refine (measure_iUnion_le _).trans ?_

Premises used: MeasureTheory.measure_iUnion_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞) (∑' (i : ℕ), (ν : (a : Set α) → ℝ≥0∞) (t i)ᶜ) (∑' (n : ℕ), (↑ε : ℝ≥0∞) * (1 / 2) ^ n)

Tactic:
ENNReal.summable.tsum_le_tsum (fun n ↦ (le_add_left le_rfl).trans (ht₂ n).le)
      ENNReal.summable

Premises used: le_rfl, ENNReal.summable, LT.lt.le, Summable.tsum_le_tsum, LE.le.trans, le_add_left
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞) (∑' (i : ℕ), (ν : (a : Set α) → ℝ≥0∞) (t i)ᶜ) (∑' (n : ℕ), (↑ε : ℝ≥0∞) * (1 / 2) ^ n)

Tactic:
exact ENNReal.summable.tsum_le_tsum (fun n ↦ (le_add_left le_rfl).trans (ht₂ n).le)
      ENNReal.summable

Premises used: le_rfl, ENNReal.summable, LT.lt.le, Summable.tsum_le_tsum, LE.le.trans, le_add_left
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
⊢ 0 < 1 / 2

Tactic:
simp