[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]


[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
⊢ ↑T v ∈ (eigenspace T μ)ᗮ
[PROOFSTEP]
intro w hw
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ inner w (↑T v) = 0
[PROOFSTEP]
have : T w = (μ : 𝕜) • w := by rwa [mem_eigenspace_iff] at hw
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
⊢ ↑T w = μ • w
[PROOFSTEP]
rwa [mem_eigenspace_iff] at hw
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
v : E
hv : v ∈ (eigenspace T μ)ᗮ
w : E
hw : w ∈ eigenspace T μ
this : ↑T w = μ • w
⊢ inner w (↑T v) = 0
[PROOFSTEP]
simp [← hT w, this, inner_smul_left, hv w hw]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
hμ : HasEigenvalue T μ
⊢ ↑(starRingEnd 𝕜) μ = μ
[PROOFSTEP]
obtain ⟨v, hv₁, hv₂⟩ := hμ.exists_hasEigenvector
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : v ∈ eigenspace T μ
hv₂ : v ≠ 0
⊢ ↑(starRingEnd 𝕜) μ = μ
[PROOFSTEP]
rw [mem_eigenspace_iff] at hv₁
[GOAL]
case intro.intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
hμ : HasEigenvalue T μ
v : E
hv₁ : ↑T v = μ • v
hv₂ : v ≠ 0
⊢ ↑(starRingEnd 𝕜) μ = μ
[PROOFSTEP]
simpa [hv₂, inner_smul_left, inner_smul_right, hv₁] using hT v v
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
⊢ OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T μ }) fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)
[PROOFSTEP]
rintro μ ν hμν ⟨v, hv⟩ ⟨w, hw⟩
[GOAL]
case mk.mk
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw }) =
    0
[PROOFSTEP]
by_cases hv' : v = 0
[GOAL]
case pos
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : v = 0
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw }) =
    0
[PROOFSTEP]
simp [hv']
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw }) =
    0
[PROOFSTEP]
have H := hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector ⟨hv, hv'⟩)
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv : v ∈ eigenspace T μ
w : E
hw : w ∈ eigenspace T ν
hv' : ¬v = 0
H : ↑(starRingEnd 𝕜) μ = μ
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw }) =
    0
[PROOFSTEP]
rw [mem_eigenspace_iff] at hv hw
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : ↑T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : ↑T w = ν • w
hv' : ¬v = 0
H : ↑(starRingEnd 𝕜) μ = μ
⊢ inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv✝ })
      (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw✝ }) =
    0
[PROOFSTEP]
refine' Or.resolve_left _ hμν.symm
[GOAL]
case neg
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ ν : 𝕜
hμν : μ ≠ ν
v : E
hv✝ : v ∈ eigenspace T μ
hv : ↑T v = μ • v
w : E
hw✝ : w ∈ eigenspace T ν
hw : ↑T w = ν • w
hv' : ¬v = 0
H : ↑(starRingEnd 𝕜) μ = μ
⊢ ν = μ ∨
    inner (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) μ) { val := v, property := hv✝ })
        (↑((fun μ => Submodule.subtypeₗᵢ (eigenspace T μ)) ν) { val := w, property := hw✝ }) =
      0
