[GOAL]
a : { x // x ∈ circle }
src✝ : ℂ ≃ₗ[ℝ] ℂ := DistribMulAction.toLinearEquiv ℝ ℂ a
x : ℂ
⊢ ↑Complex.abs (↑a * x) = ↑Complex.abs x
[PROOFSTEP]
rw [map_mul, abs_coe_circle, one_mul]
[GOAL]
a b : { x // x ∈ circle }
⊢ LinearIsometryEquiv.trans (↑rotation a) (↑rotation b) = ↑rotation (b * a)
[PROOFSTEP]
ext1
[GOAL]
case h
a b : { x // x ∈ circle }
x✝ : ℂ
⊢ ↑(LinearIsometryEquiv.trans (↑rotation a) (↑rotation b)) x✝ = ↑(↑rotation (b * a)) x✝
[PROOFSTEP]
simp
[GOAL]
a : { x // x ∈ circle }
⊢ ↑rotation a ≠ conjLie
[PROOFSTEP]
intro h
[GOAL]
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
⊢ False
[PROOFSTEP]
have h1 : rotation a 1 = conj 1 := LinearIsometryEquiv.congr_fun h 1
[GOAL]
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑(↑rotation a) 1 = ↑(starRingEnd ℂ) 1
⊢ False
[PROOFSTEP]
have hI : rotation a I = conj I := LinearIsometryEquiv.congr_fun h I
[GOAL]
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑(↑rotation a) 1 = ↑(starRingEnd ℂ) 1
hI : ↑(↑rotation a) I = ↑(starRingEnd ℂ) I
⊢ False
[PROOFSTEP]
rw [rotation_apply, RingHom.map_one, mul_one] at h1 
[GOAL]
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑a = 1
hI : ↑(↑rotation a) I = ↑(starRingEnd ℂ) I
⊢ False
[PROOFSTEP]
rw [rotation_apply, conj_I, ← neg_one_mul, mul_left_inj' I_ne_zero, h1, eq_neg_self_iff] at hI 
[GOAL]
a : { x // x ∈ circle }
h : ↑rotation a = conjLie
h1 : ↑a = 1
hI : 1 = 0
⊢ False
[PROOFSTEP]
exact one_ne_zero hI
[GOAL]
e : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ ↑e 1 / ↑(↑Complex.abs (↑e 1)) ∈ circle
[PROOFSTEP]
simp
[GOAL]
a : { x // x ∈ circle }
⊢ ↑(rotationOf (↑rotation a)) = ↑a
[PROOFSTEP]
simp
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h₃ : ∀ (z : ℂ), z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
z : ℂ
⊢ (↑f z).re = z.re
[PROOFSTEP]
simpa [ext_iff, add_re, add_im, conj_re, conj_im, ← two_mul, show (2 : ℝ) ≠ 0 by simp [two_ne_zero]] using (h₃ z).symm
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h₃ : ∀ (z : ℂ), z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
z : ℂ
⊢ 2 ≠ 0
[PROOFSTEP]
simp [two_ne_zero]
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (↑f z).re = z.re
z : ℂ
⊢ (↑f z).im = z.im ∨ (↑f z).im = -z.im
[PROOFSTEP]
have h₁ := f.norm_map z
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (↑f z).re = z.re
z : ℂ
h₁ : ‖↑f z‖ = ‖z‖
⊢ (↑f z).im = z.im ∨ (↑f z).im = -z.im
[PROOFSTEP]
simp only [Complex.abs_def, norm_eq_abs] at h₁ 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h₂ : ∀ (z : ℂ), (↑f z).re = z.re
z : ℂ
h₁ : Real.sqrt (↑normSq (↑f z)) = Real.sqrt (↑normSq z)
⊢ (↑f z).im = z.im ∨ (↑f z).im = -z.im
[PROOFSTEP]
rwa [Real.sqrt_inj (normSq_nonneg _) (normSq_nonneg _), normSq_apply (f z), normSq_apply z, h₂, add_left_cancel_iff,
  mul_self_eq_mul_self_iff] at h₁ 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
have : ‖f z - 1‖ = ‖z - 1‖ := by rw [← f.norm_map (z - 1), f.map_sub, h]
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ ‖↑f z - 1‖ = ‖z - 1‖
[PROOFSTEP]
rw [← f.norm_map (z - 1), f.map_sub, h]
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ‖↑f z - 1‖ = ‖z - 1‖
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
apply_fun fun x => x ^ 2 at this 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ‖↑f z - 1‖ ^ 2 = ‖z - 1‖ ^ 2
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
simp only [norm_eq_abs, ← normSq_eq_abs] at this 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ↑normSq (↑f z - 1) = ↑normSq (z - 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
rw [← ofReal_inj, ← mul_conj, ← mul_conj] at this 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : (↑f z - 1) * ↑(starRingEnd ℂ) (↑f z - 1) = (z - 1) * ↑(starRingEnd ℂ) (z - 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
rw [RingHom.map_sub, RingHom.map_sub] at this 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : (↑f z - 1) * (↑(starRingEnd ℂ) (↑f z) - ↑(starRingEnd ℂ) 1) = (z - 1) * (↑(starRingEnd ℂ) z - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
simp only [sub_mul, mul_sub, one_mul, mul_one] at this 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this :
  ↑f z * ↑(starRingEnd ℂ) (↑f z) - ↑(starRingEnd ℂ) (↑f z) - (↑f z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1) =
    z * ↑(starRingEnd ℂ) z - ↑(starRingEnd ℂ) z - (z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
rw [mul_conj, normSq_eq_abs, ← norm_eq_abs, LinearIsometry.norm_map] at this 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this :
  ↑(‖z‖ ^ 2) - ↑(starRingEnd ℂ) (↑f z) - (↑f z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1) =
    z * ↑(starRingEnd ℂ) z - ↑(starRingEnd ℂ) z - (z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
rw [mul_conj, normSq_eq_abs, ← norm_eq_abs] at this 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this :
  ↑(‖z‖ ^ 2) - ↑(starRingEnd ℂ) (↑f z) - (↑f z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1) =
    ↑(‖z‖ ^ 2) - ↑(starRingEnd ℂ) z - (z * ↑(starRingEnd ℂ) 1 - ↑(starRingEnd ℂ) 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
simp only [sub_sub, sub_right_inj, mul_one, ofReal_pow, RingHom.map_one, norm_eq_abs] at this 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ↑(starRingEnd ℂ) (↑f z) + (↑f z - 1) = ↑(starRingEnd ℂ) z + (z - 1)
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
simp only [add_sub, sub_left_inj] at this 
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
this : ↑(starRingEnd ℂ) (↑f z) + ↑f z = ↑(starRingEnd ℂ) z + z
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
rw [add_comm, ← this, add_comm]
[GOAL]
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ (↑f z).re = z.re
[PROOFSTEP]
apply LinearIsometry.re_apply_eq_re_of_add_conj_eq
[GOAL]
case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ ∀ (z : ℂ), z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
intro z
[GOAL]
case h₃
f : ℂ →ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z✝ z : ℂ
⊢ z + ↑(starRingEnd ℂ) z = ↑f z + ↑(starRingEnd ((fun x => ℂ) z)) (↑f z)
[PROOFSTEP]
apply LinearIsometry.im_apply_eq_im h
[GOAL]
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = conjLie
[PROOFSTEP]
have h0 : f I = I ∨ f I = -I :=
  by
  simp only [ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]
  constructor
  · rw [← I_re]
    exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I
  · apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry
    intro z
    rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]
[GOAL]
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ ↑f I = I ∨ ↑f I = -I
[PROOFSTEP]
simp only [ext_iff, ← and_or_left, neg_re, I_re, neg_im, neg_zero]
[GOAL]
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).re = 0 ∧ ((↑f I).im = I.im ∨ (↑f I).im = -I.im)
[PROOFSTEP]
constructor
[GOAL]
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).re = 0
[PROOFSTEP]
rw [← I_re]
[GOAL]
case left
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).re = I.re
[PROOFSTEP]
exact @LinearIsometry.re_apply_eq_re f.toLinearIsometry h I
[GOAL]
case right
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ (↑f I).im = I.im ∨ (↑f I).im = -I.im
[PROOFSTEP]
apply @LinearIsometry.im_apply_eq_im_or_neg_of_re_apply_eq_re f.toLinearIsometry
[GOAL]
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
⊢ ∀ (z : ℂ), (↑(LinearIsometryEquiv.toLinearIsometry f) z).re = z.re
[PROOFSTEP]
intro z
[GOAL]
case right.h₂
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
z : ℂ
⊢ (↑(LinearIsometryEquiv.toLinearIsometry f) z).re = z.re
[PROOFSTEP]
rw [@LinearIsometry.re_apply_eq_re f.toLinearIsometry h]
[GOAL]
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
⊢ f = LinearIsometryEquiv.refl ℝ ℂ ∨ f = conjLie
[PROOFSTEP]
refine' h0.imp (fun h' : f I = I => _) fun h' : f I = -I => _
[GOAL]
case refine'_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = I
⊢ f = LinearIsometryEquiv.refl ℝ ℂ
[PROOFSTEP]
apply LinearIsometryEquiv.toLinearEquiv_injective
[GOAL]
case refine'_1.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = I
⊢ f.toLinearEquiv = (LinearIsometryEquiv.refl ℝ ℂ).toLinearEquiv
[PROOFSTEP]
apply Complex.basisOneI.ext'
[GOAL]
case refine'_1.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = I
⊢ ∀ (i : Fin 2), ↑f.toLinearEquiv (↑basisOneI i) = ↑(LinearIsometryEquiv.refl ℝ ℂ).toLinearEquiv (↑basisOneI i)
[PROOFSTEP]
intro i
[GOAL]
case refine'_1.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = I
i : Fin 2
⊢ ↑f.toLinearEquiv (↑basisOneI i) = ↑(LinearIsometryEquiv.refl ℝ ℂ).toLinearEquiv (↑basisOneI i)
[PROOFSTEP]
fin_cases i
[GOAL]
case refine'_1.a.head
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = I
⊢ ↑f.toLinearEquiv (↑basisOneI { val := 0, isLt := (_ : 0 < 2) }) =
    ↑(LinearIsometryEquiv.refl ℝ ℂ).toLinearEquiv (↑basisOneI { val := 0, isLt := (_ : 0 < 2) })
[PROOFSTEP]
simp [h, h']
[GOAL]
case refine'_1.a.tail.head
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = I
⊢ ↑f.toLinearEquiv (↑basisOneI { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑(LinearIsometryEquiv.refl ℝ ℂ).toLinearEquiv (↑basisOneI { val := 1, isLt := (_ : (fun a => a < 2) 1) })
[PROOFSTEP]
simp [h, h']
[GOAL]
case refine'_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
⊢ f = conjLie
[PROOFSTEP]
apply LinearIsometryEquiv.toLinearEquiv_injective
[GOAL]
case refine'_2.a
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
⊢ f.toLinearEquiv = conjLie.toLinearEquiv
[PROOFSTEP]
apply Complex.basisOneI.ext'
[GOAL]
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)
[PROOFSTEP]
intro i
[GOAL]
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)
[PROOFSTEP]
fin_cases i
[GOAL]
case refine'_2.a.head
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
⊢ ↑f.toLinearEquiv (↑basisOneI { val := 0, isLt := (_ : 0 < 2) }) =
    ↑conjLie.toLinearEquiv (↑basisOneI { val := 0, isLt := (_ : 0 < 2) })
[PROOFSTEP]
simp [h, h']
[GOAL]
case refine'_2.a.tail.head
f : ℂ ≃ₗᵢ[ℝ] ℂ
h : ↑f 1 = 1
h0 : ↑f I = I ∨ ↑f I = -I
h' : ↑f I = -I
⊢ ↑f.toLinearEquiv (↑basisOneI { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑conjLie.toLinearEquiv (↑basisOneI { val := 1, isLt := (_ : (fun a => a < 2) 1) })
[PROOFSTEP]
simp [h, h']
[GOAL]
f : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ ∃ a, f = ↑rotation a ∨ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
[PROOFSTEP]
let a : circle := ⟨f 1, by rw [mem_circle_iff_abs, ← Complex.norm_eq_abs, f.norm_map, norm_one]⟩
[GOAL]
f : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ ↑f 1 ∈ circle
[PROOFSTEP]
rw [mem_circle_iff_abs, ← Complex.norm_eq_abs, f.norm_map, norm_one]
[GOAL]
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
⊢ ∃ a, f = ↑rotation a ∨ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
[PROOFSTEP]
use a
[GOAL]
case h
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
⊢ f = ↑rotation a ∨ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
[PROOFSTEP]
have : (f.trans (rotation a).symm) 1 = 1 := by simpa using rotation_apply a⁻¹ (f 1)
[GOAL]
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
⊢ ↑(LinearIsometryEquiv.trans f (LinearIsometryEquiv.symm (↑rotation a))) 1 = 1
[PROOFSTEP]
simpa using rotation_apply a⁻¹ (f 1)
[GOAL]
case h
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
this : ↑(LinearIsometryEquiv.trans f (LinearIsometryEquiv.symm (↑rotation a))) 1 = 1
⊢ f = ↑rotation a ∨ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
[PROOFSTEP]
refine' (linear_isometry_complex_aux this).imp (fun h₁ => _) fun h₂ => _
[GOAL]
case h.refine'_1
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
this : ↑(LinearIsometryEquiv.trans f (LinearIsometryEquiv.symm (↑rotation a))) 1 = 1
h₁ : LinearIsometryEquiv.trans f (LinearIsometryEquiv.symm (↑rotation a)) = LinearIsometryEquiv.refl ℝ ℂ
⊢ f = ↑rotation a
[PROOFSTEP]
simpa using eq_mul_of_inv_mul_eq h₁
[GOAL]
case h.refine'_2
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
this : ↑(LinearIsometryEquiv.trans f (LinearIsometryEquiv.symm (↑rotation a))) 1 = 1
h₂ : LinearIsometryEquiv.trans f (LinearIsometryEquiv.symm (↑rotation a)) = conjLie
⊢ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
[PROOFSTEP]
exact eq_mul_of_inv_mul_eq h₂
[GOAL]
a : { x // x ∈ circle }
⊢ (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0
[PROOFSTEP]
simp [pow_two, ← normSq_apply]
[GOAL]
a : { x // x ∈ circle }
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) ↑(↑rotation a).toLinearEquiv =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0))
[PROOFSTEP]
ext i j
[GOAL]
case a.h
a : { x // x ∈ circle }
i j : Fin 2
⊢ ↑(LinearMap.toMatrix basisOneI basisOneI) (↑(↑rotation a).toLinearEquiv) i j =
    ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0)) i j
[PROOFSTEP]
simp [LinearMap.toMatrix_apply]
[GOAL]
case a.h
a : { x // x ∈ circle }
i j : Fin 2
⊢ Matrix.vecCons ((↑a).re * (Matrix.vecCons 1 ![I] j).re - (↑a).im * (Matrix.vecCons 1 ![I] j).im)
      ![(↑a).re * (Matrix.vecCons 1 ![I] j).im + (↑a).im * (Matrix.vecCons 1 ![I] j).re] i =
    Matrix.vecCons (Matrix.vecCons (↑a).re ![-(↑a).im] j) (fun i => Matrix.vecCons (↑a).im ![(↑a).re] j) i
[PROOFSTEP]
fin_cases i
[GOAL]
case a.h.head
a : { x // x ∈ circle }
j : Fin 2
⊢ Matrix.vecCons ((↑a).re * (Matrix.vecCons 1 ![I] j).re - (↑a).im * (Matrix.vecCons 1 ![I] j).im)
      ![(↑a).re * (Matrix.vecCons 1 ![I] j).im + (↑a).im * (Matrix.vecCons 1 ![I] j).re]
      { val := 0, isLt := (_ : 0 < 2) } =
    Matrix.vecCons (Matrix.vecCons (↑a).re ![-(↑a).im] j) (fun i => Matrix.vecCons (↑a).im ![(↑a).re] j)
      { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.tail.head
a : { x // x ∈ circle }
j : Fin 2
⊢ Matrix.vecCons ((↑a).re * (Matrix.vecCons 1 ![I] j).re - (↑a).im * (Matrix.vecCons 1 ![I] j).im)
      ![(↑a).re * (Matrix.vecCons 1 ![I] j).im + (↑a).im * (Matrix.vecCons 1 ![I] j).re]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    Matrix.vecCons (Matrix.vecCons (↑a).re ![-(↑a).im] j) (fun i => Matrix.vecCons (↑a).im ![(↑a).re] j)
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
fin_cases j
[GOAL]
case a.h.head.head
a : { x // x ∈ circle }
⊢ Matrix.vecCons
      ((↑a).re * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).re -
        (↑a).im * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).im)
      ![(↑a).re * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).im +
          (↑a).im * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).re]
      { val := 0, isLt := (_ : 0 < 2) } =
    Matrix.vecCons (Matrix.vecCons (↑a).re ![-(↑a).im] { val := 0, isLt := (_ : 0 < 2) })
      (fun i => Matrix.vecCons (↑a).im ![(↑a).re] { val := 0, isLt := (_ : 0 < 2) }) { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp
[GOAL]
case a.h.head.tail.head
a : { x // x ∈ circle }
⊢ Matrix.vecCons
      ((↑a).re * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).re -
        (↑a).im * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).im)
      ![(↑a).re * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).im +
          (↑a).im * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).re]
      { val := 0, isLt := (_ : 0 < 2) } =
    Matrix.vecCons (Matrix.vecCons (↑a).re ![-(↑a).im] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
      (fun i => Matrix.vecCons (↑a).im ![(↑a).re] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
      { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp
[GOAL]
case a.h.tail.head.head
a : { x // x ∈ circle }
⊢ Matrix.vecCons
      ((↑a).re * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).re -
        (↑a).im * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).im)
      ![(↑a).re * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).im +
          (↑a).im * (Matrix.vecCons 1 ![I] { val := 0, isLt := (_ : 0 < 2) }).re]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    Matrix.vecCons (Matrix.vecCons (↑a).re ![-(↑a).im] { val := 0, isLt := (_ : 0 < 2) })
      (fun i => Matrix.vecCons (↑a).im ![(↑a).re] { val := 0, isLt := (_ : 0 < 2) })
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp
[GOAL]
case a.h.tail.head.tail.head
a : { x // x ∈ circle }
⊢ Matrix.vecCons
      ((↑a).re * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).re -
        (↑a).im * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).im)
      ![(↑a).re * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).im +
          (↑a).im * (Matrix.vecCons 1 ![I] { val := 1, isLt := (_ : (fun a => a < 2) 1) }).re]
      { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    Matrix.vecCons (Matrix.vecCons (↑a).re ![-(↑a).im] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
      (fun i => Matrix.vecCons (↑a).im ![(↑a).re] { val := 1, isLt := (_ : (fun a => a < 2) 1) })
      { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp
[GOAL]
a : { x // x ∈ circle }
⊢ ↑LinearMap.det ↑(↑rotation a).toLinearEquiv = 1
[PROOFSTEP]
rw [← LinearMap.det_toMatrix basisOneI, toMatrix_rotation, Matrix.det_fin_two]
[GOAL]
a : { x // x ∈ circle }
⊢ ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0)) 0 0 *
        ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0)) 1 1 -
      ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0)) 0 1 *
        ↑(Matrix.planeConformalMatrix (↑a).re (↑a).im (_ : (↑a).re ^ 2 + (↑a).im ^ 2 ≠ 0)) 1 0 =
    1
[PROOFSTEP]
simp [← normSq_apply]
[GOAL]
a : { x // x ∈ circle }
⊢ ↑LinearEquiv.det (↑rotation a).toLinearEquiv = 1
[PROOFSTEP]
rw [← Units.eq_iff, LinearEquiv.coe_det, det_rotation, Units.val_one]
