Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, (F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), (F n) (b, c) ∂η (a, b)
h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b ↦ ∫⁻ (c : γ), f' (b, c) ∂η (a, b)
n : ℕ
⊢ ∀ (c : ℝ≥0∞) {s : Set (β × γ)} (hs : MeasurableSet s),
    ∫⁻ (a : β × γ),
        (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0)) a ∂(κ ⊗ₖ η) a =
      ∫⁻ (a_1 : β),
        ∫⁻ (c_1 : γ),
          (SimpleFunc.piecewise s hs (SimpleFunc.const (β × γ) c) (SimpleFunc.const (β × γ) 0))
            (a_1, c_1) ∂η (a, a_1) ∂κ a

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, (F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), (F n) (b, c) ∂η (a, b)
h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b ↦ ∫⁻ (c : γ), f' (b, c) ∂η (a, b)
n : ℕ
⊢ ∀ ⦃f g : SimpleFunc (β × γ) ℝ≥0∞⦄,
    Disjoint (Function.support ⇑f) (Function.support ⇑g) →
      ∫⁻ (a : β × γ), f a ∂(κ ⊗ₖ η) a = ∫⁻ (a_2 : β), ∫⁻ (c : γ), f (a_2, c) ∂η (a, a_2) ∂κ a →
        ∫⁻ (a : β × γ), g a ∂(κ ⊗ₖ η) a = ∫⁻ (a_3 : β), ∫⁻ (c : γ), g (a_3, c) ∂η (a, a_3) ∂κ a →
          ∫⁻ (a : β × γ), (f + g) a ∂(κ ⊗ₖ η) a = ∫⁻ (a_4 : β), ∫⁻ (c : γ), (f + g) (a_4, c) ∂η (a, a_4) ∂κ a

Tactic:
· intro c s hs
    simp +unfoldPartialApp only [SimpleFunc.const_zero,
      SimpleFunc.coe_piecewise, SimpleFunc.coe_const, SimpleFunc.coe_zero,
      Set.piecewise_eq_indicator, Function.const, lintegral_indicator_const hs]
    rw [compProd_apply hs, ← lintegral_const_mul c _]
    swap
    · exact (measurable_kernel_prodMk_left ((measurable_fst.snd.prodMk measurable_snd) hs)).comp
        measurable_prodMk_left
    congr
    ext1 b
    rw [lintegral_indicator_const_comp measurable_prodMk_left hs]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β → γ → ℝ≥0∞
hf : Measurable (Function.uncurry f)
F : ℕ → SimpleFunc (β × γ) ℝ≥0∞ := SimpleFunc.eapprox (Function.uncurry f)
h : ∀ (a : β) (b : γ), ⨆ n, (F n) (a, b) = f a b
h_mono : Monotone F
this : ∀ (b : β), ∫⁻ (c : γ), ⨆ n, (F n) (b, c) ∂η (a, b) = ⨆ n, ∫⁻ (c : γ), (F n) (b, c) ∂η (a, b)
h_some_meas_integral : ∀ (f' : SimpleFunc (β × γ) ℝ≥0∞), Measurable fun b ↦ ∫⁻ (c : γ), f' (b, c) ∂η (a, b)
n : ℕ
⊢ ∀ ⦃f g : SimpleFunc (β × γ) ℝ≥0∞⦄,
    Disjoint (Function.support ⇑f) (Function.support ⇑g) →
      ∫⁻ (a : β × γ), f a ∂(κ ⊗ₖ η) a = ∫⁻ (a_2 : β), ∫⁻ (c : γ), f (a_2, c) ∂η (a, a_2) ∂κ a →
        ∫⁻ (a : β × γ), g a ∂(κ ⊗ₖ η) a = ∫⁻ (a_3 : β), ∫⁻ (c : γ), g (a_3, c) ∂η (a, a_3) ∂κ a →
          ∫⁻ (a : β × γ), (f + g) a ∂(κ ⊗ₖ η) a = ∫⁻ (a_4 : β), ∫⁻ (c : γ), (f + g) (a_4, c) ∂η (a, a_4) ∂κ a