awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) h.nullSetᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
h.choose_spec.2.2

Premises used: Exists.choose_spec, Set.Mem, setOf, MeasureTheory.Measure.MutuallySingular.nullSet, And.right
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ μ.restrict h.nullSet = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ ν.restrict h.nullSetᶜ = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ⟂ₘ 0

Tactic:
⟨∅, MeasurableSet.empty, measure_empty, rfl⟩

Premises used: MeasurableSet.empty, MeasureTheory.measure_empty, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro, EmptyCollection.emptyCollection, rfl
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : ν ⟂ₘ μ
⊢ μ ⟂ₘ ν

Tactic:
let ⟨i, hi, his, hit⟩ := h
  ⟨iᶜ, hi.compl, hit, (compl_compl i).symm ▸ his⟩

Premises used: compl_compl, Compl.compl, Eq.rec, MeasurableSet.compl, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro, _private.0.MeasureTheory.Measure.MutuallySingular.symm.match_1, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ μ ⟂ₘ ν ↔ ν ⟂ₘ μ

Tactic:
⟨fun h => h.symm, fun h => h.symm⟩

Premises used: Iff.intro, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ 0 ⟂ₘ μ

Tactic:
zero_right.symm

Premises used: MeasureTheory.Measure.MutuallySingular.zero_right, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν₁ ν₂ : Measure α
h : μ₁ ⟂ₘ ν₁
hμ : μ₂ ≪ μ₁
hν : ν₂ ≪ ν₁
⊢ μ₂ ⟂ₘ ν₂

Tactic:
let ⟨s, hs, h₁, h₂⟩ := h
  ⟨s, hs, hμ h₁, hν h₂⟩

Premises used: MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro, _private.0.MeasureTheory.Measure.MutuallySingular.mono_ac.match_1
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ μ₂ ν ν₂ : Measure α
hμμ₂ : μ ≪ μ₂
hμ₂μ : μ₂ ≪ μ
hνν₂ : ν ≪ ν₂
hν₂ν : ν₂ ≪ ν
⊢ μ ⟂ₘ ν ↔ μ₂ ⟂ₘ ν₂

Tactic:
⟨fun h ↦ h.mono_ac hμ₂μ hν₂ν, fun h ↦ h.mono_ac hμμ₂ hνν₂⟩

Premises used: Iff.intro, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν₁ ν₂ : Measure α
h : μ₁ ⟂ₘ ν₁
hμ : μ₂ ≤ μ₁
hν : ν₂ ≤ ν₁
⊢ μ₂ ⟂ₘ ν₂

Tactic:
h.mono_ac hμ.absolutelyContinuous hν.absolutelyContinuous

Premises used: LE.le.absolutelyContinuous, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
rw : @MutuallySingular.{u_1} α m0 0 0
⊢ μ ⟂ₘ μ

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ @MutuallySingular.{u_1} α m0 0 0

Tactic:
zero_left

Premises used: MeasureTheory.Measure.MutuallySingular.zero_left
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ @MutuallySingular.{u_1} α m0 0 0

Tactic:
exact zero_left

Premises used: MeasureTheory.Measure.MutuallySingular.zero_left
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
refine : μ ⟂ₘ μ → μ = 0
⊢ μ ⟂ₘ μ ↔ μ = 0

Tactic:
refine ⟨?_, fun h ↦ by (rw [h]; exact zero_left)⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : μ = 0), μ = 0
⊢ μ = 0

Tactic:
rwa [measure_univ_eq_zero] at this

Premises used: MeasureTheory.Measure.measure_univ_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
suffices : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0

Tactic:
suffices μ Set.univ = 0 by rwa [measure_univ_eq_zero] at this
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 0
rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 0
rw₃ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
rw₄ rw₅ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← Set.union_compl_self s, measure_union disjoint_compl_right hs.compl, hμs, hμs_compl,
    add_zero]

Premises used: Set.union_compl_self, MeasurableSet.compl, disjoint_compl_right, MeasureTheory.measure_union, add_zero
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
⊢ sum μ ⟂ₘ ν ↔ ∀ (i : ι), μ i ⟂ₘ ν

Tactic:
⟨fun h i => h.mono (le_sum _ _) le_rfl, fun H => ?_⟩

