awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
h₁ : ∀ (x : Set α), (1 / 2) ^ n = 2 * (↑((1 / 2) ^ (n + 1)) : ℝ≥0∞)
⊢ ∃ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (ν : (a : Set α) → ℝ≥0∞) sᶜ ≤ (1 / 2) ^ n

Tactic:
convert!
      exists_null_set_measure_lt_of_disjoint h (ε := (1 / 2) ^ (n + 1)) <| pow_pos (by simp) (n + 1)

Premises used: pow_pos, HAdd.hAdd, MeasureTheory.Measure.exists_null_set_measure_lt_of_disjoint, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x : Set α
enter : 1 / 2
| (1 / 2) ^ n = 2 * (↑((1 / 2) ^ (n + 1)) : ℝ≥0∞)

Tactic:
enter [1, 1]
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x : Set α
⊢ 1 / 2 = (↑1 : ℝ≥0∞) / (↑2 : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x : Set α
enter : (1 / 2) ^ n
enter₁ : 1 / 2
| (1 / 2) ^ n = 2 * (↑((1 / 2) ^ (n + 1)) : ℝ≥0∞)

Tactic:
enter [1, 1]
      equals ((1 : ℝ≥0) / (2 : ℝ≥0)) => rfl

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x : Set α
h₁ : HDiv.hDiv (α := ℝ≥0) 1 2 ^ n = 2 * HDiv.hDiv (α := ℝ≥0) 1 2 ^ (n + 1)
⊢ ((↑1 : ℝ≥0∞) / (↑2 : ℝ≥0∞)) ^ n = 2 * (↑((1 / 2) ^ (n + 1)) : ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint μ ν
n : ℕ
x : Set α
⊢ HDiv.hDiv (α := ℝ≥0) 1 2 ^ n = 2 * HDiv.hDiv (α := ℝ≥0) 1 2 ^ (n + 1)

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

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
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
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'
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
⊢ μ ⟂ₘ ν

Tactic:
Measure.MutuallySingular.mk (t := (⋃ n, s n)ᶜ) (measure_iUnion_null hs₂) ?_ ?_

Premises used: MeasureTheory.measure_iUnion_null, MeasureTheory.Measure.MutuallySingular.mk
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞)
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₂) ?_ ?_

Premises used: MeasureTheory.measure_iUnion_null, MeasureTheory.Measure.MutuallySingular.mk
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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∞) (⋂ (i : ℕ), (s i)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s n)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [compl_iUnion]

Premises used: Set.compl_iUnion
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
⊢ 1 / 2 < 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 : ∀ (n : ℕ), (ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), (s i)ᶜ) ≤ (↑1 : ℝ≥0∞) * (1 / 2) ^ n
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), (s i)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine eq_zero_of_le_mul_pow (ε := 1) (by simp : (1 / 2 : ℝ≥0∞) < 1) <| fun n ↦ ?_

Premises used: ENNReal.eq_zero_of_le_mul_pow
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 : ℕ
refine_1 : (ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), (s i)ᶜ) ≤ (1 / 2) ^ n
⊢ (ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ℕ), (s i)ᶜ) ≤ (↑1 : ℝ≥0∞) * (1 / 2) ^ n

Tactic:
rw [ENNReal.coe_one, one_mul]

Premises used: ENNReal.coe_one, one_mul
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 / 2) ^ n

Tactic:
(measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans (hs₃ n)

Premises used: Set.iInter_subset_of_subset, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 / 2) ^ n

Tactic:
exact (measure_mono <| iInter_subset_of_subset n fun _ ht ↦ ht).trans (hs₃ n)

Premises used: Set.iInter_subset_of_subset, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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_2 refine_2₁ : Subset.{u_1} (α := Set α) univ univ
⊢ Subset.{u_1} (α := Set α) univ ((⋃ (i : ℕ), s i) ∪ (⋃ (n : ℕ), s n)ᶜ)

Tactic:
rw [union_compl_self]

Premises used: Set.union_compl_self
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
ξ : Measure α
rw : ξ = ⊥ ↔ ξ = 0
⊢ ξ ≤ ⊥ ↔ ξ = 0

Tactic:
rw [le_bot_iff]

Premises used: le_bot_iff
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
ξ : Measure α
⊢ ξ = ⊥ ↔ ξ = 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0

Tactic:
have h_bot_iff (ξ : Measure α) : ξ ≤ ⊥ ↔ ξ = 0 := by
    rw [le_bot_iff]
    rfl
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
rw : ξ = 0
⊢ ξ ≤ ⊥

Tactic:
rw [h_bot_iff]
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
h₁ :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ξ = 0

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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ᶜ)
h₃ : MeasurableSet (s ∩ h.nullSetᶜ)
⊢ Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← inter_union_compl s h.nullSet, measure_union, add_eq_zero]

