f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqRe f) = (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I).re
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqRe f) = (CauSeq.lim f).re
rw [lim_eq_lim_im_add_lim_re]
no goals
f : CauSeq ℂ ↑abs
⊢ CauSeq.lim (cauSeqRe f) = (↑(CauSeq.lim (cauSeqRe f)) + ↑(CauSeq.lim (cauSeqIm f)) * I).re
simp [ofReal']