Premises used: le_rfl, MeasureTheory.Measure.MutuallySingular.mono, MeasureTheory.Measure.le_sum, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
refine : ∀ (H : ∀ (i : ι), μ i ⟂ₘ ν), sum μ ⟂ₘ ν
⊢ sum μ ⟂ₘ ν ↔ ∀ (i : ι), μ i ⟂ₘ ν

Tactic:
refine ⟨fun h i => h.mono (le_sum _ _) le_rfl, fun H => ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
H : ∀ (i : ι), μ i ⟂ₘ ν
choose :
  ∀ (s : (i : ι) → Set α) (hsm : ∀ (i : ι), MeasurableSet (s i))
    (hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞))
    (hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), sum μ ⟂ₘ ν
⊢ sum μ ⟂ₘ ν

Tactic:
choose s hsm hsμ hsν using H
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ sum μ ⟂ₘ ν

Tactic:
⟨⋂ i, s i, MeasurableSet.iInter hsm, ?_, ?_⟩

Premises used: Set.iInter, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ sum μ ⟂ₘ ν

Tactic:
refine ⟨⋂ i, s i, MeasurableSet.iInter hsm, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (b : ι), s b) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [sum_apply _ (MeasurableSet.iInter hsm), ENNReal.tsum_eq_zero]

Premises used: MeasureTheory.Measure.sum_apply, MeasurableSet.iInter, ENNReal.tsum_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (b : ι), s b) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun i => measure_mono_null (iInter_subset _ _) (hsμ i)

Premises used: MeasureTheory.measure_mono_null, Set.iInter_subset
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (b : ι), s b) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact fun i => measure_mono_null (iInter_subset _ _) (hsμ i)

Premises used: MeasureTheory.measure_mono_null, Set.iInter_subset
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), (s i)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rwa [compl_iInter, measure_iUnion_null_iff]

Premises used: Set.compl_iInter, MeasureTheory.measure_iUnion_null_iff
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : Countable ι
ν : ι → Measure α
⊢ μ ⟂ₘ sum ν ↔ ∀ (i : ι), μ ⟂ₘ ν i

Tactic:
comm.trans <| sum_left.trans <| forall_congr' fun _ => comm

