α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum (fun x => ↑re (f x)) (↑re c) ∧ HasSum (fun x => ↑im (f x)) (↑im c) → HasSum f c
α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum f c ↔ HasSum (fun x => ↑re (f x)) (↑re c) ∧ HasSum (fun x => ↑im (f x)) (↑im c)
refine' ⟨fun h => ⟨hasSum_re _ h, hasSum_im _ h⟩, _⟩
case intro
α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
h₁ : HasSum (fun x => ↑re (f x)) (↑re c)
h₂ : HasSum (fun x => ↑im (f x)) (↑im c)
⊢ HasSum f c
α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
⊢ HasSum (fun x => ↑re (f x)) (↑re c) ∧ HasSum (fun x => ↑im (f x)) (↑im c) → HasSum f c
rintro ⟨h₁, h₂⟩
no goals
case intro
α : Type u_2
𝕜 : Type u_1
inst✝ : IsROrC 𝕜
f : α → 𝕜
c : 𝕜
h₁ : HasSum (fun x => ↑re (f x)) (↑re c)
h₂ : HasSum (fun x => ↑im (f x)) (↑im c)
⊢ HasSum f c
simpa only [re_add_im] using
  ((hasSum_ofReal 𝕜).mpr h₁).add (((hasSum_ofReal 𝕜).mpr h₂).mul_right I)