Theorem: circleIntegral.integral_add (RMT4/cindex.lean)

State before:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
c : ℂ
R : ℝ
hf : CircleIntegrable f c R
hg : CircleIntegrable g c R
⊢ (∮ (z : ℂ) in C(c, R), f z + g z) = (∮ (z : ℂ) in C(c, R), f z) + ∮ (z : ℂ) in C(c, R), g z
Tactic:
simp only [circleIntegral, smul_add, intervalIntegral.integral_add hf.out hg.out]
State after:
no goals