awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r = 0
pos : (HSMul.hSMul (α := ℝ≥0) 0 μ).singularPart ν = HSMul.hSMul (α := ℝ≥0) 0 (μ.singularPart ν)
pos₁ : singularPart 0 ν = HSMul.hSMul (α := ℝ≥0) 0 (μ.singularPart ν)
pos₂ : singularPart 0 ν = 0
pos₃ pos₄ : Eq.{u_1 + 1} (α := Measure α) 0 0
⊢ (r • μ).singularPart ν = r • μ.singularPart ν

Tactic:
rw [hr, zero_smul, zero_smul, singularPart_zero]

Premises used: zero_smul, MeasureTheory.Measure.singularPart_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), (r • μ).singularPart ν = r • μ.singularPart ν
neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), (r • μ).singularPart ν = r • μ.singularPart ν
⊢ (r • μ).singularPart ν = r • μ.singularPart ν

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : μ.HaveLebesgueDecomposition ν
⊢ (r • μ).singularPart ν = r • μ.singularPart ν

Tactic:
(eq_singularPart ((measurable_rnDeriv μ ν).const_smul (r : ℝ≥0∞))
          (MutuallySingular.smul r (mutuallySingular_singularPart _ _)) ?_).symm

Premises used: ENNReal.ofNNReal, MeasureTheory.Measure.MutuallySingular.smul, Measurable.const_smul, MeasureTheory.Measure.mutuallySingular_singularPart, Eq.symm, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : μ.HaveLebesgueDecomposition ν
pos : r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • μ.rnDeriv ν)
⊢ (r • μ).singularPart ν = r • μ.singularPart ν

Tactic:
refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul (r : ℝ≥0∞))
          (MutuallySingular.smul r (mutuallySingular_singularPart _ _)) ?_).symm

Premises used: ENNReal.ofNNReal, MeasureTheory.Measure.MutuallySingular.smul, Measurable.const_smul, MeasureTheory.Measure.mutuallySingular_singularPart, Eq.symm, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : μ.HaveLebesgueDecomposition ν
pos : r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + (↑r : ℝ≥0∞) • ν.withDensity (μ.rnDeriv ν)
pos₁ : r • μ = (↑r : ℝ≥0∞) • (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
pos₂ : r • μ = (↑r : ℝ≥0∞) • μ
pos₃ pos₄ : (↑r : ℝ≥0∞) • μ = (↑r : ℝ≥0∞) • μ
⊢ r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • μ.rnDeriv ν)

Tactic:
rw [withDensity_smul _ (measurable_rnDeriv _ _), ← smul_add,
      ← haveLebesgueDecomposition_add μ ν, ENNReal.smul_def]

Premises used: ENNReal.smul_def, MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasureTheory.withDensity_smul, MeasureTheory.Measure.measurable_rnDeriv, smul_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
neg : ¬(r • μ).HaveLebesgueDecomposition ν
⊢ (r • μ).singularPart ν = r • μ.singularPart ν

Tactic:
rw [singularPart, singularPart, dif_neg hl, dif_neg, smul_zero]

Premises used: smul_zero, dif_neg, MeasureTheory.Measure.singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ¬(r • μ).HaveLebesgueDecomposition ν

Tactic:
fun hl' ↦ hl ?_

Premises used: Not
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
neg : ∀ (hl' : (r • μ).HaveLebesgueDecomposition ν), μ.HaveLebesgueDecomposition ν
⊢ ¬(r • μ).HaveLebesgueDecomposition ν

Tactic:
refine fun hl' ↦ hl ?_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : (r • μ).HaveLebesgueDecomposition ν
neg : (r⁻¹ • r • μ).HaveLebesgueDecomposition ν
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
rw [← inv_smul_smul₀ hr μ]

Premises used: inv_smul_smul₀
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : (r • μ).HaveLebesgueDecomposition ν
⊢ (r⁻¹ • r • μ).HaveLebesgueDecomposition ν

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), μ.singularPart (r • ν) = μ.singularPart ν
neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), μ.singularPart (r • ν) = μ.singularPart ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

