-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem lintegral_compProd' (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel (α × β) γ)
    [IsSFiniteKernel η] (a : α) {f : β → γ → ℝ≥0∞} (hf : Measurable (Function.uncurry f)) :
    ∫⁻ bc, f bc.1 bc.2 ∂(κ ⊗ₖ η) a = ∫⁻ b, ∫⁻ c, f b c ∂η (a, b) ∂κ a

Proof state:
case e_s.h.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

Tactic:
intro c s hs

Result:
case e_s.h.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

Proof state:
case e_s.h.refine_2.e_f.h
α : 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
b : β
⊢ ∫⁻ (c : γ), f (b, c) ∂η (a, b) + ∫⁻ (c : γ), f' (b, c) ∂η (a, b) = ∫⁻ (c : γ), f (b, c) + f' (b, c) ∂η (a, b)

Tactic:
rw [lintegral_add_left]

Result:
case e_s.h.refine_2.e_f.h.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
b : β
⊢ Measurable fun c => f (b, c)

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

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

Result:
no goals

Proof state:
α : 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)
⊢ ⨆ n, ∫⁻ (a : β × γ), (F n) a ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ∫⁻ (c : γ), ⨆ n, (F n) (b, c) ∂η (a, b) ∂κ a

Tactic:
simp_rw [this]

Result:
α : 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)
⊢ ⨆ n, ∫⁻ (a : β × γ), (F n) a ∂(κ ⊗ₖ η) a = ∫⁻ (b : β), ⨆ n, ∫⁻ (c : γ), (F n) (b, c) ∂η (a, b) ∂κ a

Proof state:
α : 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
⊢ Measurable fun b => (η (a, b)) {c | (b, c) ∈ s}

Tactic:
exact (measurable_kernel_prod_mk_left ((measurable_fst.snd.prod_mk measurable_snd) hs)).comp
  measurable_prod_mk_left

Result:
no goals