-- 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.e_a
α : 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 < ⊤
⊢ (((κ ⊗ₖ η) a) s).toReal = (∫⁻ (a_1 : β), (η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂κ a).toReal

Tactic:
rw [Kernel.compProd_apply hs]

Result:
case pos.h_ind.e_a
α : 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 < ⊤
⊢ (∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ s} ∂κ a).toReal = (∫⁻ (a_1 : β), (η (a, a_1)) (Prod.mk a_1 ⁻¹' s) ∂κ a).toReal

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 (β × γ)
hs : MeasurableSet s
h2s : ((κ ⊗ₖ η) a) s < ⊤
⊢ (((κ ⊗ₖ η) a) s).toReal • c = (∫ (x : β), ((η (a, x)) (Prod.mk x ⁻¹' s)).toReal ∂κ a) • c

Tactic:
congr 1

Result:
case pos.h_ind.e_a
α : 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 < ⊤
⊢ (((κ ⊗ₖ η) a) s).toReal = ∫ (x : β), ((η (a, x)) (Prod.mk x ⁻¹' s)).toReal ∂κ a

Proof state:
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
hfg : f =ᶠ[ae ((κ ⊗ₖ η) a)] g
a✝ : Integrable f ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
⊢ ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a

Tactic:
convert hf using 1

Result:
case h.e'_2
α : 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
⊢ ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a

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

Proof state:
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)

Tactic:
filter_upwards [ae_ae_of_ae_compProd hfg] with x hfgx using
  integral_congr_ae (ae_eq_symm hfgx)

Result:
no goals

Proof state:
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
a✝ : Disjoint (support f) (support g)
i_f : Integrable f ((κ ⊗ₖ η) a)
i_g : Integrable g ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
hg : ∫ (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

Tactic:
simp_rw [integral_add' i_f i_g, Kernel.integral_integral_add' i_f i_g, hf, hg]

Result:
no goals

Proof state:
case pos.h_ind.e_a.hf
α : 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 < ⊤
⊢ ∀ᵐ (x : β) ∂κ a, (η (a, x)) (Prod.mk x ⁻¹' s) < ⊤

Tactic:
exact ae_kernel_lt_top a h2s.ne

Result:
no goals

Proof state:
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

Tactic:
intro f g _ i_f i_g hf hg

Result:
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
a✝ : Disjoint (support f) (support g)
i_f : Integrable f ((κ ⊗ₖ η) a)
i_g : Integrable g ((κ ⊗ₖ η) a)
hf : ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a
hg : ∫ (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