z : ℂ
this : ↑2 = 2
⊢ ↑z.re = (z + ↑(starRingEnd ℂ) z) / 2
z : ℂ
⊢ ↑z.re = (z + ↑(starRingEnd ℂ) z) / 2
have : (↑(↑2 : ℝ) : ℂ)  = (2 : ℂ) := by rfl
no goals
z : ℂ
this : ↑2 = 2
⊢ ↑z.re = (z + ↑(starRingEnd ℂ) z) / 2
simp only [add_conj, ofReal_mul, ofReal_one, ofReal_bit0, this,
  mul_div_cancel_left (z.re : ℂ) two_ne_zero]
no goals
z : ℂ
⊢ ↑2 = 2
rfl