-- 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 ν
inst_2 : IsFiniteKernel η
a : α
x : γ
h1 : (κ + ν).rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h2 : κ.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h3 : ν.rnDeriv η a x = Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h4 :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
      (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x
h :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    (κ.rnDeriv η a + ν.rnDeriv η a) x
h₁ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    κ.rnDeriv η a x + ν.rnDeriv η a x
h₂ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x + ν.rnDeriv η a x
h₃ :
  Measure.rnDeriv (m := mγ) ((κ + ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h₄ :
  (∂HAdd.hAdd (α := (a : α) → Measure γ) (β := (a : α) → Measure γ) (⇑κ : (a : α) → Measure γ)
          (⇑ν : (a : α) → Measure γ) a/∂(η : (a : α) → Measure γ) a)
      x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h₅ :
  (∂HAdd.hAdd (α := Measure γ) (β := Measure γ) ((κ : (a : α) → Measure γ) a : Measure γ)
          ((ν : (a : α) → Measure γ) a : Measure γ)/∂(η : (a : α) → Measure γ) a)
      x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
h₆ :
  HAdd.hAdd (α := γ → ℝ≥0∞) (β := γ → ℝ≥0∞)
      (Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a))
      (Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a)) x =
    Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
      Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
⊢ (κ + ν).rnDeriv η a x = (κ.rnDeriv η a + ν.rnDeriv η a) x
have h₇ : Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
    Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x =
  Measure.rnDeriv (m := mγ) ((κ : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x +
    Measure.rnDeriv (m := mγ) ((ν : (a : α) → Measure γ) a) ((η : (a : α) → Measure γ) a) x
Tactic: rw [h1, Pi.add_apply, h2, h3, coe_add, Pi.add_apply, h4, Pi.add_apply]