-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
@[simp]
lemma withDensity_rnDeriv_eq_zero (μ ν : Measure α) [μ.HaveLebesgueDecomposition ν] :
    ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ ⟂ₘ ν

case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ.singularPart ν ⟂ₘ ν

Tactic:
exact mutuallySingular_singularPart μ ν

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)

Tactic:
refine MutuallySingular.mono_ac h.2 AbsolutelyContinuous.rfl ?_

Result:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ ⟂ₘ ν

Tactic:
rw [h, add_zero] at h_dec

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ ⟂ₘ ν

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [h_dec, MutuallySingular.add_left_iff] at h

Result:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν

Tactic:
have h_dec := haveLebesgueDecomposition_add μ ν

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity (μ.rnDeriv ν) = 0 ↔ μ ⟂ₘ ν

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) = 0

Tactic:
rw [← MutuallySingular.self_iff]

Result:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν.withDensity (μ.rnDeriv ν)

Proof state:
case refine_2
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
h : μ.singularPart ν ⟂ₘ ν ∧ ν.withDensity (μ.rnDeriv ν) ⟂ₘ ν
⊢ ν.withDensity (μ.rnDeriv ν) ≪ ν

Tactic:
exact withDensity_absolutelyContinuous _ _

Result:
no goals

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ ⟂ₘ ν

Tactic:
rw [h_dec]

Result:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
h_dec : μ = μ.singularPart ν
h : ν.withDensity (μ.rnDeriv ν) = 0
⊢ μ.singularPart ν ⟂ₘ ν