-- Module: Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
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)
calc :
  f (μ.rnDeriv ν a).toReal =
    f (μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal
calc₁ :
  f (μ.rnDeriv ν a * ∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal =
    f (∫⁻ (b : 𝓨), μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal
calc₂ :
  f (∫⁻ (b : 𝓨), μ.rnDeriv ν a * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal =
    f (∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal
calc₃ :
  f (∫⁻ (b : 𝓨), (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂(η : (a : 𝓧) → Measure 𝓨) a).toReal =
    f (@integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal)
calc₄ :
  f (@integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal) ≤
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal
⊢ f (μ.rnDeriv ν a).toReal ≤
    @integral _ _ _ _ m𝓨 ((η : (a : 𝓧) → Measure 𝓨) a) fun (b : 𝓨) ↦ f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal

Tactic:
calc f (μ.rnDeriv ν a).toReal
    = f (μ.rnDeriv ν a * ∫⁻ b, (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η a)).toReal := by simp [h_eq_one]
  _ = f (∫⁻ b, (μ.rnDeriv ν a) * (μ ⊗ₘ κ).rnDeriv (μ ⊗ₘ η) (a, b) ∂(η a)).toReal := by
    rw [lintegral_const_mul _ (by fun_prop)]
  _ = f (∫⁻ b, (μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b) ∂(η a)).toReal := by
    congr 2
    refine lintegral_congr_ae ?_
    filter_upwards [h_mul_eq] with b hb using hb
  _ = f (∫ b, ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal ∂(η a)) := by
    rw [integral_toReal (by fun_prop) h_lt_top]
  _ ≤ ∫ b, f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b)).toReal ∂(η a) := by
    rw [← average_eq_integral, ← average_eq_integral]
    exact ConvexOn.map_average_le hf_cvx hf_cont isClosed_Ici (by simp) h_int' h_int

Premises used: HMul.hMul, MeasureTheory.Measure.rnDeriv, Prod.mk, ENNReal.toReal, MeasureTheory.integral, MeasureTheory.Measure.compProd, DFunLike.coe, MeasureTheory.lintegral