α : Type u_1
α' : Type ?u.2419590
β : Type u_2
β' : Type ?u.2419596
γ : Type ?u.2419599
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f
hg : Integrable g
⊢ (fun x => F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᶠ[ae μ] fun x =>
    F ((∫ (y : β), f (x, y) ∂ν) - ∫ (y : β), g (x, y) ∂ν)
α : Type u_1
α' : Type ?u.2419590
β : Type u_2
β' : Type ?u.2419596
γ : Type ?u.2419599
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f
hg : Integrable g
⊢ (∫ (x : α), F (∫ (y : β), f (x, y) - g (x, y) ∂ν) ∂μ) =
    ∫ (x : α), F ((∫ (y : β), f (x, y) ∂ν) - ∫ (y : β), g (x, y) ∂ν) ∂μ
refine' integral_congr_ae _
case h
α : Type u_1
α' : Type ?u.2419590
β : Type u_2
β' : Type ?u.2419596
γ : Type ?u.2419599
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f
hg : Integrable g
a✝ : α
h2f : Integrable fun y => f (a✝, y)
h2g : Integrable fun y => g (a✝, y)
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F ((∫ (y : β), f (a✝, y) ∂ν) - ∫ (y : β), g (a✝, y) ∂ν)
α : Type u_1
α' : Type ?u.2419590
β : Type u_2
β' : Type ?u.2419596
γ : Type ?u.2419599
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f
hg : Integrable g
⊢ (fun x => F (∫ (y : β), f (x, y) - g (x, y) ∂ν)) =ᶠ[ae μ] fun x =>
    F ((∫ (y : β), f (x, y) ∂ν) - ∫ (y : β), g (x, y) ∂ν)
filter_upwards [hf.prod_right_ae, hg.prod_right_ae] with _ h2f h2g
no goals
case h
α : Type u_1
α' : Type ?u.2419590
β : Type u_2
β' : Type ?u.2419596
γ : Type ?u.2419599
E : Type u_3
inst✝¹² : MeasurableSpace α
inst✝¹¹ : MeasurableSpace α'
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : MeasurableSpace β'
inst✝⁸ : MeasurableSpace γ
μ μ' : Measure α
ν ν' : Measure β
τ : Measure γ
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SigmaFinite ν
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : CompleteSpace E
inst✝³ : SigmaFinite μ
E' : Type u_4
inst✝² : NormedAddCommGroup E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
f g : α × β → E
F : E → E'
hf : Integrable f
hg : Integrable g
a✝ : α
h2f : Integrable fun y => f (a✝, y)
h2g : Integrable fun y => g (a✝, y)
⊢ F (∫ (y : β), f (a✝, y) - g (a✝, y) ∂ν) = F ((∫ (y : β), f (a✝, y) ∂ν) - ∫ (y : β), g (a✝, y) ∂ν)
simp [integral_sub h2f h2g]