-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem Kernel.integral_fn_integral_add ⦃f g : β × γ → E⦄ (F : E → E')
    (hf : Integrable f ((κ ⊗ₖ η) a)) (hg : Integrable g ((κ ⊗ₖ η) a)) :
    ∫ x, F (∫ y, f (x, y) + g (x, y) ∂η (a, x)) ∂κ a =
      ∫ x, F (∫ y, f (x, y) ∂η (a, x) + ∫ y, g (x, y) ∂η (a, x)) ∂κ a

Proof state:
α : 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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
⊢ ∫ (x : β), F (∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x)) ∂κ a =
    ∫ (x : β), F (∫ (y : γ), f (x, y) ∂η (a, x) + ∫ (y : γ), g (x, y) ∂η (a, x)) ∂κ a

Tactic:
refine integral_congr_ae ?_

Result:
α : 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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
⊢ (fun x => F (∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x))) =ᶠ[ae (κ a)] fun x =>
    F (∫ (y : γ), f (x, y) ∂η (a, x) + ∫ (y : γ), g (x, y) ∂η (a, x))

Proof state:
α : 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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
⊢ (fun x => F (∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x))) =ᶠ[ae (κ a)] fun x =>
    F (∫ (y : γ), f (x, y) ∂η (a, x) + ∫ (y : γ), g (x, y) ∂η (a, x))

Tactic:
filter_upwards [hf.ae_of_compProd, hg.ae_of_compProd] with _ h2f h2g

Result:
case 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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
a✝ : β
h2f : Integrable (fun y => f (a✝, y)) (η (a, a✝))
h2g : Integrable (fun y => g (a✝, y)) (η (a, a✝))
⊢ F (∫ (y : γ), f (a✝, y) + g (a✝, y) ∂η (a, a✝)) =
    F (∫ (y : γ), f (a✝, y) ∂η (a, a✝) + ∫ (y : γ), g (a✝, y) ∂η (a, a✝))

Proof state:
case 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
E' : Type u_5
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace ℝ E'
f g : β × γ → E
F : E → E'
hf : Integrable f ((κ ⊗ₖ η) a)
hg : Integrable g ((κ ⊗ₖ η) a)
a✝ : β
h2f : Integrable (fun y => f (a✝, y)) (η (a, a✝))
h2g : Integrable (fun y => g (a✝, y)) (η (a, a✝))
⊢ F (∫ (y : γ), f (a✝, y) + g (a✝, y) ∂η (a, a✝)) =
    F (∫ (y : γ), f (a✝, y) ∂η (a, a✝) + ∫ (y : γ), g (a✝, y) ∂η (a, a✝))

Tactic:
simp [integral_add h2f h2g]

Result:
no goals