awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
⊢ μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν

Tactic:
have h₂ : μ.rnDeriv ν =ᵐ[ν] μ'.rnDeriv ν :=
    (Measure.rnDeriv_withDensity _ (Measure.measurable_rnDeriv _ _)).symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x

Tactic:
have hμ' := rnDeriv_withDensity_right_of_absolutelyContinuous
    (withDensity_absolutelyContinuous ν (μ.rnDeriv ν)) hf hf_ne_zero hf_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
h :
  ∀ (x : α) (hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x)
    (hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x)
    (hx_eq :
      (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x),
    μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
⊢ μ.rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦ (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
filter_upwards [h₁, h₂, hμ'] with x hx₁ hx₂ hx_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : AEMeasurable f ν
hf_ne_zero : ∀ᵐ (x : α) ∂ν, f x ≠ 0
hf_ne_top : ∀ᵐ (x : α) ∂ν, f x ≠ ∞
μ' : Measure α := ν.withDensity (μ.rnDeriv ν)
h₁ : μ'.rnDeriv (ν.withDensity f) =ᶠ[ae ν] μ.rnDeriv (ν.withDensity f)
h₂ : μ.rnDeriv ν =ᶠ[ae ν] μ'.rnDeriv ν
hμ' :
  (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) =ᶠ[ae ν] fun (x : α) ↦
    (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
x : α
hx₁ : μ'.rnDeriv (ν.withDensity f) x = μ.rnDeriv (ν.withDensity f) x
hx₂ : μ.rnDeriv ν x = μ'.rnDeriv ν x
hx_eq : (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν.withDensity f) x = (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x
h : μ'.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x
h₃ : μ'.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ'.rnDeriv ν x
h₄ h₅ : (f x)⁻¹ * (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν x = (f x)⁻¹ * μ'.rnDeriv ν x
⊢ μ.rnDeriv (ν.withDensity f) x = (f x)⁻¹ * μ.rnDeriv ν x

Tactic:
rw [← hx₁, hx₂, hx_eq]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
⊢ MeasurableSet t

Tactic:
have ht : MeasurableSet t := h.measurableSet_nullSet
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ ∀ᵐ (x : α) ∂ν.restrict tᶜ, μ.rnDeriv ν' x = 0 x

Tactic:
simp [t]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
refine : ∀ᵐ (x : α) ∂ν.restrict t, μ.rnDeriv ν' x = 0 x
⊢ μ.rnDeriv ν' =ᶠ[ae ν] 0

Tactic:
refine ae_of_ae_restrict_of_ae_restrict_compl t ?_ (by simp [t])

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')

Tactic:
have h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν') :=
      hνν'.ae_le (rnDeriv_restrict μ ν' ht)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h_1 : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h_1.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
rw : ∀ᵐ (x : α) ∂ν, x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' ht]

Premises used: Filter.EventuallyEq, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h_1 : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h_1.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
h₁ :
  ∀ (x : α) (hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x) (hxt : x ∈ t),
    μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x
⊢ ∀ᵐ (x : α) ∂ν, x ∈ t → μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x

Tactic:
filter_upwards [h] with x hx hxt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h_1 : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h_1.nullSet
ht : MeasurableSet t
h : (μ.restrict t).rnDeriv ν' =ᶠ[ae ν] t.indicator (μ.rnDeriv ν')
x : α
hx : (μ.restrict t).rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
hxt : x ∈ t
h₁ : μ.rnDeriv ν' x = t.indicator (μ.rnDeriv ν') x
h₂ h₃ : μ.rnDeriv ν' x = μ.rnDeriv ν' x
⊢ μ.rnDeriv ν' x = (μ.restrict t).rnDeriv ν' x

Tactic:
rw [hx, Set.indicator_of_mem hxt]

Premises used: Set.indicator_of_mem
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'

Tactic:
have : μ.rnDeriv ν' =ᵐ[ν.restrict t] (μ.restrict t).rnDeriv ν' := by
    have h : (μ.restrict t).rnDeriv ν' =ᵐ[ν] t.indicator (μ.rnDeriv ν') :=
      hνν'.ae_le (rnDeriv_restrict μ ν' ht)
    rw [Filter.EventuallyEq, ae_restrict_iff' ht]
    filter_upwards [h] with x hx hxt
    rw [hx, Set.indicator_of_mem hxt]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0

Tactic:
this.trans ?_

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
refine : (μ.restrict t).rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0
⊢ μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0

Tactic:
refine this.trans ?_

Premises used: Filter.EventuallyEq.trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
simp : rnDeriv 0 ν' =ᶠ[ae (ν.restrict h.nullSet)] 0
⊢ (μ.restrict t).rnDeriv ν' =ᶠ[ae (ν.restrict t)] 0

Tactic:
simp only [t, MutuallySingular.restrict_nullSet]

Premises used: MeasureTheory.Measure.MutuallySingular.restrict_nullSet
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this_1 : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
this : rnDeriv 0 ν' =ᶠ[ae ν'] 0
⊢ ν.restrict t ≪ ν'

Tactic:
have h_ac' : ν.restrict t ≪ ν' := restrict_le_self.absolutelyContinuous.trans hνν'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this_1 : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
this : rnDeriv 0 ν' =ᶠ[ae ν'] 0
h_ac' : ν.restrict t ≪ ν'
⊢ rnDeriv 0 ν' =ᶠ[ae (ν.restrict h.nullSet)] 0