Premises used: MeasureTheory.Measure.HaveLebesgueDecomposition
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
(eq_singularPart ((measurable_rnDeriv μ ν).const_smul r⁻¹) ?_ ?_).symm

Premises used: Measurable.const_smul, Inv.inv, Eq.symm, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
pos : μ.singularPart ν ⟂ₘ r • ν
pos₁ : μ = μ.singularPart ν + (r • ν).withDensity (r⁻¹ • μ.rnDeriv ν)
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul r⁻¹) ?_ ?_).symm

Premises used: Measurable.const_smul, Inv.inv, Eq.symm, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ r • ν

Tactic:
(mutuallySingular_singularPart μ ν).mono_ac AbsolutelyContinuous.rfl
        smul_absolutelyContinuous

Premises used: MeasureTheory.Measure.smul_absolutelyContinuous, 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 α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν ⟂ₘ r • ν

Tactic:
exact (mutuallySingular_singularPart μ ν).mono_ac AbsolutelyContinuous.rfl
        smul_absolutelyContinuous

Premises used: MeasureTheory.Measure.smul_absolutelyContinuous, 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 α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
pos : μ = μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν)
pos₁ : Measurable (r⁻¹ • μ.rnDeriv ν)
⊢ μ = μ.singularPart ν + (r • ν).withDensity (r⁻¹ • μ.rnDeriv ν)

Tactic:
rw [ENNReal.smul_def r, withDensity_smul_measure, ← withDensity_smul]

Premises used: ENNReal.smul_def, MeasureTheory.withDensity_smul_measure, MeasureTheory.withDensity_smul
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ Measurable (r⁻¹ • μ.rnDeriv ν)

Tactic:
(measurable_rnDeriv _ _).const_smul _

Premises used: Measurable.const_smul, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ Measurable (r⁻¹ • μ.rnDeriv ν)

Tactic:
exact (measurable_rnDeriv _ _).const_smul _

Premises used: Measurable.const_smul, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
⊢ μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)

Tactic:
haveLebesgueDecomposition_add μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
h : (↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν = μ.rnDeriv ν
⊢ μ = μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν)

