awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
j : n
⊢ A *ᵥ ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j) =
    HSMul.hSMul (β := (i : n) → (fun (x : n) ↦ 𝕜) i) (hA.eigenvalues j)
      (ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j))

Tactic:
simpa only [eigenvectorBasis, OrthonormalBasis.reindex_apply, toLpLin_apply,
    RCLike.real_smul_eq_coe_smul (K := 𝕜)] using
      congr(⇑$((isSymmetric_toEuclideanLin_iff.mpr hA).apply_eigenvectorBasis
        finrank_euclideanSpace ((Fintype.equivOfCardEq (Fintype.card_fin _)).symm j)))

Premises used: Iff.mpr, Fintype.card_fin, Matrix.isSymmetric_toEuclideanLin_iff, RCLike.real_smul_eq_coe_smul, OrthonormalBasis.reindex_apply, finrank_euclideanSpace, Matrix.IsHermitian.eigenvectorBasis, LinearMap.IsSymmetric.apply_eigenvectorBasis, Equiv.symm, Matrix.toLpLin_apply, DFunLike.coe, Fintype.equivOfCardEq
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
i : n
apply : Membership.mem (α := 𝕜) (spectrum 𝕜 A) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (hA.eigenvalues i) : 𝕜)
⊢ hA.eigenvalues i ∈ spectrum ℝ A

Tactic:
apply spectrum.of_algebraMap_mem 𝕜

Premises used: spectrum.of_algebraMap_mem
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
i : n
rw :
  Membership.mem (α := 𝕜)
    (spectrum 𝕜 (A := WithLp 2 (n → 𝕜) →ₗ[𝕜] WithLp 2 (n → 𝕜))
      ((toLpLin 2 2 : (a : Matrix n n 𝕜) → WithLp 2 (n → 𝕜) →ₗ[𝕜] WithLp 2 (n → 𝕜)) A :
        WithLp 2 (n → 𝕜) →ₗ[𝕜] WithLp 2 (n → 𝕜)))
    ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (hA.eigenvalues i) : 𝕜)
⊢ Membership.mem (α := 𝕜) (spectrum 𝕜 A) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (hA.eigenvalues i) : 𝕜)

Tactic:
rw [← Matrix.spectrum_toLpLin 2]

Premises used: Matrix.spectrum_toLpLin, OfNat.ofNat
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
i : n
⊢ Membership.mem (α := 𝕜)
    (spectrum 𝕜 (A := WithLp 2 (n → 𝕜) →ₗ[𝕜] WithLp 2 (n → 𝕜))
      ((toLpLin 2 2 : (a : Matrix n n 𝕜) → WithLp 2 (n → 𝕜) →ₗ[𝕜] WithLp 2 (n → 𝕜)) A :
        WithLp 2 (n → 𝕜) →ₗ[𝕜] WithLp 2 (n → 𝕜)))
    ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (hA.eigenvalues i) : 𝕜)

Tactic:
LinearMap.IsSymmetric.hasEigenvalue_eigenvalues _ _ _ |>.mem_spectrum

Premises used: Module.End.HasEigenvalue.mem_spectrum, Matrix.IsHermitian.eigenvalues₀, Set.Mem, LinearMap.IsSymmetric.hasEigenvalue_eigenvalues, Matrix.IsHermitian.eigenvalues
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
i : n
⊢ Membership.mem (α := 𝕜)
    (spectrum 𝕜 (A := WithLp 2 (n → 𝕜) →ₗ[𝕜] WithLp 2 (n → 𝕜))
      ((toLpLin 2 2 : (a : Matrix n n 𝕜) → WithLp 2 (n → 𝕜) →ₗ[𝕜] WithLp 2 (n → 𝕜)) A :
        WithLp 2 (n → 𝕜) →ₗ[𝕜] WithLp 2 (n → 𝕜)))
    ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (hA.eigenvalues i) : 𝕜)

Tactic:
exact LinearMap.IsSymmetric.hasEigenvalue_eigenvalues _ _ _ |>.mem_spectrum

Premises used: Module.End.HasEigenvalue.mem_spectrum, LinearMap.IsSymmetric.hasEigenvalue_eigenvalues
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
n : Type u_4
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
    Module.Basis.toMatrix (OrthonormalBasis.toBasis (EuclideanSpace.basisFun n 𝕜))
      (⇑(OrthonormalBasis.toBasis hA.eigenvectorBasis) : (a : n) → EuclideanSpace 𝕜 n)

Tactic:
rfl

Premises used: Module.Basis.toMatrix, rfl
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
j : n
⊢ (↑hA.eigenvectorUnitary : Matrix n n 𝕜)ᵀ j = ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j)

