-- 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
⊢ Measurable fun a => ⨆ n, ∫⁻ (b : β), (F n) (a, b) ∂κ a

Tactic:
refine .iSup fun n => ?_

Result:
α : 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

Proof state:
case h_mono
α : 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
a : α
⊢ Monotone fun n b => (F n) (a, b)

Tactic:
exact fun i j hij b => SimpleFunc.monotone_eapprox (uncurry f) hij _

Result:
no goals

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
⊢ Measurable fun a => ∫⁻ (b : β), ⨆ n, (F n) (a, b) ∂κ a

Tactic:
simp_rw [this]

Result:
α : 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
⊢ Measurable fun a => ⨆ n, ∫⁻ (b : β), (F n) (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 : ℕ
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
⊢ (fun a => ∫⁻ (b : β), g₁ (a, b) + g₂ (a, b) ∂κ a) =
    (fun a => ∫⁻ (b : β), g₁ (a, b) ∂κ a) + fun a => ∫⁻ (b : β), g₂ (a, b) ∂κ a

Tactic:
ext1 a

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 : α
⊢ ∫⁻ (b : β), g₁ (a, b) + g₂ (a, b) ∂κ a =
    ((fun a => ∫⁻ (b : β), g₁ (a, b) ∂κ a) + fun a => ∫⁻ (b : β), g₂ (a, b) ∂κ a) a

Proof state:
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 : ℕ
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
⊢ Measurable fun a => ∫⁻ (b : β), g₁ (a, b) + g₂ (a, b) ∂κ a

Tactic:
have h_add :
  (fun a => ∫⁻ b, g₁ (a, b) + g₂ (a, b) ∂κ a) =
    (fun a => ∫⁻ b, g₁ (a, b) ∂κ a) + fun a => ∫⁻ b, g₂ (a, b) ∂κ a := by
  ext1 a
  rw [Pi.add_apply]
  erw [lintegral_add_left (g₁.measurable.comp measurable_prod_mk_left)]
  simp_rw [Function.comp_apply]

Result:
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 : ℕ
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
h_add :
  (fun a => ∫⁻ (b : β), g₁ (a, b) + g₂ (a, b) ∂κ a) =
    (fun a => ∫⁻ (b : β), g₁ (a, b) ∂κ a) + fun a => ∫⁻ (b : β), g₂ (a, b) ∂κ a
⊢ Measurable fun a => ∫⁻ (b : β), g₁ (a, b) + g₂ (a, b) ∂κ a

Proof state:
case hf
α : 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
a : α
⊢ ∀ (n : ℕ), Measurable fun b => (F n) (a, b)

Tactic:
exact fun n => (F n).measurable.comp measurable_prod_mk_left

Result:
no goals

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 : α × β), ⨆ n, (F n) a = uncurry f a
⊢ Measurable fun a => ∫⁻ (b : β), f a b ∂κ a

Tactic:
simp only [Prod.forall, uncurry_apply_pair] at h

Result:
α : 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
⊢ Measurable fun a => ∫⁻ (b : β), f a b ∂κ a