Tactic:
convert! haveLebesgueDecomposition_add μ ν

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
h : ∀ (x : α), ((↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν) x = μ.rnDeriv ν x
⊢ (↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν = μ.rnDeriv ν

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : μ.HaveLebesgueDecomposition ν
x : α
h : r • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x
h₁ h₂ : μ.rnDeriv ν x = μ.rnDeriv ν x
⊢ (↑r : ℝ≥0∞) • r⁻¹ • μ.rnDeriv ν x = μ.rnDeriv ν x

Tactic:
rw [← ENNReal.smul_def, smul_inv_smul₀ hr]

Premises used: ENNReal.smul_def, smul_inv_smul₀
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
neg : ¬μ.HaveLebesgueDecomposition (r • ν)
⊢ μ.singularPart (r • ν) = μ.singularPart ν

Tactic:
rw [singularPart, singularPart, dif_neg hl, dif_neg]

Premises used: dif_neg, MeasureTheory.Measure.singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ¬μ.HaveLebesgueDecomposition (r • ν)

Tactic:
fun hl' ↦ hl ?_

Premises used: Not
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
neg : ∀ (hl' : μ.HaveLebesgueDecomposition (r • ν)), μ.HaveLebesgueDecomposition ν
⊢ ¬μ.HaveLebesgueDecomposition (r • ν)

Tactic:
refine fun hl' ↦ hl ?_
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : μ.HaveLebesgueDecomposition (r • ν)
neg : μ.HaveLebesgueDecomposition (r⁻¹ • r • ν)
⊢ μ.HaveLebesgueDecomposition ν

Tactic:
rw [← inv_smul_smul₀ hr ν]

Premises used: inv_smul_smul₀
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r ≠ 0
hl : ¬μ.HaveLebesgueDecomposition ν
hl' : μ.HaveLebesgueDecomposition (r • ν)
⊢ μ.HaveLebesgueDecomposition (r⁻¹ • r • ν)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
⊢ (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν

Tactic:
(eq_singularPart ((measurable_rnDeriv μ₁ ν).add (measurable_rnDeriv μ₂ ν))
    ((mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)) ?_).symm

Premises used: MeasureTheory.Measure.MutuallySingular.add_left, Measurable.add, MeasureTheory.Measure.mutuallySingular_singularPart, Eq.symm, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
refine : μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + ν.withDensity fun (a : α) ↦ μ₁.rnDeriv ν a + μ₂.rnDeriv ν a
⊢ (μ₁ + μ₂).singularPart ν = μ₁.singularPart ν + μ₂.singularPart ν

Tactic:
refine (eq_singularPart ((measurable_rnDeriv μ₁ ν).add (measurable_rnDeriv μ₂ ν))
    ((mutuallySingular_singularPart _ _).add_left (mutuallySingular_singularPart _ _)) ?_).symm

Premises used: MeasureTheory.Measure.MutuallySingular.add_left, Measurable.add, MeasureTheory.Measure.mutuallySingular_singularPart, Eq.symm, MeasureTheory.Measure.measurable_rnDeriv, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
rw : μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + ν.withDensity fun (a : α) ↦ μ₁.rnDeriv ν a + μ₂.rnDeriv ν a

Tactic:
rw [← Pi.add_def, withDensity_add_left (measurable_rnDeriv μ₁ ν)]

Premises used: MeasureTheory.withDensity_add_left, Pi.add_def, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
rw : μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
| μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))

Tactic:
rw [add_assoc, add_comm (μ₂.singularPart ν), ← add_assoc, ← add_assoc]

Premises used: add_assoc, add_comm, MeasureTheory.Measure.singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
conv_rhs : μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
⊢ μ₁ + μ₂ = μ₁.singularPart ν + μ₂.singularPart ν + (ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν))

Tactic:
conv_rhs => rw [add_assoc, add_comm (μ₂.singularPart ν), ← add_assoc, ← add_assoc]

Premises used: add_assoc, add_comm, MeasureTheory.Measure.singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ₁ μ₂ ν : Measure α
inst : μ₁.HaveLebesgueDecomposition ν
inst_1 : μ₂.HaveLebesgueDecomposition ν
rw : μ₁ + μ₂ = μ₁ + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν
rw₁ : μ₁ + μ₂ = μ₁ + (ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν)
rw₂ : μ₁ + μ₂ = μ₁ + (μ₂.singularPart ν + ν.withDensity (μ₂.rnDeriv ν))
rw₃ rw₄ : μ₁ + μ₂ = μ₁ + μ₂
⊢ μ₁ + μ₂ = μ₁.singularPart ν + ν.withDensity (μ₁.rnDeriv ν) + ν.withDensity (μ₂.rnDeriv ν) + μ₂.singularPart ν

Tactic:
rw [← haveLebesgueDecomposition_add μ₁ ν, add_assoc, add_comm (ν.withDensity (μ₂.rnDeriv ν)),
    ← haveLebesgueDecomposition_add μ₂ ν]

Premises used: MeasureTheory.Measure.withDensity, MeasureTheory.Measure.haveLebesgueDecomposition_add, add_assoc, MeasureTheory.Measure.rnDeriv, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s

Tactic:
(Measure.eq_singularPart (f := s.indicator (μ.rnDeriv ν)) ?_ ?_ ?_).symm

Premises used: Eq.symm, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
refine_1 : Measurable (s.indicator (μ.rnDeriv ν))
refine_2 : (μ.singularPart ν).restrict s ⟂ₘ ν
refine_3 : μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))
⊢ (μ.restrict s).singularPart ν = (μ.singularPart ν).restrict s

Tactic:
refine (Measure.eq_singularPart (f := s.indicator (μ.rnDeriv ν)) ?_ ?_ ?_).symm

Premises used: Eq.symm, MeasureTheory.Measure.eq_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ Measurable (s.indicator (μ.rnDeriv ν))