Premises used: MeasureTheory.Measure.MutuallySingular.comm, forall_congr', Iff.trans, MeasureTheory.Measure.MutuallySingular.sum_left
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
rw : (sum fun (b : Bool) ↦ bif b then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₁ : (∀ (i : Bool), (bif i then μ₁ else μ₂) ⟂ₘ ν) ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₂ : (bif false then μ₁ else μ₂) ⟂ₘ ν ∧ (bif true then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₃ : (bif false then μ₁ else μ₂) ⟂ₘ ν ∧ μ₁ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₄ : μ₂ ⟂ₘ ν ∧ μ₁ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₅ rw₆ : μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν

Tactic:
rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]

Premises used: cond, Bool.forall_bool, MeasureTheory.Measure.sum_cond, and_comm, MeasureTheory.Measure.MutuallySingular.sum_left
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
⊢ μ ⟂ₘ ν₁ + ν₂ ↔ μ ⟂ₘ ν₁ ∧ μ ⟂ₘ ν₂

Tactic:
comm.trans <| add_left_iff.trans <| and_congr comm comm

Premises used: MeasureTheory.Measure.MutuallySingular.comm, MeasureTheory.Measure.MutuallySingular.add_left_iff, Iff.trans, and_congr
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h₁ : ν₁ ⟂ₘ μ
h₂ : ν₂ ⟂ₘ μ
⊢ ν₁ + ν₂ ⟂ₘ μ

Tactic:
add_left_iff.2 ⟨h₁, h₂⟩

Premises used: Iff.mpr, MeasureTheory.Measure.MutuallySingular.add_left_iff, And.intro
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h₁ : μ ⟂ₘ ν₁
h₂ : μ ⟂ₘ ν₂
⊢ μ ⟂ₘ ν₁ + ν₂

Tactic:
add_right_iff.2 ⟨h₁, h₂⟩

Premises used: Iff.mpr, And.intro, MeasureTheory.Measure.MutuallySingular.add_right_iff
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0∞
h : ν ⟂ₘ μ
⊢ r • ν ⟂ₘ μ

Tactic:
h.mono_ac (AbsolutelyContinuous.rfl.smul_left r) AbsolutelyContinuous.rfl

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
h : ν ⟂ₘ μ
⊢ r • ν ⟂ₘ μ

Tactic:
h.smul r

Premises used: ENNReal.ofNNReal, MeasureTheory.Measure.MutuallySingular.smul
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ μ.restrict s ⟂ₘ ν

Tactic:
⟨h.nullSet, h.measurableSet_nullSet, ?_, h.measure_compl_nullSet⟩

Premises used: MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet, MeasureTheory.Measure.MutuallySingular.nullSet, MeasureTheory.Measure.MutuallySingular, And.intro, Exists.intro, MeasureTheory.Measure.MutuallySingular.measure_compl_nullSet
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
refine : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.restrict s ⟂ₘ ν

Tactic:
refine ⟨h.nullSet, h.measurableSet_nullSet, ?_, h.measure_compl_nullSet⟩
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (h.nullSet ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply h.measurableSet_nullSet]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (h.nullSet ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null Set.inter_subset_left h.measure_nullSet

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono_null, MeasureTheory.Measure.MutuallySingular.measure_nullSet
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (h.nullSet ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_mono_null Set.inter_subset_left h.measure_nullSet

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono_null, MeasureTheory.Measure.MutuallySingular.measure_nullSet
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h_ac : μ ≪ ν
h_ms : μ ⟂ₘ ν
rw : μ ⟂ₘ μ
⊢ μ = 0

Tactic:
rw [← Measure.MutuallySingular.self_iff]

Premises used: MeasureTheory.Measure.MutuallySingular.self_iff
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h_ac : μ ≪ ν
h_ms : μ ⟂ₘ ν
⊢ μ ⟂ₘ μ

Tactic:
h_ms.mono_ac Measure.AbsolutelyContinuous.rfl h_ac

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h_ac : μ ≪ ν
h_ms : μ ⟂ₘ ν
⊢ μ ⟂ₘ μ

Tactic:
exact h_ms.mono_ac Measure.AbsolutelyContinuous.rfl h_ac

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
⊢ μ ≪ ν₁

Tactic:
AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
refine :
  ∀ (s : Set α) (hs : MeasurableSet s) (hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ≪ ν₁

Tactic:
refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- 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
⊢ MeasurableSet t

Tactic:
have ht : MeasurableSet t := h_ms.measurableSet_nullSet
-- 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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have htμ : μ t = 0 := h_ms.measure_nullSet
-- 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∞)
⊢ Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have htν₂ : ν₂ tᶜ = 0 := h_ms.measure_compl_nullSet
-- 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∞)
rw : ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞)
| ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← inter_union_compl s t]

Premises used: Set.inter_union_compl
-- 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∞)
conv_lhs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)

Tactic:
conv_lhs => rw [← inter_union_compl s t]

Premises used: Set.inter_union_compl
-- 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∞)
hd : Disjoint (s ∩ t) (s ∩ tᶜ)
h₁ : MeasurableSet (s ∩ tᶜ)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞)

Tactic:
rw [measure_union, measure_inter_null_of_null_right _ htμ, zero_add]

Premises used: zero_add, MeasureTheory.measure_inter_null_of_null_right, MeasureTheory.measure_union
-- 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∞)
⊢ Disjoint (s ∩ t) (s ∩ tᶜ)

Tactic:
(disjoint_compl_right.inter_right' _).inter_left' _

Premises used: Disjoint.inter_left', disjoint_compl_right, Disjoint.inter_right'
-- 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∞)
⊢ Disjoint (s ∩ t) (s ∩ tᶜ)

Tactic:
exact (disjoint_compl_right.inter_right' _).inter_left' _

Premises used: Disjoint.inter_left', disjoint_compl_right, Disjoint.inter_right'
-- 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∞)
⊢ MeasurableSet (s ∩ tᶜ)

Tactic:
hs.inter ht.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- 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∞)
⊢ MeasurableSet (s ∩ tᶜ)

Tactic:
exact hs.inter ht.compl

Premises used: MeasurableSet.compl, MeasurableSet.inter
-- 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∞)
⊢ 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