-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma withDensity_rnDeriv_eq_zero_iff_mutuallySingular (κ η : Kernel α γ)
    [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
    withDensity η (rnDeriv κ η) a = 0 ↔ κ a ⟂ₘ η a

Proof state:
case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a ⟂ₘ η a ∧ (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0

Tactic:
rw [← Measure.MutuallySingular.self_iff]

Result:
case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a ⟂ₘ η a ∧ (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a ⟂ₘ (η.withDensity (κ.rnDeriv η)) a

Proof state:
case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a ⟂ₘ η a ∧ (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a ⟂ₘ (η.withDensity (κ.rnDeriv η)) a

Tactic:
exact h.1.mono_ac Measure.AbsolutelyContinuous.rfl
  (withDensity_absolutelyContinuous (κ := η) (rnDeriv κ η) a)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0

Tactic:
rw [Measure.MutuallySingular.add_left_iff] at h

Result:
case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a ⟂ₘ η a ∧ (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a

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

Result:
case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a = 0
⊢ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a

case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0

Proof state:
case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a = 0
⊢ (κ.singularPart η) a ⟂ₘ η a

Tactic:
exact mutuallySingular_singularPart _ _ _

Result:
no goals

Proof state:
case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a = 0
⊢ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a

Tactic:
rw [h, zero_add]

Result:
case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a = 0
⊢ (κ.singularPart η) a ⟂ₘ η a

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ κ a ⟂ₘ η a

Tactic:
conv_rhs => rw [← rnDeriv_add_singularPart κ η, coe_add, Pi.add_apply]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a