no goals
K : Type u_1
E : Type ?u.3572488
inst✝ : IsROrC K
z : K
⊢ ↑(↑im z) = I * (↑(starRingEnd K) z - z) / 2
rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
  neg_sub, mul_sub, neg_mul, sub_eq_add_neg]