[PROOFSTEP]
simpa [inner_smul_left, inner_smul_right, hv, hw, H] using (hT v w).symm
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
v : E
hv : v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
[PROOFSTEP]
rw [← Submodule.iInf_orthogonal] at hv ⊢
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
v : E
hv : v ∈ ⨅ (i : 𝕜), (eigenspace T i)ᗮ
⊢ ↑T v ∈ ⨅ (i : 𝕜), (eigenspace T i)ᗮ
[PROOFSTEP]
exact T.iInf_invariant hT.invariant_orthogonalComplement_eigenspace v hv
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
⊢ eigenspace (restrict T (_ : ∀ ⦃v : E⦄, v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ → ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ)) μ = ⊥
[PROOFSTEP]
set p : Submodule 𝕜 E := (⨆ μ, eigenspace T μ)ᗮ
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ eigenspace (restrict T (_ : ∀ ⦃v : E⦄, v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ → ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ)) μ = ⊥
[PROOFSTEP]
refine' eigenspace_restrict_eq_bot hT.orthogonalComplement_iSup_eigenspaces_invariant _
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
⊢ Disjoint (eigenspace T μ) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
[PROOFSTEP]
have H₂ : eigenspace T μ ⟂ p := (Submodule.isOrtho_orthogonal_right _).mono_left (le_iSup _ _)
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
μ : 𝕜
p : Submodule 𝕜 E := (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
H₂ : eigenspace T μ ⟂ p
⊢ Disjoint (eigenspace T μ) (⨆ (μ : 𝕜), eigenspace T μ)ᗮ
[PROOFSTEP]
exact H₂.disjoint
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
⊢ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ = ⊥
[PROOFSTEP]
have hT' : IsSymmetric _ := hT.restrict_invariant hT.orthogonalComplement_iSup_eigenspaces_invariant
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
hT' : IsSymmetric (restrict T (_ : ∀ ⦃v : E⦄, v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ → ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ))
⊢ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ = ⊥
[PROOFSTEP]
haveI := hT'.subsingleton_of_no_eigenvalue_finiteDimensional hT.orthogonalComplement_iSup_eigenspaces
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
hT' : IsSymmetric (restrict T (_ : ∀ ⦃v : E⦄, v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ → ↑T v ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ))
this : Subsingleton { x // x ∈ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ }
⊢ (⨆ (μ : 𝕜), eigenspace T μ)ᗮ = ⊥
[PROOFSTEP]
exact Submodule.eq_bot_of_subsingleton _
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
⊢ (⨆ (μ : { μ // eigenspace T μ ≠ ⊥ }), eigenspace T ↑μ)ᗮ = ⊥
[PROOFSTEP]
rw [iSup_ne_bot_subtype, hT.orthogonalComplement_iSup_eigenspaces_eq_bot]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT✝ : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
hT : Fact (IsSymmetric T)
μ : Eigenvalues T
⊢ CompleteSpace { x // x ∈ eigenspace T (↑T μ) }
[PROOFSTEP]
infer_instance
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
⊢ ↑(diagonalization hT) (↑T v) μ = ↑T μ • ↑(diagonalization hT) v μ
[PROOFSTEP]
suffices
  ∀ w : PiLp 2 fun μ : Eigenvalues T => eigenspace T μ,
    T (hT.diagonalization.symm w) = hT.diagonalization.symm fun μ => (μ : 𝕜) • w μ
  by
  simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
    congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
this :
  ∀ (w : PiLp 2 fun μ => { x // x ∈ eigenspace T (↑T μ) }),
    ↑T (↑(LinearIsometryEquiv.symm (diagonalization hT)) w) =
      ↑(LinearIsometryEquiv.symm (diagonalization hT)) fun μ => ↑T μ • w μ
⊢ ↑(diagonalization hT) (↑T v) μ = ↑T μ • ↑(diagonalization hT) v μ
[PROOFSTEP]
simpa only [LinearIsometryEquiv.symm_apply_apply, LinearIsometryEquiv.apply_symm_apply] using
  congr_arg (fun w => hT.diagonalization w μ) (this (hT.diagonalization v))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
⊢ ∀ (w : PiLp 2 fun μ => { x // x ∈ eigenspace T (↑T μ) }),
    ↑T (↑(LinearIsometryEquiv.symm (diagonalization hT)) w) =
      ↑(LinearIsometryEquiv.symm (diagonalization hT)) fun μ => ↑T μ • w μ
[PROOFSTEP]
intro w
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ => { x // x ∈ eigenspace T (↑T μ) }
⊢ ↑T (↑(LinearIsometryEquiv.symm (diagonalization hT)) w) =
    ↑(LinearIsometryEquiv.symm (diagonalization hT)) fun μ => ↑T μ • w μ
[PROOFSTEP]
have hwT : ∀ μ, T (w μ) = (μ : 𝕜) • w μ := fun μ => mem_eigenspace_iff.1 (w μ).2
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
v : E
μ : Eigenvalues T
w : PiLp 2 fun μ => { x // x ∈ eigenspace T (↑T μ) }
hwT : ∀ (μ : Eigenvalues T), ↑T ↑(w μ) = ↑(↑T μ • w μ)
⊢ ↑T (↑(LinearIsometryEquiv.symm (diagonalization hT)) w) =
    ↑(LinearIsometryEquiv.symm (diagonalization hT)) fun μ => ↑T μ • w μ
[PROOFSTEP]
simp only [hwT, diagonalization_symm_apply, map_sum, Submodule.coe_smul_of_tower]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
⊢ HasEigenvector T (↑(eigenvalues hT hn i)) (↑(eigenvectorBasis hT hn) i)
[PROOFSTEP]
let v : E := hT.eigenvectorBasis hn i
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
⊢ HasEigenvector T (↑(eigenvalues hT hn i)) (↑(eigenvectorBasis hT hn) i)
[PROOFSTEP]
let μ : 𝕜 := (hT.direct_sum_isInternal.subordinateOrthonormalBasisIndex hn i hT.orthogonalFamily_eigenspaces').val
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ HasEigenvector T (↑(eigenvalues hT hn i)) (↑(eigenvectorBasis hT hn) i)
[PROOFSTEP]
simp_rw [eigenvalues]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ HasEigenvector T
    (↑(↑IsROrC.re
        (↑T
          (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn
            (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
            (_ :
              OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
                Submodule.subtypeₗᵢ (eigenspace T (↑T μ)))))))
    (↑(eigenvectorBasis hT hn) i)
[PROOFSTEP]
change HasEigenvector T (IsROrC.re μ) v
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ HasEigenvector T (↑(↑IsROrC.re μ)) v
[PROOFSTEP]
have key : HasEigenvector T μ v :=
  by
  have H₁ : v ∈ eigenspace T μ := by
    simp_rw [eigenvectorBasis]
    exact hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i hT.orthogonalFamily_eigenspaces'
  have H₂ : v ≠ 0 := by simpa using (hT.eigenvectorBasis hn).toBasis.ne_zero i
  exact ⟨H₁, H₂⟩
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ HasEigenvector T μ v
[PROOFSTEP]
have H₁ : v ∈ eigenspace T μ := by
  simp_rw [eigenvectorBasis]
  exact hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i hT.orthogonalFamily_eigenspaces'
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ v ∈ eigenspace T μ
[PROOFSTEP]
simp_rw [eigenvectorBasis]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
⊢ ↑(DirectSum.IsInternal.subordinateOrthonormalBasis hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ))
          (_ :
            OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
              Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
      i ∈
    eigenspace T
      (↑T
        (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn
          (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
          (_ :
            OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
              Submodule.subtypeₗᵢ (eigenspace T (↑T μ)))))
[PROOFSTEP]
exact hT.direct_sum_isInternal.subordinateOrthonormalBasis_subordinate hn i hT.orthogonalFamily_eigenspaces'
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
H₁ : v ∈ eigenspace T μ
⊢ HasEigenvector T μ v
[PROOFSTEP]
have H₂ : v ≠ 0 := by simpa using (hT.eigenvectorBasis hn).toBasis.ne_zero i
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
H₁ : v ∈ eigenspace T μ
⊢ v ≠ 0
[PROOFSTEP]
simpa using (hT.eigenvectorBasis hn).toBasis.ne_zero i
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
H₁ : v ∈ eigenspace T μ
H₂ : v ≠ 0
⊢ HasEigenvector T μ v
[PROOFSTEP]
exact ⟨H₁, H₂⟩
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
key : HasEigenvector T μ v
⊢ HasEigenvector T (↑(↑IsROrC.re μ)) v
[PROOFSTEP]
have re_μ : ↑(IsROrC.re μ) = μ := by
  rw [← IsROrC.conj_eq_iff_re]
  exact hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector key)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
key : HasEigenvector T μ v
⊢ ↑(↑IsROrC.re μ) = μ
[PROOFSTEP]
rw [← IsROrC.conj_eq_iff_re]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
key : HasEigenvector T μ v
⊢ ↑(starRingEnd 𝕜) μ = μ
[PROOFSTEP]
exact hT.conj_eigenvalue_eq_self (hasEigenvalue_of_hasEigenvector key)
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
i : Fin n
v : E := ↑(eigenvectorBasis hT hn) i
μ : 𝕜 :=
  ↑T
    (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn (_ : DirectSum.IsInternal fun μ => eigenspace T (↑T μ)) i
      (_ :
        OrthogonalFamily 𝕜 (fun μ => { x // x ∈ eigenspace T (↑T μ) }) fun μ =>
          Submodule.subtypeₗᵢ (eigenspace T (↑T μ))))
key : HasEigenvector T μ v
re_μ : ↑(↑IsROrC.re μ) = μ
⊢ HasEigenvector T (↑(↑IsROrC.re μ)) v
[PROOFSTEP]
simpa [re_μ] using key
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
⊢ ↑(eigenvectorBasis hT hn).repr (↑T v) i = ↑(eigenvalues hT hn i) * ↑(eigenvectorBasis hT hn).repr v i
[PROOFSTEP]
suffices
  ∀ w : EuclideanSpace 𝕜 (Fin n),
    T ((hT.eigenvectorBasis hn).repr.symm w) = (hT.eigenvectorBasis hn).repr.symm fun i => hT.eigenvalues hn i * w i
  by
  simpa [OrthonormalBasis.sum_repr_symm] using
    congr_arg (fun v => (hT.eigenvectorBasis hn).repr v i) (this ((hT.eigenvectorBasis hn).repr v))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
this :
  ∀ (w : EuclideanSpace 𝕜 (Fin n)),
    ↑T (↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) w) =
      ↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) fun i => ↑(eigenvalues hT hn i) * w i
⊢ ↑(eigenvectorBasis hT hn).repr (↑T v) i = ↑(eigenvalues hT hn i) * ↑(eigenvectorBasis hT hn).repr v i
[PROOFSTEP]
simpa [OrthonormalBasis.sum_repr_symm] using
  congr_arg (fun v => (hT.eigenvectorBasis hn).repr v i) (this ((hT.eigenvectorBasis hn).repr v))
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
⊢ ∀ (w : EuclideanSpace 𝕜 (Fin n)),
    ↑T (↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) w) =
      ↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) fun i => ↑(eigenvalues hT hn i) * w i
[PROOFSTEP]
intro w
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ↑T (↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) w) =
    ↑(LinearIsometryEquiv.symm (eigenvectorBasis hT hn).repr) fun i => ↑(eigenvalues hT hn i) * w i
[PROOFSTEP]
simp_rw [← OrthonormalBasis.sum_repr_symm, LinearMap.map_sum, LinearMap.map_smul, apply_eigenvectorBasis]
[GOAL]
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ∑ x : Fin n, w x • ↑(eigenvalues hT hn x) • ↑(eigenvectorBasis hT hn) x =
    ∑ x : Fin n, (↑(eigenvalues hT hn x) * w x) • ↑(eigenvectorBasis hT hn) x
[PROOFSTEP]
apply Fintype.sum_congr
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
⊢ ∀ (a : Fin n),
    w a • ↑(eigenvalues hT hn a) • ↑(eigenvectorBasis hT hn) a =
      (↑(eigenvalues hT hn a) * w a) • ↑(eigenvectorBasis hT hn) a
[PROOFSTEP]
intro a
[GOAL]
case h
𝕜 : Type u_1
inst✝³ : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : IsSymmetric T
inst✝ : FiniteDimensional 𝕜 E
n : ℕ
hn : FiniteDimensional.finrank 𝕜 E = n
v : E
i : Fin n
w : EuclideanSpace 𝕜 (Fin n)
a : Fin n
⊢ w a • ↑(eigenvalues hT hn a) • ↑(eigenvectorBasis hT hn) a =
    (↑(eigenvalues hT hn a) * w a) • ↑(eigenvectorBasis hT hn) a
[PROOFSTEP]
rw [smul_smul, mul_comm]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : 𝕜
v : E
T : E →ₗ[𝕜] E
h : v ∈ eigenspace T μ
⊢ inner v (↑T v) = μ * ↑‖v‖ ^ 2
[PROOFSTEP]
simp only [mem_eigenspace_iff.mp h, inner_smul_right, inner_self_eq_norm_sq_to_K]
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
⊢ 0 ≤ μ
[PROOFSTEP]
obtain ⟨v, hv⟩ := hμ.exists_hasEigenvector
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 ≤ μ
[PROOFSTEP]
have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 < ‖v‖ ^ 2
[PROOFSTEP]
simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ 0 ≤ μ
[PROOFSTEP]
have : IsROrC.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 :=
  by
  have :=
    congr_arg IsROrC.re
      (inner_product_apply_eigenvector hv.1)
        -- porting note: why can't `exact_mod_cast` do this? These lemmas are marked `norm_cast`
  rw [← IsROrC.ofReal_pow, ← IsROrC.ofReal_mul] at this
  exact_mod_cast this
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
have :=
  congr_arg IsROrC.re
    (inner_product_apply_eigenvector hv.1)
      -- porting note: why can't `exact_mod_cast` do this? These lemmas are marked `norm_cast`
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = ↑IsROrC.re (↑μ * ↑‖v‖ ^ 2)
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
rw [← IsROrC.ofReal_pow, ← IsROrC.ofReal_mul] at this
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = ↑IsROrC.re ↑(μ * ‖v‖ ^ 2)
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
exact_mod_cast this
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 ≤ ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
⊢ 0 ≤ μ
[PROOFSTEP]
exact (zero_le_mul_right hpos).mp (this ▸ hnn v)
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
⊢ 0 < μ
[PROOFSTEP]
obtain ⟨v, hv⟩ := hμ.exists_hasEigenvector
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 < μ
[PROOFSTEP]
have hpos : (0 : ℝ) < ‖v‖ ^ 2 := by simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
⊢ 0 < ‖v‖ ^ 2
[PROOFSTEP]
simpa only [sq_pos_iff, norm_ne_zero_iff] using hv.2
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ 0 < μ
[PROOFSTEP]
have : IsROrC.re ⟪v, T v⟫ = μ * ‖v‖ ^ 2 :=
  by
  have :=
    congr_arg IsROrC.re
      (inner_product_apply_eigenvector hv.1)
        -- porting note: why can't `exact_mod_cast` do this? These lemmas are marked `norm_cast`
  rw [← IsROrC.ofReal_pow, ← IsROrC.ofReal_mul] at this
  exact_mod_cast this
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
have :=
  congr_arg IsROrC.re
    (inner_product_apply_eigenvector hv.1)
      -- porting note: why can't `exact_mod_cast` do this? These lemmas are marked `norm_cast`
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = ↑IsROrC.re (↑μ * ↑‖v‖ ^ 2)
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
rw [← IsROrC.ofReal_pow, ← IsROrC.ofReal_mul] at this
[GOAL]
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = ↑IsROrC.re ↑(μ * ‖v‖ ^ 2)
⊢ ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
[PROOFSTEP]
exact_mod_cast this
[GOAL]
case intro
𝕜 : Type u_1
inst✝² : IsROrC 𝕜
dec_𝕜 : DecidableEq 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : ℝ
T : E →ₗ[𝕜] E
hμ : HasEigenvalue T ↑μ
hnn : ∀ (x : E), 0 < ↑IsROrC.re (inner x (↑T x))
v : E
hv : HasEigenvector T (↑μ) v
hpos : 0 < ‖v‖ ^ 2
this : ↑IsROrC.re (inner v (↑T v)) = μ * ‖v‖ ^ 2
⊢ 0 < μ
[PROOFSTEP]
exact (zero_lt_mul_right hpos).mp (this ▸ hnn v)