no goals
α : Type u_1
E : Type u_2
F : Type ?u.968060
𝕜 : Type ?u.968063
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : f =ᵐ[μ] 0
⊢ (∫ (a : α), f a ∂μ) = 0
simp [integral_congr_ae hf, integral_zero]