-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem _root_.Measurable.lintegral_kernel_prod_right {f : α → β → ℝ≥0∞}
    (hf : Measurable (uncurry f)) : Measurable fun a => ∫⁻ b, f a b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
⊢ Measurable fun a => ∫⁻ (b : β), (F n) (a, b) ∂κ a

Tactic:
refine SimpleFunc.induction
  (P := fun f => Measurable (fun (a : α) => ∫⁻ (b : β), f (a, b) ∂κ a)) ?_ ?_ (F n)

Result:
case refine_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
⊢ ∀ (c : ℝ≥0∞) {s : Set (α × β)} (hs : MeasurableSet s),
    (fun f => Measurable fun a => ∫⁻ (b : β), f (a, b) ∂κ a)
      (SimpleFunc.piecewise s hs (SimpleFunc.const (α × β) c) (SimpleFunc.const (α × β) 0))

case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
⊢ ∀ ⦃f g : SimpleFunc (α × β) ℝ≥0∞⦄,
    Disjoint (support ⇑f) (support ⇑g) →
      (fun f => Measurable fun a => ∫⁻ (b : β), f (a, b) ∂κ a) f →
        (fun f => Measurable fun a => ∫⁻ (b : β), f (a, b) ∂κ a) g →
          (fun f => Measurable fun a => ∫⁻ (b : β), f (a, b) ∂κ a) (f + g)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ⇑g₁) (support ⇑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), g₁ (a, b) ∂κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), g₂ (a, b) ∂κ a
a : α
⊢ ∫⁻ (b : β), g₁ (a, b) + g₂ (a, b) ∂κ a = ∫⁻ (b : β), g₁ (a, b) ∂κ a + ∫⁻ (b : β), g₂ (a, b) ∂κ a

Tactic:
erw [lintegral_add_left (g₁.measurable.comp measurable_prod_mk_left)]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (uncurry f)
F : ℕ → SimpleFunc (α × β) ℝ≥0∞ := SimpleFunc.eapprox (uncurry f)
h : ∀ (a : α) (b : β), ⨆ n, (F n) (a, b) = f a b
this : ∀ (a : α), ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a = ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a
n : ℕ
g₁ g₂ : SimpleFunc (α × β) ℝ≥0∞
a✝ : Disjoint (support ⇑g₁) (support ⇑g₂)
hm₁ : Measurable fun a => ∫⁻ (b : β), g₁ (a, b) ∂κ a
hm₂ : Measurable fun a => ∫⁻ (b : β), g₂ (a, b) ∂κ a
a : α
⊢ ∫⁻ (a_1 : β), (⇑g₁ ∘ Prod.mk a) a_1 ∂κ a + ∫⁻ (a_1 : β), g₂ (a, a_1) ∂κ a =
    ∫⁻ (b : β), g₁ (a, b) ∂κ a + ∫⁻ (b : β), g₂ (a, b) ∂κ a