awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
Measure.le_add_left le_rfl

Premises used: le_rfl, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
exact Measure.le_add_left le_rfl

Premises used: le_rfl, MeasureTheory.Measure.le_add_left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
hl : ¬μ.HaveLebesgueDecomposition ν
neg : 0 ≤ μ
⊢ ν.withDensity (μ.rnDeriv ν) ≤ μ

Tactic:
rw [rnDeriv, dif_neg hl, withDensity_zero]

Premises used: MeasureTheory.withDensity_zero, MeasureTheory.Measure.rnDeriv, dif_neg
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
ν : Measure α
⊢ AEMeasurable f (μ.singularPart ν)

Tactic:
AEMeasurable.mono_measure hf (Measure.singularPart_le _ _)

Premises used: MeasureTheory.Measure.singularPart_le, AEMeasurable.mono_measure
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
x : MeasurableSpace β
f : α → β
hf : AEMeasurable f μ
ν : Measure α
⊢ AEMeasurable f (ν.withDensity (μ.rnDeriv ν))

Tactic:
AEMeasurable.mono_measure hf (Measure.withDensity_rnDeriv_le _ _)

Premises used: MeasureTheory.Measure.withDensity_rnDeriv_le, AEMeasurable.mono_measure
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
ν' : Measure α
⊢ μ.singularPart ν' ⟂ₘ ν

Tactic:
h.mono (singularPart_le μ ν') le_rfl

Premises used: le_rfl, MeasureTheory.Measure.MutuallySingular.mono, MeasureTheory.Measure.singularPart_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν
⊢ μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)

Tactic:
rw [haveLebesgueDecomposition_add ν μ] at hμν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
⊢ μ ≪ μ.withDensity (ν.rnDeriv μ)

Tactic:
AbsolutelyContinuous.mk (fun s _ hνs ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
refine :
  ∀ (s : Set α),
    MeasurableSet s →
      ∀ (hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ≪ μ.withDensity (ν.rnDeriv μ)

Tactic:
refine AbsolutelyContinuous.mk (fun s _ hνs ↦ ?_)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.mk
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
obtain :
  ∀ (t : Set α),
    MeasurableSet t →
      ∀ (ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞))
        (ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
obtain ⟨t, _, ht1, ht2⟩ := mutuallySingular_singularPart ν μ

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← inter_union_compl s, ← nonpos_iff_eq_zero]

Premises used: Set.inter_union_compl, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t ∪ s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(measure_union_le (s ∩ t) (s ∩ tᶜ)).trans ?_

Premises used: Compl.compl, Inter.inter, LE.le.trans, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
simp :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) ≤
    0

Tactic:
simp only [nonpos_iff_eq_zero, add_eq_zero]

