f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
⊢ ∃ a, f = ↑rotation a ∨ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
f : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ ∃ a, f = ↑rotation a ∨ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
let a : circle := ⟨f 1, by rw [mem_circle_iff_abs, ← Complex.norm_eq_abs, f.norm_map, norm_one]⟩
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
⊢ f = ↑rotation a ∨ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
⊢ ∃ a, f = ↑rotation a ∨ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
use a
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)
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
⊢ f = ↑rotation a ∨ f = LinearIsometryEquiv.trans conjLie (↑rotation a)
have : (f.trans (rotation a).symm) 1 = 1 := by simpa using rotation_apply a⁻¹ (f 1)
case 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

case 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)
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)
refine' (linear_isometry_complex_aux this).imp (fun h₁ => _) fun h₂ => _
no goals
f : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ ↑f 1 ∈ circle
rw [mem_circle_iff_abs, ← Complex.norm_eq_abs, f.norm_map, norm_one]
no goals
f : ℂ ≃ₗᵢ[ℝ] ℂ
a : { x // x ∈ circle } := { val := ↑f 1, property := (_ : ↑f 1 ∈ circle) }
⊢ ↑(LinearIsometryEquiv.trans f (LinearIsometryEquiv.symm (↑rotation a))) 1 = 1
simpa using rotation_apply a⁻¹ (f 1)
no goals
case 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
simpa using eq_mul_of_inv_mul_eq h₁
no goals
case 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)
exact eq_mul_of_inv_mul_eq h₂