Theorem: Matrix.spectral_theorem (CvxLean/Lib/Math/LinearAlgebra/Matrix/Spectrum.lean)

State before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n) * A = diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)
Tactic:
rw [basis_toMatrix_basisFun_mul]
State after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (of fun i j => (xs.toBasis.repr (A.transpose j)) i) =
    diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)

State before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
⊢ (of fun i j => (xs.toBasis.repr (A.transpose j)) i) =
    diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)
Tactic:
ext i j
State after:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j

State before:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Tactic:
let xs' := xs.reindex (Fintype.equivOfCardEq (Fintype.card_fin _)).symm
State after:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j

State before:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Tactic:
let as' : Fin (Fintype.card n) → ℝ :=
  fun i => as <| (Fintype.equivOfCardEq (Fintype.card_fin _)) i
State after:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j

State before:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Tactic:
have hxs' : ∀ j, Module.End.HasEigenvector (Matrix.toLin' A) (as' j) (xs' j) := by
  simp only [xs', OrthonormalBasis.coe_reindex, Equiv.symm_symm]
  intros j
  exact (hxs ((Fintype.equivOfCardEq (Fintype.card_fin _)) j))
State after:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j

State before:
case a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j
Tactic:
convert @LinearMap.spectral_theorem' 𝕜 _
  (PiLp 2 (fun (_ : n) => 𝕜)) _ _ (Fintype.card n) (Matrix.toLin' A)
  (EuclideanSpace.single j 1)
  ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm i)
  xs' as' hxs'
State after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr ((toLin' A) (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)

case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)

State before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr ((toLin' A) (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)

case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
{ erw [toLin'_apply]
  simp only [xs', OrthonormalBasis.coe_toBasis_repr_apply, of_apply,
    OrthonormalBasis.repr_reindex]
  erw [Equiv.symm_apply_apply, EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2, mulVec_single]
  simp_rw [mul_one]
  rfl }
State after:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)

State before:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
{ simp only [diagonal_mul, Function.comp]
  erw [Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply,
    OrthonormalBasis.repr_reindex, Pi.basisFun_apply, LinearMap.coe_stdBasis,
    EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2,
    Equiv.symm_apply_apply, Equiv.apply_symm_apply]
  congr; simp }
State after:
no goals

State before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
Tactic:
simp only [xs', OrthonormalBasis.coe_reindex, Equiv.symm_symm]
State after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) ((⇑xs ∘ ⇑(Fintype.equivOfCardEq ⋯)) j)

State before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
⊢ ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) ((⇑xs ∘ ⇑(Fintype.equivOfCardEq ⋯)) j)
Tactic:
intros j
State after:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j✝ : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
j : Fin (Fintype.card n)
⊢ Module.End.HasEigenvector (toLin' A) (↑(as' j)) ((⇑xs ∘ ⇑(Fintype.equivOfCardEq ⋯)) j)

State before:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j✝ : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
j : Fin (Fintype.card n)
⊢ Module.End.HasEigenvector (toLin' A) (↑(as' j)) ((⇑xs ∘ ⇑(Fintype.equivOfCardEq ⋯)) j)
Tactic:
exact (hxs ((Fintype.equivOfCardEq (Fintype.card_fin _)) j))
State after:
no goals

State before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr ((toLin' A) (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
erw [toLin'_apply]
State after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr (A.mulVec (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)

State before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ of (fun i j => (xs.toBasis.repr (A.transpose j)) i) i j =
    xs'.repr (A.mulVec (EuclideanSpace.single j 1)) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
simp only [xs', OrthonormalBasis.coe_toBasis_repr_apply, of_apply,
  OrthonormalBasis.repr_reindex]
State after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ xs.repr (A.transpose j) i =
    xs.repr (A.mulVec (EuclideanSpace.single j 1))
      ((Fintype.equivOfCardEq ⋯).symm.symm ((Fintype.equivOfCardEq ⋯).symm i))

State before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ xs.repr (A.transpose j) i =
    xs.repr (A.mulVec (EuclideanSpace.single j 1))
      ((Fintype.equivOfCardEq ⋯).symm.symm ((Fintype.equivOfCardEq ⋯).symm i))
Tactic:
erw [Equiv.symm_apply_apply, EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2, mulVec_single]
State after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ EquivLike.coe xs.repr (A.transpose j) i = xs.repr (fun i => A i j * 1) i

State before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ EquivLike.coe xs.repr (A.transpose j) i = xs.repr (fun i => A i j * 1) i
Tactic:
simp_rw [mul_one]
State after:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ EquivLike.coe xs.repr (A.transpose j) i = xs.repr (fun i => A i j) i

State before:
case h.e'_2
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ EquivLike.coe xs.repr (A.transpose j) i = xs.repr (fun i => A i j) i
Tactic:
rfl
State after:
no goals

State before:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ (diagonal (RCLike.ofReal ∘ as) * xs.toBasis.toMatrix ⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
simp only [diagonal_mul, Function.comp]
State after:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ ↑(as i) * xs.toBasis.toMatrix (⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)

State before:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ ↑(as i) * xs.toBasis.toMatrix (⇑(Pi.basisFun 𝕜 n)) i j =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) * xs'.repr (EuclideanSpace.single j 1) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
erw [Basis.toMatrix_apply, OrthonormalBasis.coe_toBasis_repr_apply,
  OrthonormalBasis.repr_reindex, Pi.basisFun_apply, LinearMap.coe_stdBasis,
  EuclideanSpace.single, WithLp.equiv_symm_pi_apply 2,
  Equiv.symm_apply_apply, Equiv.apply_symm_apply]
State after:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ ↑(as i) * EquivLike.coe xs.repr (Pi.single j 1) i =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) *
      xs.repr (fun a => Decidable.rec (fun h => (fun h => 0 a) h) (fun h => (fun h => ⋯ ▸ 1) h) (inst✝ a j)) i

State before:
case h.e'_3
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ ↑(as i) * EquivLike.coe xs.repr (Pi.single j 1) i =
    ↑(as' ((Fintype.equivOfCardEq ⋯).symm i)) *
      xs.repr (fun a => Decidable.rec (fun h => (fun h => 0 a) h) (fun h => (fun h => ⋯ ▸ 1) h) (inst✝ a j)) i
Tactic:
congr
State after:
case h.e'_3.e_a.e_a.e_a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ i = (Fintype.equivOfCardEq ⋯) ((Fintype.equivOfCardEq ⋯).symm i)

State before:
case h.e'_3.e_a.e_a.e_a
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
inst✝² : DecidableEq 𝕜
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n 𝕜
xs : OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
as : n → ℝ
hxs : ∀ (j : n), Module.End.HasEigenvector (toLin' A) (↑(as j)) (xs j)
i j : n
xs' : OrthonormalBasis (Fin (Fintype.card n)) 𝕜 (EuclideanSpace 𝕜 n) := xs.reindex (Fintype.equivOfCardEq ⋯).symm
as' : Fin (Fintype.card n) → ℝ := fun i => as ((Fintype.equivOfCardEq ⋯) i)
hxs' : ∀ (j : Fin (Fintype.card n)), Module.End.HasEigenvector (toLin' A) (↑(as' j)) (xs' j)
⊢ i = (Fintype.equivOfCardEq ⋯) ((Fintype.equivOfCardEq ⋯).symm i)
Tactic:
simp
State after:
no goals