-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
theorem withDensity_rnDeriv_eq (μ ν : Measure α) [HaveLebesgueDecomposition μ ν] (h : μ ≪ ν) :
    ν.withDensity (rnDeriv μ ν) = μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν) Set.univ = 0

Tactic:
rw [← measure_add_measure_compl h_sing.measurableSet_nullSet]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν) h_sing.nullSet + (μ.singularPart ν) h_sing.nullSetᶜ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν) h_sing.nullSetᶜ = 0

Tactic:
refine le_antisymm ?_ (zero_le _)

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν) h_sing.nullSetᶜ ≤ 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν) h_sing.nullSetᶜ ≤ 0

Tactic:
refine (singularPart_le μ ν ?_ ).trans_eq ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ μ h_sing.nullSetᶜ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν) h_sing.nullSet + (μ.singularPart ν) h_sing.nullSetᶜ = 0

Tactic:
simp only [MutuallySingular.measure_nullSet, zero_add]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν) h_sing.nullSetᶜ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
⊢ μ.singularPart ν = 0

Tactic:
suffices μ.singularPart ν Set.univ = 0 by simpa using this

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
⊢ (μ.singularPart ν) Set.univ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
this : μ.singularPart ν = 0
⊢ ν.withDensity (μ.rnDeriv ν) = μ

Tactic:
conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
this : (μ.singularPart ν) Set.univ = 0
⊢ μ.singularPart ν = 0

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ μ h_sing.nullSetᶜ = 0

Tactic:
exact h h_sing.measure_compl_nullSet

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
⊢ (μ.singularPart ν) Set.univ = 0

Tactic:
have h_sing := mutuallySingular_singularPart μ ν

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
h_sing : μ.singularPart ν ⟂ₘ ν
⊢ (μ.singularPart ν) Set.univ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
⊢ ν.withDensity (μ.rnDeriv ν) = μ

Tactic:
suffices μ.singularPart ν = 0 by
  conv_rhs => rw [haveLebesgueDecomposition_add μ ν, this, zero_add]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h : μ ≪ ν
⊢ μ.singularPart ν = 0