no goals
K : Type u_1
E : Type ?u.2851475
inst✝ : IsROrC K
z : K
⊢ ↑(starRingEnd K) (↑(↑re z) + ↑(↑im z) * I) = ↑(↑re z) - ↑(↑im z) * I
rw [map_add, map_mul, conj_I, conj_ofReal, conj_ofReal, mul_neg, sub_eq_add_neg]