case refine'_1
f : ℂ →ₐ[ℝ] ℂ
h : ↑f I = I
⊢ ↑f I = ↑(AlgHom.id ℝ ℂ) I

case refine'_2
f : ℂ →ₐ[ℝ] ℂ
h : ↑f I = -I
⊢ ↑f I = ↑↑conjAe I
f : ℂ →ₐ[ℝ] ℂ
⊢ f = AlgHom.id ℝ ℂ ∨ f = ↑conjAe
refine'
    (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp _ _ <;>
  refine' fun h => algHom_ext _
no goals
case refine'_1
f : ℂ →ₐ[ℝ] ℂ
h : ↑f I = I
⊢ ↑f I = ↑(AlgHom.id ℝ ℂ) I

case refine'_2
f : ℂ →ₐ[ℝ] ℂ
h : ↑f I = -I
⊢ ↑f I = ↑↑conjAe I
exacts [h, conj_I.symm ▸ h]
no goals
f : ℂ →ₐ[ℝ] ℂ
⊢ ↑f I ^ 2 = I ^ 2
rw [← map_pow, I_sq, map_neg, map_one]