z : ℂ
this : ↑2 * I = 2 * I
⊢ ↑z.im = (z - ↑(starRingEnd ℂ) z) / (2 * I)
z : ℂ
⊢ ↑z.im = (z - ↑(starRingEnd ℂ) z) / (2 * I)
have : (↑2 : ℝ ) * I = 2 * I := by rfl
no goals
z : ℂ
this : ↑2 * I = 2 * I
⊢ ↑z.im = (z - ↑(starRingEnd ℂ) z) / (2 * I)
simp only [sub_conj, ofReal_mul, ofReal_one, ofReal_bit0, mul_right_comm, this,
  mul_div_cancel_left _ (mul_ne_zero two_ne_zero I_ne_zero : 2 * I ≠ 0)]
no goals
z : ℂ
⊢ ↑2 * I = 2 * I
rfl