no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → ℂ
a : E
c : ℂ
R : ℝ
⊢ (∮ (z : ℂ) in C(c, R), f z • a) = (∮ (z : ℂ) in C(c, R), f z) • a
simp only [circleIntegral, intervalIntegral.integral_smul_const, ← smul_assoc]