no goals
f : ℂ →ₗᵢ[ℝ] ℂ
h₃ : ∀ (z : ℂ), z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
z : ℂ
⊢ (↑f z).re = z.re
simpa [ext_iff, add_re, add_im, conj_re, conj_im, ← two_mul,
  show (2 : ℝ) ≠ 0 by simp [two_ne_zero]] using (h₃ z).symm
no goals
f : ℂ →ₗᵢ[ℝ] ℂ
h₃ : ∀ (z : ℂ), z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
z : ℂ
⊢ 2 ≠ 0
simp [two_ne_zero]