-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma singularPart_eq_zero_iff_measure_eq_zero (κ η : Kernel α γ)
    [IsFiniteKernel κ] [IsFiniteKernel η] (a : α) :
    singularPart κ η a = 0 ↔ κ a (mutuallySingularSetSlice κ η a) = 0

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

Tactic:
simp_rw [Kernel.ext_iff, Measure.ext_iff] at h_eq_add

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add : ∀ (a : α) (s : Set γ), MeasurableSet s → ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) s = (κ a) s
⊢ (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0

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

Tactic:
exact singularPart_eq_zero_iff_apply_eq_zero κ η a

Result:
no goals

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

Tactic:
have h_eq_add := rnDeriv_add_singularPart κ η

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

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

Tactic:
simp only [coe_add, Pi.add_apply, Measure.coe_add,
  withDensity_rnDeriv_mutuallySingularSetSlice κ η, zero_add] at h_eq_add

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add : ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = (κ a) (κ.mutuallySingularSetSlice η a)
⊢ (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0

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

Tactic:
rw [← h_eq_add]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add : ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = (κ a) (κ.mutuallySingularSetSlice η a)
⊢ (κ.singularPart η) a = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add : ∀ (a : α) (s : Set γ), MeasurableSet s → ((η.withDensity (κ.rnDeriv η) + κ.singularPart η) a) s = (κ a) s
⊢ (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
specialize h_eq_add a (mutuallySingularSetSlice κ η a)
  (measurableSet_mutuallySingularSetSlice κ η a)

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