Tactic:
h_ac'.ae_le this

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this_1 : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
this : rnDeriv 0 ν' =ᶠ[ae ν'] 0
h_ac' : ν.restrict t ≪ ν'
⊢ rnDeriv 0 ν' =ᶠ[ae (ν.restrict h.nullSet)] 0

Tactic:
exact h_ac'.ae_le this

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
suffices : rnDeriv 0 ν' =ᶠ[ae ν'] 0
⊢ rnDeriv 0 ν' =ᶠ[ae (ν.restrict h.nullSet)] 0

Tactic:
suffices (0 : Measure α).rnDeriv ν' =ᵐ[ν'] 0 by
    have h_ac' : ν.restrict t ≪ ν' := restrict_le_self.absolutelyContinuous.trans hνν'
    exact h_ac'.ae_le this
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
⊢ rnDeriv 0 ν' =ᶠ[ae ν'] 0

Tactic:
rnDeriv_zero _

Premises used: MeasureTheory.Measure.rnDeriv_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν'
inst_1 : SigmaFinite ν'
h : μ ⟂ₘ ν
hνν' : ν ≪ ν'
t : Set α := h.nullSet
ht : MeasurableSet t
this : μ.rnDeriv ν' =ᶠ[ae (ν.restrict t)] (μ.restrict t).rnDeriv ν'
⊢ rnDeriv 0 ν' =ᶠ[ae ν'] 0

Tactic:
exact rnDeriv_zero _

Premises used: MeasureTheory.Measure.rnDeriv_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0

Tactic:
rnDeriv_eq_zero_of_mutuallySingular (mutuallySingular_singularPart ν μ).symm ?_

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
refine : ν.singularPart μ ≪ ν
⊢ ∀ᵐ (x : α) ∂ν.singularPart μ, μ.rnDeriv ν x = 0

Tactic:
refine rnDeriv_eq_zero_of_mutuallySingular (mutuallySingular_singularPart ν μ).symm ?_

Premises used: MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular, MeasureTheory.Measure.mutuallySingular_singularPart, MeasureTheory.Measure.MutuallySingular.symm
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ ν.singularPart μ ≪ ν

Tactic:
(Measure.singularPart_le _ _).absolutelyContinuous

Premises used: MeasureTheory.Measure.singularPart_le, LE.le.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ ν.singularPart μ ≪ ν

Tactic:
exact (Measure.singularPart_le _ _).absolutelyContinuous

