a : { x // x ∈ circle }
h : ↑rotation a = conjLie
⊢ False
a : { x // x ∈ circle }
⊢ ↑rotation a ≠ conjLie
intro h
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑(↑rotation a) 1 = ↑(starRingEnd ℂ) 1
⊢ False
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
⊢ False
have h1 : rotation a 1 = conj 1 := LinearIsometryEquiv.congr_fun h 1
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑(↑rotation a) 1 = ↑(starRingEnd ℂ) 1
hI : ↑(↑rotation a) I = ↑(starRingEnd ℂ) I
⊢ False
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑(↑rotation a) 1 = ↑(starRingEnd ℂ) 1
⊢ False
have hI : rotation a I = conj I := LinearIsometryEquiv.congr_fun h I
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑a = 1
hI : ↑(↑rotation a) I = ↑(starRingEnd ℂ) I
⊢ False
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑(↑rotation a) 1 = ↑(starRingEnd ℂ) 1
hI : ↑(↑rotation a) I = ↑(starRingEnd ℂ) I
⊢ False
rw [rotation_apply, RingHom.map_one, mul_one] at h1
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑a = 1
hI : 1 = 0
⊢ False
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑a = 1
hI : ↑(↑rotation a) I = ↑(starRingEnd ℂ) I
⊢ False
rw [rotation_apply, conj_I, ← neg_one_mul, mul_left_inj' I_ne_zero, h1, eq_neg_self_iff] at hI
no goals
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑a = 1
hI : 1 = 0
⊢ False
exact one_ne_zero hI