Tactic:
rfl

Premises used: Function.update, Module.Basis.toMatrix, Pi.single, dite, Matrix.transpose, rfl
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
j : n
⊢ (↑hA.eigenvectorUnitary : Matrix n n 𝕜).col j = ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j)

Tactic:
rfl

Premises used: Function.update, Module.Basis.toMatrix, Pi.single, dite, Matrix.transpose, Matrix.col, rfl
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
i j : n
⊢ (↑hA.eigenvectorUnitary : Matrix n n 𝕜) i j = ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j) i

Tactic:
rfl

Premises used: Function.update, Module.Basis.toMatrix, Pi.single, dite, rfl
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
j : n
simp_rw simp_rw₁ :
  (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ Pi.single (M := fun (a : n) ↦ 𝕜) j 1 =
    ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j)
simp_rw₂ :
  (↑hA.eigenvectorUnitary : Matrix n n 𝕜).col j = ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j)
⊢ (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ Pi.single (M := fun (a : n) ↦ 𝕜) j 1 =
    ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j)

Tactic:
simp_rw [mulVec_single_one, eigenvectorUnitary_col_eq]

Premises used: Matrix.mulVec_single_one, Matrix.IsHermitian.eigenvectorUnitary_col_eq
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
j : n
rw :
  star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ
      (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ Pi.single (M := fun (a : n) ↦ 𝕜) j 1 =
    Pi.single (M := fun (j : n) ↦ 𝕜) j 1
rw₁ :
  (star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) * (↑hA.eigenvectorUnitary : Matrix n n 𝕜)) *ᵥ
      Pi.single (M := fun (a : n) ↦ 𝕜) j 1 =
    Pi.single (M := fun (j : n) ↦ 𝕜) j 1
rw₂ : Eq (α := n → 𝕜) (1 *ᵥ Pi.single (M := fun (a : n) ↦ 𝕜) j 1) (Pi.single (M := fun (j : n) ↦ 𝕜) j 1)
rw₃ rw₄ : Eq (α := n → 𝕜) (Pi.single (M := fun (a : n) ↦ 𝕜) j 1) (Pi.single (M := fun (j : n) ↦ 𝕜) j 1)
⊢ star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ
      ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j) =
    Pi.single (M := fun (j : n) ↦ 𝕜) j 1

Tactic:
rw [← eigenvectorUnitary_mulVec, mulVec_mulVec, Unitary.coe_star_mul_self, one_mulVec]

Premises used: Matrix.IsHermitian.eigenvectorUnitary_mulVec, Unitary.coe_star_mul_self, Matrix.one_mulVec, Matrix.mulVec_mulVec
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← conjStarAlgAut_star_eigenvectorUnitary, ← conjStarAlgAut_mul_apply]

Premises used: Unitary.conjStarAlgAut_mul_apply, Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
i : n
rw :
  hA.eigenvalues i =
    (RCLike.re : (a : 𝕜) → ℝ)
      (A *ᵥ ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) i) ⬝ᵥ
        star (ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) i)))
⊢ hA.eigenvalues i =
    (RCLike.re : (a : 𝕜) → ℝ)
      (star (ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) i)) ⬝ᵥ
        A *ᵥ ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) i))

Tactic:
rw [dotProduct_comm]

Premises used: dotProduct_comm
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
i : n
⊢ hA.eigenvalues i =
    (RCLike.re : (a : 𝕜) → ℝ)
      (A *ᵥ ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) i) ⬝ᵥ
        star (ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) i)))

Tactic:
simp only [mulVec_eigenvectorBasis, smul_dotProduct, ← EuclideanSpace.inner_eq_star_dotProduct,
    inner_self_eq_norm_sq_to_K, RCLike.smul_re, hA.eigenvectorBasis.orthonormal.1 i,
    mul_one, algebraMap.coe_one, one_pow, RCLike.one_re]

Premises used: RCLike.one_re, one_pow, algebraMap.coe_one, RCLike.smul_re, inner_self_eq_norm_sq_to_K, Matrix.IsHermitian.eigenvectorBasis, EuclideanSpace.inner_eq_star_dotProduct, And.left, OrthonormalBasis.orthonormal, mul_one, Matrix.IsHermitian.mulVec_eigenvectorBasis, smul_dotProduct
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
rw :
  (star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) * (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
      diagonal (RCLike.ofReal ∘ hA.eigenvalues)).charpoly
| A.charpoly

Tactic:
rw [hA.spectral_theorem, conjStarAlgAut_apply, charpoly_mul_comm, ← mul_assoc]

