lemma integrable_exp_add_compProd {η : Kernel (Ω' × Ω) Ω''} [IsZeroOrMarkovKernel η]
    (hX : HasSubexponentialMGF X V b κ ν) (hY : HasSubexponentialMGF Y VY b η (ν ⊗ₘ κ))
    {t : ℝ} (ht : b * |t| ≤ 1) :
    Integrable (fun ω ↦ exp (t * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ∘ₘ ν)

by
  by_cases hκ : IsSFiniteKernel κ
  swap; · simp [FunLike.coe_zero, hκ]
  rcases eq_zero_or_isMarkovKernel η with rfl | hη
  · simp [FunLike.coe_zero]
  set μ := (κ ⊗ₖ η) ∘ₘ ν with hμ
  have hfst : κ ∘ₘ ν = μ.map Prod.fst := by
    rw [hμ, Measure.map_comp _ _ measurable_fst, ← Kernel.fst_eq, Kernel.fst_compProd]
  have hsnd : η ∘ₘ (ν ⊗ₘ κ) = μ.map Prod.snd := by
    rw [hμ, Measure.comp_compProd_comm, Measure.snd]
  -- measurable representatives of `X` and `Y`
  have hXm := hX.aestronglyMeasurable
  have hYm := hY.aestronglyMeasurable
  set X' := hXm.mk X with hX'
  set Y' := hYm.mk Y with hY'
  have hX'm : Measurable X' := hXm.stronglyMeasurable_mk.measurable
  have hY'm : Measurable Y' := hYm.stronglyMeasurable_mk.measurable
  have hX'' : HasSubexponentialMGF X' V b κ ν := hX.congr hXm.ae_eq_mk
  have hY'' : HasSubexponentialMGF Y' VY b η (ν ⊗ₘ κ) := hY.congr hYm.ae_eq_mk
  have hXeq : (fun ω : Ω × Ω'' ↦ X ω.1) =ᵐ[μ] fun ω ↦ X' ω.1 := by
    have h : ∀ᵐ y ∂(μ.map Prod.fst), X y = X' y := by
      rw [← hfst]
      exact hXm.ae_eq_mk
    exact ae_of_ae_map measurable_fst.aemeasurable h
  have hYeq : (fun ω : Ω × Ω'' ↦ Y ω.2) =ᵐ[μ] fun ω ↦ Y' ω.2 := by
    have h : ∀ᵐ y ∂(μ.map Prod.snd), Y y = Y' y := by
      rw [← hsnd]
      exact hYm.ae_eq_mk
    exact ae_of_ae_map measurable_snd.aemeasurable h
  have h_eq : (fun ω : Ω × Ω'' ↦ exp (t * (X ω.1 + Y ω.2)))
      =ᵐ[μ] fun ω ↦ exp (t * X' ω.1) * exp (t * Y' ω.2) := by
    filter_upwards [hXeq, hYeq] with ω h1 h2
    rw [h1, h2, mul_add, exp_add]
  rw [integrable_congr h_eq]
  refine ⟨(by fun_prop : Measurable fun ω : Ω × Ω'' ↦ exp (t * X' ω.1) * exp (t * Y' ω.2))
    |>.aestronglyMeasurable, ?_⟩
  rw [hasFiniteIntegral_iff_ofReal (ae_of_all _ fun _ ↦ by positivity)]
  -- the bound on the inner integral
  have h_inner : ∀ᵐ ω' ∂ν, ∀ᵐ x ∂κ ω',
      ∫⁻ y, ENNReal.ofReal (exp (t * Y' y)) ∂η (ω', x) ≤ ENNReal.ofReal (exp (VY * t ^ 2 / 2)) := by
    refine Measure.ae_ae_of_ae_compProd (p := fun p ↦ ∫⁻ y, ENNReal.ofReal (exp (t * Y' y)) ∂η p
      ≤ ENNReal.ofReal (exp (VY * t ^ 2 / 2))) ?_
    filter_upwards [hY''.mgf_le, hY''.ae_integrable_exp_mul ht] with p h_mgf h_int
    rw [← ofReal_integral_eq_lintegral_ofReal h_int (ae_of_all _ fun _ ↦ by positivity)]
    exact ENNReal.ofReal_le_ofReal (h_mgf t ht)
  have hmeas : Measurable fun ω : Ω × Ω'' ↦
      ENNReal.ofReal (exp (t * X' ω.1)) * ENNReal.ofReal (exp (t * Y' ω.2)) := by fun_prop
  calc ∫⁻ ω, ENNReal.ofReal (exp (t * X' ω.1) * exp (t * Y' ω.2)) ∂μ
  _ = ∫⁻ ω', ∫⁻ x, ∫⁻ y, ENNReal.ofReal (exp (t * X' x)) * ENNReal.ofReal (exp (t * Y' y))
      ∂η (ω', x) ∂κ ω' ∂ν := by
    simp_rw [ENNReal.ofReal_mul (exp_pos _).le]
    rw [hμ, Measure.lintegral_bind (Kernel.aemeasurable _) hmeas.aemeasurable]
    congr with ω'
    rw [Kernel.lintegral_compProd _ _ _ hmeas]
  _ ≤ ∫⁻ ω', ∫⁻ x, ENNReal.ofReal (exp (t * X' x)) * ENNReal.ofReal (exp (VY * t ^ 2 / 2))
      ∂κ ω' ∂ν := by
    refine lintegral_mono_ae ?_
    filter_upwards [h_inner] with ω' h_inner
    refine lintegral_mono_ae ?_
    filter_upwards [h_inner] with x hx
    rw [lintegral_const_mul' _ _ ENNReal.ofReal_ne_top]
    gcongr
  _ = (∫⁻ x, ENNReal.ofReal (exp (t * X' x)) ∂(κ ∘ₘ ν))
      * ENNReal.ofReal (exp (VY * t ^ 2 / 2)) := by
    rw [Measure.lintegral_bind (Kernel.aemeasurable _) (by fun_prop),
      ← lintegral_mul_const' _ _ ENNReal.ofReal_ne_top]
    congr with ω'
    rw [lintegral_mul_const' _ _ ENNReal.ofReal_ne_top]
  _ < ∞ := by
    refine ENNReal.mul_lt_top ?_ ENNReal.ofReal_lt_top
    have := (hX''.integrable_exp_mul t ht).2
    rwa [hasFiniteIntegral_iff_ofReal (ae_of_all _ fun _ ↦ by positivity)] at this