-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem integral_compProd :
    ∀ {f : β × γ → E} (_ : Integrable f ((κ ⊗ₖ η) a)),
      ∫ z, f z ∂(κ ⊗ₖ η) a = ∫ x, ∫ y, f (x, y) ∂η (a, x) ∂κ a

Proof state:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ ∀ (c : E) ⦃s : Set (β × γ)⦄,
    MeasurableSet s →
      ((κ ⊗ₖ η) a) s < ⊤ →
        ∫ (z : β × γ), s.indicator (fun x => c) z ∂(κ ⊗ₖ η) a =
          ∫ (x : β), ∫ (y : γ), s.indicator (fun x => c) (x, y) ∂η (a, x) ∂κ a

Tactic:
intro c s hs h2s

Result:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ ∫ (z : β × γ), s.indicator (fun x => c) z ∂(κ ⊗ₖ η) a =
    ∫ (x : β), ∫ (y : γ), s.indicator (fun x => c) (x, y) ∂η (a, x) ∂κ a

Proof state:
case h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae ((κ ⊗ₖ η) a)] g
a✝ : Integrable f ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
⊢ ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a

Tactic:
apply integral_congr_ae

Result:
case h.e'_3.h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
f g : β × γ → E
hfg : f =ᶠ[ae ((κ ⊗ₖ η) a)] g
a✝ : Integrable f ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
⊢ (fun a_1 => ∫ (y : γ), g (a_1, y) ∂η (a, a_1)) =ᶠ[ae (κ a)] fun a_1 => ∫ (y : γ), f (a_1, y) ∂η (a, a_1)

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ Integrable f✝ ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f✝ z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f✝ (x, y) ∂η (a, x) ∂κ a

Tactic:
apply Integrable.induction

Result:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ ∀ (c : E) ⦃s : Set (β × γ)⦄,
    MeasurableSet s →
      ((κ ⊗ₖ η) a) s < ⊤ →
        ∫ (z : β × γ), s.indicator (fun x => c) z ∂(κ ⊗ₖ η) a =
          ∫ (x : β), ∫ (y : γ), s.indicator (fun x => c) (x, y) ∂η (a, x) ∂κ a

case pos.h_add
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ ∀ ⦃f g : β × γ → E⦄,
    Disjoint (support f) (support g) →
      Integrable f ((κ ⊗ₖ η) a) →
        Integrable g ((κ ⊗ₖ η) a) →
          ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a →
            ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a →
              ∫ (z : β × γ), (f + g) z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂η (a, x) ∂κ a

case pos.h_closed
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ IsClosed {f | ∫ (z : β × γ), ↑↑f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a}

case pos.h_ae
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ ∀ ⦃f g : β × γ → E⦄,
    f =ᶠ[ae ((κ ⊗ₖ η) a)] g →
      Integrable f ((κ ⊗ₖ η) a) →
        ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a →
          ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a

Proof state:
case pos.h_ind.e_a.hfm
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
c : E
s : Set (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ AEMeasurable (fun x => (η (a, x)) (Prod.mk x ⁻¹' s)) (κ a)

Tactic:
exact (Kernel.measurable_kernel_prod_mk_left' hs _).aemeasurable

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ Integrable f✝ ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f✝ z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f✝ (x, y) ∂η (a, x) ∂κ a

case neg
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : ¬CompleteSpace E
⊢ Integrable f✝ ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f✝ z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f✝ (x, y) ∂η (a, x) ∂κ a

Tactic:
swap

Result:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : ¬CompleteSpace E
⊢ Integrable f✝ ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f✝ z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f✝ (x, y) ∂η (a, x) ∂κ a

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f✝ : β × γ → E
hE : CompleteSpace E
⊢ Integrable f✝ ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f✝ z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f✝ (x, y) ∂η (a, x) ∂κ a