Premises used: mul_assoc, Unitary.conjStarAlgAut_apply, Matrix.IsHermitian.spectral_theorem, Matrix.charpoly_mul_comm
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
conv_lhs :
  Eq (α := 𝕜[X])
    (star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) * (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
        diagonal (RCLike.ofReal ∘ hA.eigenvalues)).charpoly
    (∏ i : n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(hA.eigenvalues i) : 𝕜)))
⊢ Eq (α := 𝕜[X]) A.charpoly (∏ i : n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(hA.eigenvalues i) : 𝕜)))

Tactic:
conv_lhs => rw [hA.spectral_theorem, conjStarAlgAut_apply, charpoly_mul_comm, ← mul_assoc]

Premises used: mul_assoc, Unitary.conjStarAlgAut_apply, Matrix.IsHermitian.spectral_theorem, Matrix.charpoly_mul_comm
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ Eq (α := 𝕜[X])
    (star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) * (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
        diagonal (RCLike.ofReal ∘ hA.eigenvalues)).charpoly
    (∏ i : n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(hA.eigenvalues i) : 𝕜)))

Tactic:
simp [charpoly_diagonal]

Premises used: Matrix.charpoly_diagonal
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
rw :
  Eq.{u_1 + 1} (α := Multiset 𝕜)
    (Multiset.bind (Finset.val Finset.univ) fun (i : n) ↦
      (HSub.hSub (α := Polynomial 𝕜) Polynomial.X
          ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hA.eigenvalues i) : 𝕜))).roots)
    (Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) (Finset.val Finset.univ))
a :
  Ne.{u_1 + 1} (α := Polynomial 𝕜)
    (∏ i : n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hA.eigenvalues i) : 𝕜)))
    0
⊢ Polynomial.roots A.charpoly = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) (Finset.val Finset.univ)

Tactic:
rw [hA.charpoly_eq, Polynomial.roots_prod]

Premises used: Polynomial.roots_prod, Matrix.IsHermitian.charpoly_eq
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ Eq.{u_1 + 1} (α := Multiset 𝕜)
    (Multiset.bind (Finset.val Finset.univ) fun (i : n) ↦
      (HSub.hSub (α := Polynomial 𝕜) Polynomial.X
          ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hA.eigenvalues i) : 𝕜))).roots)
    (Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) (Finset.val Finset.univ))

Tactic:
simp
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ Ne.{u_1 + 1} (α := Polynomial 𝕜)
    (∏ i : n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hA.eigenvalues i) : 𝕜)))
    0

Tactic:
simp [Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero]

Premises used: Finset.prod_ne_zero_iff, Polynomial.X_sub_C_ne_zero
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
rw :
  Eq.{u_1 + 1} (α := Multiset 𝕜) (Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) (Finset.val Finset.univ))
    (Multiset.map (α := Fin (Fintype.card n)) (RCLike.ofReal ∘ hA.eigenvalues₀) (Finset.val Finset.univ))
⊢ Polynomial.roots A.charpoly =
    Multiset.map (α := Fin (Fintype.card n)) (RCLike.ofReal ∘ hA.eigenvalues₀) (Finset.val Finset.univ)

Tactic:
rw [hA.roots_charpoly_eq_eigenvalues]

Premises used: Matrix.IsHermitian.roots_charpoly_eq_eigenvalues
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
simp :
  Eq.{u_1 + 1} (α := Multiset 𝕜)
    (Multiset.map (fun (x : ℝ) ↦ (↑x : 𝕜))
      (Multiset.map (α := Fin (Fintype.card n)) hA.eigenvalues₀
        (Multiset.map.{0, u_2} (α := n) (⇑(Equiv.symm (Fintype.equivOfCardEq ⋯)) : (a : n) → Fin (Fintype.card n))
          (Finset.val Finset.univ))))
    (Multiset.map RCLike.ofReal (Multiset.map (α := Fin (Fintype.card n)) hA.eigenvalues₀ (Finset.val Finset.univ)))
⊢ Eq.{u_1 + 1} (α := Multiset 𝕜) (Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) (Finset.val Finset.univ))
    (Multiset.map (α := Fin (Fintype.card n)) (RCLike.ofReal ∘ hA.eigenvalues₀) (Finset.val Finset.univ))

Tactic:
simp only [← Multiset.map_map, eigenvalues, ← Function.comp_apply (f := hA.eigenvalues₀)]