Premises used: add_eq_zero, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left_1 : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
left : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
right : 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:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
hμν ?_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left_1 : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
left : Eq (α := ℝ≥0∞) ((ν.singularPart μ + μ.withDensity (ν.rnDeriv μ) : (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.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left_1 : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
left :
  Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.singularPart μ + μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [coe_add, Pi.add_apply, add_eq_zero]

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply, add_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left_1 : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
left : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
left₁ : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null Set.inter_subset_right ht1

Premises used: MeasureTheory.measure_mono_null, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_mono_null Set.inter_subset_right ht1

Premises used: MeasureTheory.measure_mono_null, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null Set.inter_subset_left hνs

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_mono_null Set.inter_subset_left hνs

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono_null
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null Set.inter_subset_right ht2

Premises used: MeasureTheory.measure_mono_null, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
hμν : μ ≪ ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((μ.withDensity (ν.rnDeriv μ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α
left : MeasurableSet t
ht1 : Eq (α := ℝ≥0∞) ((ν.singularPart μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
ht2 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ tᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact measure_mono_null Set.inter_subset_right ht2

Premises used: MeasureTheory.measure_mono_null, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
rw : ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
| μ

Tactic:
rw [μ.haveLebesgueDecomposition_add ν, add_comm]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
⊢ ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν

Tactic:
conv_rhs at hξμ => rw [μ.haveLebesgueDecomposition_add ν, add_comm]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ μ
hξν : ξ ≪ ν
hξμ₁ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
⊢ ξ ≪ ν

Tactic:
conv_rhs at hξμ => rw [μ.haveLebesgueDecomposition_add ν, add_comm]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
hξν : ξ ≪ ν
⊢ ξ ≪ ν.withDensity (μ.rnDeriv ν)

Tactic:
absolutelyContinuous_of_add_of_mutuallySingular hξμ ?_

Premises used: MeasureTheory.Measure.absolutelyContinuous_of_add_of_mutuallySingular
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
hξν : ξ ≪ ν
refine : ξ ⟂ₘ μ.singularPart ν
⊢ ξ ≪ ν.withDensity (μ.rnDeriv ν)

Tactic:
refine absolutelyContinuous_of_add_of_mutuallySingular hξμ ?_

Premises used: MeasureTheory.Measure.absolutelyContinuous_of_add_of_mutuallySingular
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
hξν : ξ ≪ ν
⊢ ξ ⟂ₘ μ.singularPart ν

Tactic:
MutuallySingular.mono_ac (mutuallySingular_singularPart μ ν).symm hξν .rfl

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.mono_ac, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ξ : Measure α
inst : μ.HaveLebesgueDecomposition ν
hξμ : ξ ≪ ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν
hξν : ξ ≪ ν
⊢ ξ ⟂ₘ μ.singularPart ν

Tactic:
exact MutuallySingular.mono_ac (mutuallySingular_singularPart μ ν).symm hξν .rfl

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.mono_ac, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : ν.HaveLebesgueDecomposition μ
⊢ ν.withDensity (μ.rnDeriv ν) ≪ μ.withDensity (ν.rnDeriv μ)

Tactic:
(withDensity_absolutelyContinuous ν (μ.rnDeriv ν)).withDensity_rnDeriv
    (absolutelyContinuous_of_le (withDensity_rnDeriv_le _ _))

Premises used: MeasureTheory.Measure.rnDeriv, MeasureTheory.Measure.withDensity_rnDeriv_le, MeasureTheory.Measure.AbsolutelyContinuous.withDensity_rnDeriv, MeasureTheory.Measure.absolutelyContinuous_of_le, MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
rw : μ.singularPart ν ⟂ₘ μ.singularPart ν
⊢ μ.singularPart ν = 0

Tactic:
rw [← MutuallySingular.self_iff]

Premises used: MeasureTheory.Measure.MutuallySingular.self_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
⊢ μ.singularPart ν ⟂ₘ μ.singularPart ν

Tactic:
MutuallySingular.mono_ac (mutuallySingular_singularPart _ _)
    AbsolutelyContinuous.rfl ((absolutelyContinuous_of_le (singularPart_le _ _)).trans h)

Premises used: MeasureTheory.Measure.singularPart_le, MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.absolutelyContinuous_of_le, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν
⊢ μ.singularPart ν ⟂ₘ μ.singularPart ν

Tactic:
exact MutuallySingular.mono_ac (mutuallySingular_singularPart _ _)
    AbsolutelyContinuous.rfl ((absolutelyContinuous_of_le (singularPart_le _ _)).trans h)

Premises used: MeasureTheory.Measure.singularPart_le, MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.absolutelyContinuous_of_le, MeasureTheory.Measure.AbsolutelyContinuous.rfl, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.mono_ac
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
ν : Measure α
⊢ singularPart 0 ν = 0

Tactic:
singularPart_eq_zero_of_ac (AbsolutelyContinuous.zero _)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.zero, MeasureTheory.Measure.singularPart_eq_zero_of_ac
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
rw : μ.singularPart 0 + withDensity 0 (μ.rnDeriv 0)
| μ

Tactic:
rw [haveLebesgueDecomposition_add μ 0]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
conv_rhs : μ.singularPart 0 = μ.singularPart 0 + withDensity 0 (μ.rnDeriv 0)
⊢ μ.singularPart 0 = μ

Tactic:
conv_rhs => rw [haveLebesgueDecomposition_add μ 0]

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
⊢ μ.singularPart 0 = μ.singularPart 0 + withDensity 0 (μ.rnDeriv 0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
have h_dec := haveLebesgueDecomposition_add μ ν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν = 0 ↔ μ ≪ ν

Tactic:
⟨fun h ↦ ?_, singularPart_eq_zero_of_ac⟩

Premises used: Iff.intro, MeasureTheory.Measure.singularPart_eq_zero_of_ac
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
refine : ∀ (h : μ.singularPart ν = 0), μ ≪ ν
⊢ μ.singularPart ν = 0 ↔ μ ≪ ν

Tactic:
refine ⟨fun h ↦ ?_, singularPart_eq_zero_of_ac⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ μ = ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [h, zero_add] at h_dec

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
h_dec₁ : μ = ν.withDensity (μ.rnDeriv ν)
⊢ μ.singularPart ν = 0

Tactic:
rw [h, zero_add] at h_dec

Premises used: zero_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
rw : ν.withDensity (μ.rnDeriv ν) ≪ ν
⊢ μ ≪ ν

Tactic:
rw [h_dec]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
withDensity_absolutelyContinuous ν _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
h_dec : μ = ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν = 0
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
exact withDensity_absolutelyContinuous ν _

Premises used: MeasureTheory.withDensity_absolutelyContinuous