-- Lean 4 proof step from Mathlib.Probability.Kernel.RadonNikodym (goal)
Goal:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) +
      (κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞)) =
    κ + η
a : α
s : Set γ
h_1 : MeasurableSet s
h :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                  (a : α) → Measure γ)
                a :
              Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) : (a : α) → Measure γ)
                a :
              Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          s :
        ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
h₁ :
  ∀
    (h :
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
          (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                      (a : α) → Measure γ)
                    a :
                  Measure γ) :
                (a : Set γ) → ℝ≥0∞)
              s :
            ℝ≥0∞)
          ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞) =
        HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
          ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                  (a : α) → Measure γ)
                a :
              Measure γ) :
            (a : Set γ) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
have h₂ : ∀
  (h :
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                    (a : α) → Measure γ)
                  a :
                Measure γ) :
              (a : Set γ) → ℝ≥0∞)
            s :
          ℝ≥0∞) =
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((((κ : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
        ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    (((((κ + η).withDensity fun (a : α) (x : γ) ↦ (↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal : ℝ≥0∞) :
                (a : α) → Measure γ)
              a :
            Measure γ) :
          (a : Set γ) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((η : (a : α) → Measure γ) a : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at h
Cleared hypotheses: h