Premises used: Matrix.IsHermitian.eigenvalues, Multiset.map_map, Function.comp_apply
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ Eq.{u_1 + 1} (α := Multiset 𝕜)
    (Multiset.map (fun (x : ℝ) ↦ (↑x : 𝕜))
      (Multiset.map (α := Fin (Fintype.card n)) hA.eigenvalues₀
        (Multiset.map.{0, u_2} (α := n) (⇑(Equiv.symm (Fintype.equivOfCardEq ⋯)) : (a : n) → Fin (Fintype.card n))
          (Finset.val Finset.univ))))
    (Multiset.map RCLike.ofReal (Multiset.map (α := Fin (Fintype.card n)) hA.eigenvalues₀ (Finset.val Finset.univ)))

Tactic:
simp
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
simp_rw :
  (List.mergeSort (List.ofFn (n := Fintype.card n) fun (x : Fin (Fintype.card n)) ↦ hA.eigenvalues₀ x) fun (x1 x2 : ℝ) ↦
      decide (x1 ≥ x2)) =
    List.ofFn (n := Fintype.card n) hA.eigenvalues₀
⊢ (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) (Polynomial.roots A.charpoly)) fun (x1 x2 : ℝ) ↦ x1 ≥ x2) =
    List.ofFn (n := Fintype.card n) hA.eigenvalues₀

Tactic:
simp_rw [hA.roots_charpoly_eq_eigenvalues₀, Fin.univ_val_map, Multiset.map_coe, List.map_ofFn,
    Function.comp_def, RCLike.ofReal_re, Multiset.coe_sort]

Premises used: RCLike.ofReal_re, List.map_ofFn, Function.comp_def, Multiset.coe_sort, Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀, Multiset.map_coe, Fin.univ_val_map
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x :
  List.Pairwise (fun (a b : ℝ) ↦ decide (a ≥ b) = true)
    (List.ofFn (n := Fintype.card n) fun (x : Fin (Fintype.card n)) ↦ hA.eigenvalues₀ x)
⊢ (List.mergeSort (List.ofFn (n := Fintype.card n) fun (x : Fin (Fintype.card n)) ↦ hA.eigenvalues₀ x) fun (x1 x2 : ℝ) ↦
      decide (x1 ≥ x2)) =
    List.ofFn (n := Fintype.card n) hA.eigenvalues₀

Tactic:
apply List.mergeSort_of_pairwise

Premises used: List.mergeSort_of_pairwise
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
x : List.SortedGE (α := ℝ) (List.ofFn (n := Fintype.card n) fun (x : Fin (Fintype.card n)) ↦ hA.eigenvalues₀ x)
⊢ List.Pairwise (fun (a b : ℝ) ↦ decide (a ≥ b) = true)
    (List.ofFn (n := Fintype.card n) fun (x : Fin (Fintype.card n)) ↦ hA.eigenvalues₀ x)

Tactic:
simp_rw [decide_eq_true_eq, ← List.sortedGE_iff_pairwise]

Premises used: List.sortedGE_iff_pairwise, decide_eq_true_eq
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ List.SortedGE (α := ℝ) (List.ofFn (n := Fintype.card n) fun (x : Fin (Fintype.card n)) ↦ hA.eigenvalues₀ x)

Tactic:
(eigenvalues₀_antitone hA).sortedGE_ofFn

Premises used: Antitone.sortedGE_ofFn, Matrix.IsHermitian.eigenvalues₀_antitone
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ List.SortedGE (α := ℝ) (List.ofFn (n := Fintype.card n) fun (x : Fin (Fintype.card n)) ↦ hA.eigenvalues₀ x)

Tactic:
exact (eigenvalues₀_antitone hA).sortedGE_ofFn

Premises used: Antitone.sortedGE_ofFn, Matrix.IsHermitian.eigenvalues₀_antitone
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A B : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
mp : hA.eigenvalues = hB.eigenvalues → Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
mpr : Eq (α := Polynomial 𝕜) A.charpoly B.charpoly → hA.eigenvalues = hB.eigenvalues
⊢ hA.eigenvalues = hB.eigenvalues ↔ Eq (α := Polynomial 𝕜) A.charpoly B.charpoly

Tactic:
constructor
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A B : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : hA.eigenvalues = hB.eigenvalues
mp :
  Eq (α := Polynomial 𝕜)
    (∏ i : n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hA.eigenvalues i) : 𝕜)))
    B.charpoly
mp₁ :
  Eq.{u_1 + 1} (α := Polynomial 𝕜)
    (∏ i : n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hA.eigenvalues i) : 𝕜)))
    (∏ i : n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hB.eigenvalues i) : 𝕜)))
mp₂ mp₃ :
  Eq.{u_1 + 1} (α := Polynomial 𝕜)
    (∏ i : n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hB.eigenvalues i) : 𝕜)))
    (∏ i : n,
      HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hB.eigenvalues i) : 𝕜)))
