K : Type u_1
E : Type ?u.2663909
inst✝ : IsROrC K
r : ℝ
⊢ ↑re (↑(starRingEnd K) ↑r) = ↑re ↑r ∧ ↑im (↑(starRingEnd K) ↑r) = ↑im ↑r
K : Type u_1
E : Type ?u.2663909
inst✝ : IsROrC K
r : ℝ
⊢ ↑(starRingEnd K) ↑r = ↑r
rw [ext_iff]
no goals
K : Type u_1
E : Type ?u.2663909
inst✝ : IsROrC K
r : ℝ
⊢ ↑re (↑(starRingEnd K) ↑r) = ↑re ↑r ∧ ↑im (↑(starRingEnd K) ↑r) = ↑im ↑r
simp only [ofReal_im, conj_im, eq_self_iff_true, conj_re, and_self_iff, neg_zero]