-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv (goal)
Goal:
𝓧 : Type u_1
m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
𝓨 : Type u_2
m𝓨 : MeasurableSpace 𝓨
κ η : Kernel 𝓧 𝓨
f : ℝ → ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
hf : StronglyMeasurable f
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont_at : ContinuousWithinAt f (Ici 0) 0
h_int_1 :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal)
        ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
hκη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
hf_cont : ContinuousOn f (Ici 0)
h_lt_top_1 : ∀ᵐ (a : 𝓧) ∂ν, ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_integrable :
  (∀ᵐ (x : 𝓧) ∂ν,
      @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) x)) ∧
    Integrable (ε := ℝ)
      (fun (x : 𝓧) ↦
        @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) x) fun (y : 𝓨) ↦ ‖((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (x, y)).toReal‖)
      ν
h_ae1 :
  ∀ᵐ (a : 𝓧) ∂ν,
    μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_ae2 :
  ∀ᵐ (a : 𝓧) ∂ν,
    ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
      μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
a : 𝓧
h_eq_one : μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a = μ.rnDeriv ν a
h_mul_eq :
  ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨),
    μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
h_lt_top : ∀ᵐ (b : 𝓨) ∂((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) < ∞
h_int' : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
h_int : @Integrable ℝ _ _ _ m𝓨 (fun (y : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, y)).toReal) ((η : (a : 𝓧) → Measure 𝓨) a)
h :
  ∀ (a_1 : 𝓨),
    Membership.mem (γ := Set 𝓨)
      {x : 𝓨 |
        Membership.mem (γ := Set 𝓨)
            {x : 𝓨 |
              (fun (b : 𝓨) ↦ μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)) x}
            x →
          Membership.mem (γ := Set 𝓨)
            {x : 𝓨 |
              (fun (x : 𝓨) ↦
                  Eq (α := ℝ≥0∞) ((fun (b : 𝓨) ↦ μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b)) x)
                    ((fun (b : 𝓨) ↦ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)) x))
                x}
            x}
      a_1
⊢ (ae (F := Measure 𝓨) ((η : (a : 𝓧) → Measure 𝓨) a : Measure 𝓨)).EventuallyEq (β := ℝ≥0∞)
    (fun (b : 𝓨) ↦ μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b)) fun (b : 𝓨) ↦ (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)
have h₁ : ∀ (a_1 : 𝓨),
  μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, a_1) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, a_1) →
    μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, a_1) = (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, a_1)
Tactic: filter_upwards [h_mul_eq] with b hb using hb