⊢ Eq (α := Polynomial 𝕜) A.charpoly B.charpoly

Tactic:
rw [hA.charpoly_eq, hB.charpoly_eq, h]

Premises used: Matrix.IsHermitian.charpoly_eq
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A B : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
this : Eq (α := Fin (Fintype.card n) → ℝ) hA.eigenvalues₀ hB.eigenvalues₀
rw rw₁ :
  Eq.{u_2 + 1} (α := n → ℝ)
    (fun (i : n) ↦
      hB.eigenvalues₀
        (((Equiv.symm (Fintype.equivOfCardEq ⋯) : n ≃ Fin (Fintype.card n)) : (a : n) → Fin (Fintype.card n)) i))
    fun (i : n) ↦
    hB.eigenvalues₀
      (((Equiv.symm (Fintype.equivOfCardEq ⋯) : n ≃ Fin (Fintype.card n)) : (a : n) → Fin (Fintype.card n)) i)
⊢ Eq.{u_2 + 1} (α := n → ℝ)
    (fun (i : n) ↦
      hA.eigenvalues₀
        (((Equiv.symm (Fintype.equivOfCardEq ⋯) : n ≃ Fin (Fintype.card n)) : (a : n) → Fin (Fintype.card n)) i))
    fun (i : n) ↦
    hB.eigenvalues₀
      (((Equiv.symm (Fintype.equivOfCardEq ⋯) : n ≃ Fin (Fintype.card n)) : (a : n) → Fin (Fintype.card n)) i)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A B : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
mpr : Eq (α := Fin (Fintype.card n) → ℝ) hA.eigenvalues₀ hB.eigenvalues₀
⊢ hA.eigenvalues = hB.eigenvalues

Tactic:
suffices hA.eigenvalues₀ = hB.eigenvalues₀ by unfold eigenvalues; rw [this]
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A B : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
hB : B.IsHermitian
h : Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
mpr : List.ofFn (n := Fintype.card n) hA.eigenvalues₀ = List.ofFn (n := Fintype.card n) hB.eigenvalues₀
mpr₁ :
  Eq (α := List ℝ)
    (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) (Polynomial.roots A.charpoly)) fun (x1 x2 : ℝ) ↦ x1 ≥ x2)
    (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) (Polynomial.roots B.charpoly)) fun (x1 x2 : ℝ) ↦ x1 ≥ x2)
⊢ Eq (α := Fin (Fintype.card n) → ℝ) hA.eigenvalues₀ hB.eigenvalues₀

Tactic:
simp_rw [← List.ofFn_inj, ← sort_roots_charpoly_eq_eigenvalues₀, h]

Premises used: Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀, List.ofFn_inj
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ (Polynomial.roots A.charpoly).card = Polynomial.natDegree A.charpoly

Tactic:
simp [hA.roots_charpoly_eq_eigenvalues]

Premises used: Matrix.IsHermitian.roots_charpoly_eq_eigenvalues
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
⊢ A.det = ∏ i : n, (↑(hA.eigenvalues i) : 𝕜)

Tactic:
simp [det_eq_prod_roots_charpoly_of_splits hA.splits_charpoly, hA.roots_charpoly_eq_eigenvalues]

Premises used: Matrix.det_eq_prod_roots_charpoly_of_splits, Matrix.IsHermitian.roots_charpoly_eq_eigenvalues, Matrix.IsHermitian.splits_charpoly
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
rw :
  ((↑hA.eigenvectorUnitary : Matrix n n 𝕜) * diagonal (RCLike.ofReal ∘ hA.eigenvalues) *
      (↑(star hA.eigenvectorUnitary) : Matrix n n 𝕜)).rank
| A.rank

Tactic:
rw [hA.spectral_theorem, conjStarAlgAut_apply, ← coe_star]

Premises used: Unitary.conjStarAlgAut_apply, Matrix.IsHermitian.spectral_theorem, Unitary.coe_star
-- Module: Mathlib.Analysis.Matrix.Spectrum
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
hA : A.IsHermitian
conv_lhs :
  ((↑hA.eigenvectorUnitary : Matrix n n 𝕜) * diagonal (RCLike.ofReal ∘ hA.eigenvalues) *
        (↑(star hA.eigenvectorUnitary) : Matrix n n 𝕜)).rank =
    (diagonal hA.eigenvalues).rank
⊢ A.rank = (diagonal hA.eigenvalues).rank

Tactic:
conv_lhs => rw [hA.spectral_theorem, conjStarAlgAut_apply, ← coe_star]

Premises used: Unitary.conjStarAlgAut_apply, Matrix.IsHermitian.spectral_theorem, Unitary.coe_star