Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
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 f' : SimpleFunc (β × γ) ℝ≥0∞
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑f')
hf_eq : ∫⁻ (a : β × γ), f a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c : γ), f (a_1, c) ∂η (a, a_1) ∂κ a
hf'_eq : ∫⁻ (a : β × γ), f' a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c : γ), f' (a_1, c) ∂η (a, a_1) ∂κ a
⊢ ∫⁻ (x : β × γ), f x + f' x ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) + f' (b, c) ∂η (a, b) ∂κ a

Tactic:
rw [lintegral_add_left (SimpleFunc.measurable _), hf_eq, hf'_eq, ← lintegral_add_left]

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 f' : SimpleFunc (β × γ) ℝ≥0∞
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑f')
hf_eq : ∫⁻ (a : β × γ), f a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c : γ), f (a_1, c) ∂η (a, a_1) ∂κ a
hf'_eq : ∫⁻ (a : β × γ), f' a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c : γ), f' (a_1, c) ∂η (a, a_1) ∂κ a
⊢ ∫⁻ (a_1 : β), ∫⁻ (c : γ), f (a_1, c) ∂η (a, a_1) + ∫⁻ (c : γ), f' (a_1, c) ∂η (a, a_1) ∂κ a =
    ∫⁻ (b : β), ∫⁻ (c : γ), f (b, c) + f' (b, c) ∂η (a, b) ∂κ a

case refine_2.hf
α : 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 f' : SimpleFunc (β × γ) ℝ≥0∞
a✝ : Disjoint (Function.support ⇑f) (Function.support ⇑f')
hf_eq : ∫⁻ (a : β × γ), f a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c : γ), f (a_1, c) ∂η (a, a_1) ∂κ a
hf'_eq : ∫⁻ (a : β × γ), f' a ∂(κ ⊗ₖ η) a = ∫⁻ (a_1 : β), ∫⁻ (c : γ), f' (a_1, c) ∂η (a, a_1) ∂κ a
⊢ Measurable fun a_1 ↦ ∫⁻ (c : γ), f (a_1, c) ∂η (a, a_1)