awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
simp : μ.singularPart ν ⟂ₘ ν ∧ μ.singularPart ν ⟂ₘ ν'
⊢ (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] 0

Tactic:
simp only [rnDeriv_eq_zero, MutuallySingular.add_right_iff]

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero, MeasureTheory.Measure.MutuallySingular.add_right_iff
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ μ.singularPart ν ⟂ₘ ν ∧ μ.singularPart ν ⟂ₘ ν'

Tactic:
⟨mutuallySingular_singularPart μ ν, hμν'.singularPart ν⟩

Premises used: MeasureTheory.Measure.MutuallySingular.singularPart, And.intro, MeasureTheory.Measure.mutuallySingular_singularPart
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ μ.singularPart ν ⟂ₘ ν ∧ μ.singularPart ν ⟂ₘ ν'

Tactic:
exact ⟨mutuallySingular_singularPart μ ν, hμν'.singularPart ν⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae ν] 0

Tactic:
have h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᵐ[ν] 0 := by
    refine h_ac.ae_eq ?_
    simp only [rnDeriv_eq_zero, MutuallySingular.add_right_iff]
    exact ⟨mutuallySingular_singularPart μ ν, hμν'.singularPart ν⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae ν] 0
⊢ (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0

Tactic:
have h₅ : (μ.singularPart ν).rnDeriv ν =ᵐ[ν] 0 := rnDeriv_singularPart μ ν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0
h :
  ∀ (x : α) (hx₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x = (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x)
    (hx₄ : (μ.singularPart ν).rnDeriv (ν + ν') x = 0 x) (hx₅ : (μ.singularPart ν).rnDeriv ν x = 0 x),
    ((μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')) x =
      ((μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν) x
⊢ (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
h₄ : (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (μ.singularPart ν).rnDeriv ν =ᶠ[ae ν] 0
x : α
hx₃ : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x = (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
hx₄ : (μ.singularPart ν).rnDeriv (ν + ν') x = 0 x
hx₅ : (μ.singularPart ν).rnDeriv ν x = 0 x
h :
  (μ.singularPart ν).rnDeriv (ν + ν') x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x =
    (μ.singularPart ν).rnDeriv ν x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
h₆ :
  0 x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x =
    (μ.singularPart ν).rnDeriv ν x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
h₇ h₈ : 0 x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x = 0 x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
⊢ (μ.singularPart ν).rnDeriv (ν + ν') x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') x =
    (μ.singularPart ν).rnDeriv ν x + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x

Tactic:
rw [hx₃, hx₄, hx₅]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
⊢ ν ≪ ν + ν'

Tactic:
have h_ac : ν ≪ ν + ν' := Measure.AbsolutelyContinuous.rfl.add_right _
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
rw :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ μ.rnDeriv (ν + ν') =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
rw [haveLebesgueDecomposition_add μ ν']

Premises used: MeasureTheory.Measure.haveLebesgueDecomposition_add
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')

Tactic:
have h₁ := rnDeriv_add' (μ.singularPart ν') (ν'.withDensity (μ.rnDeriv ν')) (ν + ν')
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

Tactic:
have h₂ := rnDeriv_add' (μ.singularPart ν') (ν'.withDensity (μ.rnDeriv ν')) ν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

Tactic:
(Filter.EventuallyEq.trans (h_ac.ae_le h₁) ?_).trans h₂.symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.AbsolutelyContinuous.ae_le, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
refine :
  (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
⊢ (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

Tactic:
refine (Filter.EventuallyEq.trans (h_ac.ae_le h₁) ?_).trans h₂.symm

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.AbsolutelyContinuous.ae_le, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
refine_2 :
  ∀ (h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν),
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
      (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
refine_1 : μ.singularPart ν' ⟂ₘ ν'
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

Tactic:
have h₃ := rnDeriv_add_right_of_mutuallySingular' (?_ : μ.singularPart ν' ⟂ₘ ν') hνν'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
⊢ (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0

Tactic:
rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
refine : ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν
⊢ (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0

Tactic:
refine rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
⊢ ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν

Tactic:
hνν'.symm.withDensity

Premises used: MeasureTheory.Measure.MutuallySingular.withDensity, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
⊢ ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν

Tactic:
exact hνν'.symm.withDensity

Premises used: MeasureTheory.Measure.MutuallySingular.withDensity, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
⊢ (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0

Tactic:
have h₄ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv (ν + ν') =ᵐ[ν] 0 := by
      refine rnDeriv_eq_zero_of_mutuallySingular ?_ h_ac
      exact hνν'.symm.withDensity
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
rw : ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν
⊢ (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0

Tactic:
rw [rnDeriv_eq_zero]

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
⊢ ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν

Tactic:
hνν'.symm.withDensity

Premises used: MeasureTheory.Measure.MutuallySingular.withDensity, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
⊢ ν'.withDensity (μ.rnDeriv ν') ⟂ₘ ν

Tactic:
exact hνν'.symm.withDensity

Premises used: MeasureTheory.Measure.MutuallySingular.withDensity, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
⊢ (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0

Tactic:
have h₅ : (ν'.withDensity (rnDeriv μ ν')).rnDeriv ν =ᵐ[ν] 0 := by
      rw [rnDeriv_eq_zero]
      exact hνν'.symm.withDensity
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
h :
  ∀ (x : α) (hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x)
    (hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x)
    (hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x),
    ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
      ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
⊢ (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν

Tactic:
filter_upwards [h₃, h₄, h₅] with x hx₃ hx₄ hx₅
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hνν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν
h₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] 0
h₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] 0
x : α
hx₃ : (μ.singularPart ν').rnDeriv (ν + ν') x = (μ.singularPart ν').rnDeriv ν x
hx₄ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x = 0 x
hx₅ : (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x = 0 x
h :
  (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x
h₆ :
  (μ.singularPart ν').rnDeriv (ν + ν') x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
h₇ :
  (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') x =
    (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
h₈ :
  (μ.singularPart ν').rnDeriv ν x + 0 x = (μ.singularPart ν').rnDeriv ν x + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν x
h₉ h₁₀ : (μ.singularPart ν').rnDeriv ν x + 0 x = (μ.singularPart ν').rnDeriv ν x + 0 x
⊢ ((μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')) x =
    ((μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν) x

Tactic:
rw [Pi.add_apply, Pi.add_apply, hx₃, hx₄, hx₅]

Premises used: Pi.add_apply