Premises used: MeasureTheory.Measure.MutuallySingular.nullSet, Set.inter_union_compl, MeasureTheory.measure_union, add_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 ∩ h.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) (s ∩ h.nullSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨measure_inter_null_of_null_right _ <| absolutelyContinuous_of_le hξμ h.measure_nullSet,
      measure_inter_null_of_null_right _ <| absolutelyContinuous_of_le hξν h.measure_compl_nullSet⟩

Premises used: MeasureTheory.Measure.MutuallySingular.measure_nullSet, MeasureTheory.measure_inter_null_of_null_right, And.intro, MeasureTheory.Measure.absolutelyContinuous_of_le, MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 ∩ h.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((ξ : (a : Set α) → ℝ≥0∞) (s ∩ h.nullSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ⟨measure_inter_null_of_null_right _ <| absolutelyContinuous_of_le hξμ h.measure_nullSet,
      measure_inter_null_of_null_right _ <| absolutelyContinuous_of_le hξν h.measure_compl_nullSet⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ Disjoint (s ∩ h.nullSet) (s ∩ h.nullSetᶜ)

Tactic:
Disjoint.mono inter_subset_right inter_subset_right disjoint_compl_right

Premises used: disjoint_compl_right, Disjoint.mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ Disjoint (s ∩ h.nullSet) (s ∩ h.nullSetᶜ)

Tactic:
exact Disjoint.mono inter_subset_right inter_subset_right disjoint_compl_right

Premises used: disjoint_compl_right, Disjoint.mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (s ∩ h.nullSetᶜ)

Tactic:
hs.inter h.measurableSet_nullSet.compl

Premises used: MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet, MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
h_bot_iff : ∀ (ξ : Measure α), ξ ≤ ⊥ ↔ ξ = 0
ξ : Measure α
hξμ : ξ ≤ μ
hξν : ξ ≤ ν
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet (s ∩ h.nullSetᶜ)

Tactic:
exact hs.inter h.measurableSet_nullSet.compl

Premises used: MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet, MeasurableSet.compl, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
rw : ae μ ⊓ ae ν ≤ ⊥
⊢ Disjoint (ae μ) (ae ν)

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
_ : Membership.mem (γ := Filter α) ⊥ s → s ∈ ae μ ⊓ ae ν
⊢ Membership.mem (γ := Filter α) ⊥ s → s ∈ ae μ ⊓ ae ν

Tactic:
_
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
⊢ s ∈ ae μ ⊓ ae ν

Tactic:
⟨s ∪ h.nullSetᶜ, ?_, s ∪ h.nullSet, ?_, ?_⟩

Premises used: Set.Mem, Compl.compl, setOf, MeasureTheory.Measure.MutuallySingular.nullSet, And.intro, Exists.intro, Union.union
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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 ν
refine_3 : s = (s ∪ h.nullSetᶜ) ∩ (s ∪ h.nullSet)
⊢ s ∈ ae μ ⊓ ae ν

Tactic:
refine ⟨s ∪ h.nullSetᶜ, ?_, s ∪ h.nullSet, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sᶜ ∩ h.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s ∪ h.nullSetᶜ ∈ ae μ

Tactic:
rw [mem_ae_iff, compl_union, compl_compl]

Premises used: Set.compl_union, compl_compl, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sᶜ ∩ h.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_inter_null_of_null_right _ h.measure_nullSet

Premises used: MeasureTheory.Measure.MutuallySingular.measure_nullSet, MeasureTheory.measure_inter_null_of_null_right
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sᶜ ∩ h.nullSet) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_inter_null_of_null_right _ h.measure_nullSet

Premises used: MeasureTheory.Measure.MutuallySingular.measure_nullSet, MeasureTheory.measure_inter_null_of_null_right
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (sᶜ ∩ h.nullSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s ∪ h.nullSet ∈ ae ν

Tactic:
rw [mem_ae_iff, compl_union]

Premises used: Set.compl_union, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (sᶜ ∩ h.nullSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_inter_null_of_null_right _ h.measure_compl_nullSet

Premises used: MeasureTheory.measure_inter_null_of_null_right, MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
h_1 : Membership.mem (γ := Filter α) ⊥ s
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (sᶜ ∩ h.nullSetᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_inter_null_of_null_right _ h.measure_compl_nullSet

Premises used: MeasureTheory.measure_inter_null_of_null_right, MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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ᶜᶜ
refine_3₅ refine_3₆ : s = s
⊢ 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]

Premises used: Set.compl_union, compl_compl, Set.inter_union_compl, Set.union_eq_compl_compl_inter_compl
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : Disjoint (ae μ) (ae ν)
⊢ ∃ (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

Premises used: Filter.disjoint_iff, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
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 μ ν
⊢ Disjoint μ ν

Tactic:
obtain ⟨s, hs, t, ht, hst⟩ := h
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
rw : μ ⊓ ν ≤ ⊥
⊢ Disjoint μ ν

Tactic:
rw [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
⊢ Eq.{u_1 + 1} (α := Measure α) ⊥ 0

Tactic:
have : (⊥ : Measure α) = 0 := rfl
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
⊢ μ ⊓ ν ≤ ⊥

Tactic:
Measure.le_intro fun u hu _ ↦ ?_

Premises used: MeasureTheory.Measure.le_intro
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
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 _ ↦ ?_

Premises used: MeasureTheory.Measure.le_intro
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
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
⊢ LE.le (α := ℝ≥0∞) ((μ ⊓ ν : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (((⊥ : Measure α) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)

Tactic:
simp only [Measure.inf_apply hu, this, coe_zero, Pi.zero_apply, nonpos_iff_eq_zero]

Premises used: Pi.zero_apply, MeasureTheory.Measure.inf_apply, MeasureTheory.Measure.coe_zero, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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

Tactic:
csInf_eq_bot_of_bot_mem ⟨t, ?_⟩

Premises used: csInf_eq_bot_of_bot_mem, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
refine :
  ⊥ =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ u) : ℝ≥0∞)
⊢ 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:
refine csInf_eq_bot_of_bot_mem ⟨t, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
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
⊢ ⊥ =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ u) : ℝ≥0∞)

Tactic:
simp [measure_mono_null (inter_subset_left.trans hst.subset_compl_left) hs,
    measure_mono_null inter_subset_left ht]

Premises used: HasSubset.Subset.trans, Set.inter_subset_left, MeasureTheory.measure_mono_null, Disjoint.subset_compl_left
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ μ ⟂ₘ ν

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ Disjoint μ ν

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ ∀ (a : μ ⟂ₘ ν), Disjoint μ ν

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false