Premises used: MeasureTheory.Measure.singularPart_le, LE.le.absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ.HaveLebesgueDecomposition (ν + ν')
inst_2 : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
⊢ MeasurableSet t

Tactic:
have ht : MeasurableSet t := hνν'.measurableSet_nullSet
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ.HaveLebesgueDecomposition (ν + ν')
inst_2 : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
⊢ ∀ᵐ (x : α) ∂ν.restrict t, μ.rnDeriv (ν + ν') x = μ.rnDeriv ν x

Tactic:
simp [t]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ.HaveLebesgueDecomposition (ν + ν')
inst_2 : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
refine : ∀ᵐ (x : α) ∂ν.restrict tᶜ, μ.rnDeriv (ν + ν') x = μ.rnDeriv ν x
⊢ μ.rnDeriv (ν + ν') =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
refine ae_of_ae_restrict_of_ae_restrict_compl t (by simp [t]) ?_

Premises used: MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ.HaveLebesgueDecomposition (ν + ν')
inst_2 : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
rw : (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = (ν.restrict tᶜ).withDensity (μ.rnDeriv ν)
⊢ μ.rnDeriv (ν + ν') =ᶠ[ae (ν.restrict tᶜ)] μ.rnDeriv ν

Tactic:
rw [← withDensity_eq_iff_of_sigmaFinite (μ := ν.restrict tᶜ)
    (Measure.measurable_rnDeriv _ _).aemeasurable (Measure.measurable_rnDeriv _ _).aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.withDensity_eq_iff_of_sigmaFinite, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ.HaveLebesgueDecomposition (ν + ν')
inst_2 : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
⊢ (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = ((ν + ν').restrict tᶜ).withDensity (μ.rnDeriv (ν + ν'))

Tactic:
simp [t]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ.HaveLebesgueDecomposition (ν + ν')
inst_2 : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
⊢ (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = ((ν + ν').restrict tᶜ).withDensity (μ.rnDeriv (ν + ν'))

Tactic:
have : (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν'))
      = ((ν + ν').restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) := by simp [t]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : μ.HaveLebesgueDecomposition ν
inst_1 : μ.HaveLebesgueDecomposition (ν + ν')
inst_2 : SigmaFinite ν
hμν : μ ≪ ν
hνν' : ν ⟂ₘ ν'
t : Set α := hνν'.nullSet
ht : MeasurableSet t
this : (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = ((ν + ν').restrict tᶜ).withDensity (μ.rnDeriv (ν + ν'))
rw : ((ν + ν').restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = (ν.restrict tᶜ).withDensity (μ.rnDeriv ν)
rw₁ : ((ν + ν').withDensity (μ.rnDeriv (ν + ν'))).restrict tᶜ = (ν.restrict tᶜ).withDensity (μ.rnDeriv ν)
rw₂ : ((ν + ν').withDensity (μ.rnDeriv (ν + ν'))).restrict tᶜ = (ν.withDensity (μ.rnDeriv ν)).restrict tᶜ
rw₃ : μ.restrict tᶜ = (ν.withDensity (μ.rnDeriv ν)).restrict tᶜ
rw₄ rw₅ : μ.restrict tᶜ = μ.restrict tᶜ
⊢ (ν.restrict tᶜ).withDensity (μ.rnDeriv (ν + ν')) = (ν.restrict tᶜ).withDensity (μ.rnDeriv ν)

Tactic:
rw [this, ← restrict_withDensity ht.compl, ← restrict_withDensity ht.compl,
      Measure.withDensity_rnDeriv_eq _ _ (hμν.add_right ν'), Measure.withDensity_rnDeriv_eq _ _ hμν]

Premises used: MeasureTheory.restrict_withDensity, MeasureTheory.Measure.AbsolutelyContinuous.add_right, MeasurableSet.compl, MeasureTheory.Measure.withDensity_rnDeriv_eq
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν ν' : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
inst_2 : SigmaFinite ν'
hμν' : μ ⟂ₘ ν'
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νν' : ν ⟂ₘ ν'
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νν' : ν ⟂ₘ ν'
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νν' : ν ⟂ₘ ν'
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νν' : ν ⟂ₘ ν'
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νν' : ν ⟂ₘ ν'
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νν' : ν ⟂ₘ ν'
h_ac : ν ≪ ν + ν'
h₁ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')]
    (μ.singularPart ν).rnDeriv (ν + ν') + (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν')
h₂ :
  (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)).rnDeriv ν =ᶠ[ae ν]
    (μ.singularPart ν).rnDeriv ν + (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν
⊢ (ν.withDensity (μ.rnDeriv ν)).rnDeriv (ν + ν') =ᶠ[ae ν] (ν.withDensity (μ.rnDeriv ν)).rnDeriv ν

Tactic:
have h₃ := rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular
    (withDensity_absolutelyContinuous ν (μ.rnDeriv ν)) hνν'
-- 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 ν
refine : (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] 0
⊢ (μ.singularPart ν).rnDeriv (ν + ν') =ᶠ[ae ν] 0

Tactic:
refine h_ac.ae_eq ?_

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.ae_eq