Tactic:
(μ.measurable_rnDeriv ν).indicator hs

Premises used: Measurable.indicator, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ Measurable (s.indicator (μ.rnDeriv ν))

Tactic:
exact (μ.measurable_rnDeriv ν).indicator hs

Premises used: Measurable.indicator, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ (μ.singularPart ν).restrict s ⟂ₘ ν

Tactic:
(Measure.mutuallySingular_singularPart μ ν).restrict s

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.restrict
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
⊢ (μ.singularPart ν).restrict s ⟂ₘ ν

Tactic:
exact (Measure.mutuallySingular_singularPart μ ν).restrict s

Premises used: MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.restrict
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
refine_3 :
  ∀ (t : Set α),
    MeasurableSet t →
      Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        (((μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν)) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ μ.restrict s = (μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν))

Tactic:
ext t
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
s : Set α
hs : MeasurableSet s
t : Set α
h : MeasurableSet t
refine_3 :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + (ν.restrict s).withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_3₁ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_3₂ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine_3₃ refine_3₄ :
  Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    (((μ.singularPart ν).restrict s + ν.withDensity (s.indicator (μ.rnDeriv ν)) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [withDensity_indicator hs, ← restrict_withDensity hs, ← Measure.restrict_add,
      ← μ.haveLebesgueDecomposition_add ν]

Premises used: MeasureTheory.Measure.restrict_add, MeasureTheory.withDensity_indicator, MeasureTheory.Measure.haveLebesgueDecomposition_add, MeasureTheory.restrict_withDensity
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
| μ.restrict s

Tactic:
rw [← singularPart_add_rnDeriv μ ν]

Premises used: MeasureTheory.Measure.singularPart_add_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
conv_rhs : μ.singularPart ν = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s
⊢ μ.singularPart ν = μ.restrict s

Tactic:
conv_rhs => rw [← singularPart_add_rnDeriv μ ν]

Premises used: MeasureTheory.Measure.singularPart_add_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rwa : μ.singularPart ν = (μ.singularPart ν).restrict s + (ν.withDensity (μ.rnDeriv ν)).restrict s
rwa₁ : μ.singularPart ν = μ.singularPart ν + (ν.withDensity (μ.rnDeriv ν)).restrict s
hs : ∀ᵐ (x : α) ∂μ.singularPart ν, x ∈ s
rwa₂ : μ.singularPart ν = μ.singularPart ν + 0
hs₁ : ∀ᵐ (x : α) ∂μ.singularPart ν, x ∈ s
rwa₃ : μ.singularPart ν = μ.singularPart ν
hs₂ : ∀ᵐ (x : α) ∂μ.singularPart ν, x ∈ s
rwa₄ : μ.singularPart ν = μ.singularPart ν
hs₃ hs₄ hs₅ : ∀ᵐ (x : α) ∂μ.singularPart ν, x ∈ s
⊢ μ.singularPart ν = (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).restrict s

Tactic:
rwa [restrict_add, restrict_eq_self_of_ae_mem, restrict_eq_zero.2 hνs, add_zero]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_add, MeasureTheory.Measure.restrict_eq_zero, MeasureTheory.Measure.restrict_eq_self_of_ae_mem, add_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : μ.HaveLebesgueDecomposition ν
hμs : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.singularPart ν = μ.restrict s

Tactic:
singularPart_eq_restrict' hμs <| withDensity_absolutelyContinuous _ _ hνs

Premises used: MeasureTheory.Measure.singularPart_eq_restrict', MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : IsFiniteMeasure μ
nth_rw : ν.withDensity (μ.rnDeriv ν) + μ.singularPart ν - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)
⊢ μ - μ.singularPart ν = ν.withDensity (μ.rnDeriv ν)

Tactic:
nth_rw 1 [← rnDeriv_add_singularPart μ ν]

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

Tactic:
Measure.add_sub_cancel

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

Tactic:
exact Measure.add_sub_cancel

Premises used: MeasureTheory.Measure.add_sub_cancel