no goals
K : Type u_1
E : Type ?u.2979461
inst✝ : IsROrC K
z : K
⊢ z - ↑(starRingEnd K) z = ↑(↑re z) + ↑(↑im z) * I - (↑(↑re z) - ↑(↑im z) * I)
rw [re_add_im, ← conj_eq_re_sub_im]
no goals
K : Type u_1
E : Type ?u.2979461
inst✝ : IsROrC K
z : K
⊢ ↑(↑re z) + ↑(↑im z) * I - (↑(↑re z) - ↑(↑im z) * I) = 2 * ↑(↑im z) * I
rw [add_sub_sub_cancel, ← two_mul, mul_assoc]