f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).re = 0 ∧ ((↑f I).im = I.im ∨ (↑f I).im = -I.im)
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ ↑f I = I ∨ ↑f I = -I
simp only [ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).re = 0

case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).im = I.im ∨ (↑f I).im = -I.im
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).re = 0 ∧ ((↑f I).im = I.im ∨ (↑f I).im = -I.im)
constructor
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).re = I.re
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).re = 0
rw [← I_re]
no goals
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).re = I.re
exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ ∀ (z : ℂ), (↑(LinearIsometryEquiv.toLinearIsometry f) z).re = z.re
case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).im = I.im ∨ (↑f I).im = -I.im
apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ (↑(LinearIsometryEquiv.toLinearIsometry f) z).re = z.re
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ ∀ (z : ℂ), (↑(LinearIsometryEquiv.toLinearIsometry f) z).re = z.re
intro z
no goals
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ (↑(LinearIsometryEquiv.toLinearIsometry f) z).re = z.re
rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]
case refine'_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
⊢ f.toLinearEquiv = conjLie.toLinearEquiv
case refine'_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
⊢ f = conjLie
apply LinearIsometryEquiv.toLinearEquiv_injective
case refine'_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
⊢ ∀ (i : Fin 2), ↑f.toLinearEquiv (↑basisOneI i) = ↑conjLie.toLinearEquiv (↑basisOneI i)
case refine'_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
⊢ f.toLinearEquiv = conjLie.toLinearEquiv
apply Complex.basisOneI.ext'
case refine'_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
i : Fin 2
⊢ ↑f.toLinearEquiv (↑basisOneI i) = ↑conjLie.toLinearEquiv (↑basisOneI i)
case refine'_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
⊢ ∀ (i : Fin 2), ↑f.toLinearEquiv (↑basisOneI i) = ↑conjLie.toLinearEquiv (↑basisOneI i)
intro i
no goals
case refine'_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
i : Fin 2
⊢ ↑f.toLinearEquiv (↑basisOneI i) = ↑conjLie.toLinearEquiv (↑basisOneI i)
fin_cases i <;> simp [h, h']