case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ ∀ (z : ℂ), z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ (↑f z).re = z.re
apply LinearIsometry.re_apply_eq_re_of_add_conj_eq
case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z✝ z : ℂ
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ ∀ (z : ℂ), z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
intro z
no goals
case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z✝ z : ℂ
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
apply LinearIsometry.im_apply_eq_im h