-- Module: Mathlib.Probability.Kernel.RadonNikodym
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
h :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s ∩ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s \ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s \ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
h₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s ∩ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s \ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
        (0 : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
h₂ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s ∩ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s \ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞))
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
h₃ :
  HAdd.hAdd (β := ℝ≥0∞)
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s \ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞))
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
h₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
          (s \ κ.mutuallySingularSetSlice η a) :
        ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
h₅ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
h₆ h₇ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s ∩ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((η.withDensity (κ.rnDeriv η) : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s \ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞) +
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s ∩ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞)
        ((((κ.singularPart η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞)
            (s \ κ.mutuallySingularSetSlice η a) :
          ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s ∩ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)
      ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) (s \ κ.mutuallySingularSetSlice η a) : ℝ≥0∞)

Tactic:
rw [singularPart_of_subset_mutuallySingularSetSlice (hs.inter hm) inter_subset_right,
    singularPart_of_subset_compl_mutuallySingularSetSlice (diff_subset_iff.mpr (by simp)),
    add_zero, withDensity_rnDeriv_of_subset_mutuallySingularSetSlice inter_subset_right,
    zero_add, withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice (hs.diff hm)
      (diff_subset_iff.mpr (by simp)), add_comm]

Premises used: Iff.mpr, MeasurableSet.diff, Set.diff_subset_iff, zero_add, add_comm, ProbabilityTheory.Kernel.withDensity_rnDeriv_of_subset_mutuallySingularSetSlice, ProbabilityTheory.Kernel.withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice, ProbabilityTheory.Kernel.singularPart_of_subset_compl_mutuallySingularSetSlice, add_zero, Set.inter_subset_right, ProbabilityTheory.Kernel.singularPart_of_subset_mutuallySingularSetSlice, MeasurableSet.inter