awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star y ⬝ᵥ M *ᵥ x) = M *ᵥ y ⬝ᵥ star x
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₂ : star (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (M *ᵥ x ⬝ᵥ star y) = M *ᵥ y ⬝ᵥ star x
have rw₃ : star (M *ᵥ x) ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
Tactic: rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
      star_mulVec, dotProduct_comm (M *ᵥ y), dotProduct_mulVec, hM.isHermitian.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star y ⬝ᵥ M *ᵥ x) = M *ᵥ y ⬝ᵥ star x
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₂ : star (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₃ : star (M *ᵥ x) ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (M *ᵥ x ⬝ᵥ star y) = M *ᵥ y ⬝ᵥ star x
have rw₄ : star x ᵥ* Mᴴ ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
Tactic: rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
      star_mulVec, dotProduct_comm (M *ᵥ y), dotProduct_mulVec, hM.isHermitian.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star y ⬝ᵥ M *ᵥ x) = M *ᵥ y ⬝ᵥ star x
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₂ : star (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₃ : star (M *ᵥ x) ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
rw₄ : star x ᵥ* Mᴴ ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (M *ᵥ x ⬝ᵥ star y) = M *ᵥ y ⬝ᵥ star x
have rw₅ : star x ᵥ* Mᴴ ⬝ᵥ y = star x ⬝ᵥ M *ᵥ y
Tactic: rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
      star_mulVec, dotProduct_comm (M *ᵥ y), dotProduct_mulVec, hM.isHermitian.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star y ⬝ᵥ M *ᵥ x) = M *ᵥ y ⬝ᵥ star x
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₂ : star (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₃ : star (M *ᵥ x) ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
rw₄ : star x ᵥ* Mᴴ ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
rw₅ : star x ᵥ* Mᴴ ⬝ᵥ y = star x ⬝ᵥ M *ᵥ y
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (M *ᵥ x ⬝ᵥ star y) = M *ᵥ y ⬝ᵥ star x
have rw₆ : star x ᵥ* Mᴴ ⬝ᵥ y = star x ᵥ* M ⬝ᵥ y
Tactic: rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
      star_mulVec, dotProduct_comm (M *ᵥ y), dotProduct_mulVec, hM.isHermitian.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x y : n → 𝕜
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star y ⬝ᵥ M *ᵥ x) = M *ᵥ y ⬝ᵥ star x
rw₁ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₂ : star (star (star (M *ᵥ x) ⬝ᵥ y)) = M *ᵥ y ⬝ᵥ star x
rw₃ : star (M *ᵥ x) ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
rw₄ : star x ᵥ* Mᴴ ⬝ᵥ y = M *ᵥ y ⬝ᵥ star x
rw₅ : star x ᵥ* Mᴴ ⬝ᵥ y = star x ⬝ᵥ M *ᵥ y
rw₆ : star x ᵥ* Mᴴ ⬝ᵥ y = star x ᵥ* M ⬝ᵥ y
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (M *ᵥ x ⬝ᵥ star y) = M *ᵥ y ⬝ᵥ star x
have rw₇ : star x ᵥ* M ⬝ᵥ y = star x ᵥ* M ⬝ᵥ y
Tactic: rw [dotProduct_comm, star_dotProduct, starRingEnd_apply, star_star,
      star_mulVec, dotProduct_comm (M *ᵥ y), dotProduct_mulVec, hM.isHermitian.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x x_1 : n → 𝕜
x_2 : 𝕜
⊢ M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)
have rw : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)
Tactic: rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x x_1 : n → 𝕜
x_2 : 𝕜
rw : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)
⊢ M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)
have rw₁ : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = M *ᵥ x_1 ⬝ᵥ HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (star x)
Tactic: rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x x_1 : n → 𝕜
x_2 : 𝕜
rw : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)
rw₁ : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = M *ᵥ x_1 ⬝ᵥ HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (star x)
⊢ M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)
have rw₂ : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = M *ᵥ x_1 ⬝ᵥ star x_2 • star x
Tactic: rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosSemidef
x x_1 : n → 𝕜
x_2 : 𝕜
rw : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)
rw₁ : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = M *ᵥ x_1 ⬝ᵥ HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (star x)
rw₂ : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = M *ᵥ x_1 ⬝ᵥ star x_2 • star x
⊢ M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) x_2 : 𝕜) (M *ᵥ x_1 ⬝ᵥ star x)
have rw₃ : M *ᵥ x_1 ⬝ᵥ star (x_2 • x) = M *ᵥ x_1 ⬝ᵥ star (x_2 • x)
Tactic: rw [← smul_eq_mul, ← dotProduct_smul, starRingEnd_apply, ← star_smul]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.PosDef (goal)
Goal:
m : Type u_1
n : Type u_2
𝕜 : Type u_3
inst : Fintype m
inst_1 : Fintype n
inst_2 : RCLike 𝕜
A M : Matrix n n 𝕜
hM : M.PosDef
x : n → 𝕜
hx : M *ᵥ x ⬝ᵥ star x = 0
⊢ x = 0
have by_contra! : ∀ (h : x ≠ 0), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
n : Type u_2
inst_1 : Fintype n
A : Matrix n n 𝕜
inst_2 : DecidableEq n
⊢ (spectrum ℝ A).Finite
have rw : Set.Finite (α := ℝ) ((⇑(algebraMap ℝ 𝕜) : (a : ℝ) → 𝕜) ⁻¹' spectrum 𝕜 A)
Tactic: rw [← spectrum.preimage_algebraMap 𝕜]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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 ∈ spectrum ℝ A
have apply : Membership.mem (α := 𝕜) (spectrum 𝕜 A) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (hA.eigenvalues i) : 𝕜)
Tactic: apply spectrum.of_algebraMap_mem 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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) ((algebraMap ℝ 𝕜 : (a : ℝ) → 𝕜) (hA.eigenvalues i) : 𝕜)
have 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) : 𝕜)
Tactic: rw [← Matrix.spectrum_toLpLin 2]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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)
⊢ (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ Pi.single (M := fun (a : n) ↦ 𝕜) j 1 =
    ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j)
have simp_rw₂ : (↑hA.eigenvectorUnitary : Matrix n n 𝕜).col j = ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j)
Tactic: simp_rw [mulVec_single_one, eigenvectorUnitary_col_eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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
⊢ star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ
      ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j) =
    Pi.single (M := fun (j : n) ↦ 𝕜) j 1
have 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
Tactic: rw [← eigenvectorUnitary_mulVec, mulVec_mulVec, Unitary.coe_star_mul_self, one_mulVec]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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
⊢ star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ
      ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j) =
    Pi.single (M := fun (j : n) ↦ 𝕜) j 1
have 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
Tactic: rw [← eigenvectorUnitary_mulVec, mulVec_mulVec, Unitary.coe_star_mul_self, one_mulVec]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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
⊢ star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ
      ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j) =
    Pi.single (M := fun (j : n) ↦ 𝕜) j 1
have rw₂ : Eq (α := n → 𝕜) (1 *ᵥ Pi.single (M := fun (a : n) ↦ 𝕜) j 1) (Pi.single (M := fun (j : n) ↦ 𝕜) j 1)
Tactic: rw [← eigenvectorUnitary_mulVec, mulVec_mulVec, Unitary.coe_star_mul_self, one_mulVec]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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)
⊢ star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *ᵥ
      ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) j) =
    Pi.single (M := fun (j : n) ↦ 𝕜) j 1
have rw₃ : Eq (α := n → 𝕜) (Pi.single (M := fun (a : n) ↦ 𝕜) j 1) (Pi.single (M := fun (j : n) ↦ 𝕜) j 1)
Tactic: rw [← eigenvectorUnitary_mulVec, mulVec_mulVec, Unitary.coe_star_mul_self, one_mulVec]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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)
have rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: rw [← conjStarAlgAut_star_eigenvectorUnitary, ← conjStarAlgAut_mul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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 : 𝕜) → ℝ)
      (star (ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) i)) ⬝ᵥ
        A *ᵥ ofLp (p := 2) ((hA.eigenvectorBasis : (a : n) → EuclideanSpace 𝕜 n) i))
have 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)))
Tactic: rw [dotProduct_comm]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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.charpoly
have rw : (star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) * (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
    diagonal (RCLike.ofReal ∘ hA.eigenvalues)).charpoly
Tactic: rw [hA.spectral_theorem, conjStarAlgAut_apply, charpoly_mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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]) A.charpoly (∏ i : n, HSub.hSub (α := 𝕜[X]) X ((C : (a : 𝕜) → 𝕜[X]) (↑(hA.eigenvalues i) : 𝕜)))
have 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) : 𝕜)))
Tactic: conv_lhs => rw [hA.spectral_theorem, conjStarAlgAut_apply, charpoly_mul_comm, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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 = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) (Finset.val Finset.univ)
have 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))
Tactic: rw [hA.charpoly_eq, Polynomial.roots_prod]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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))
⊢ Polynomial.roots A.charpoly = Multiset.map (RCLike.ofReal ∘ hA.eigenvalues) (Finset.val Finset.univ)
have a : Ne.{u_1 + 1} (α := Polynomial 𝕜)
  (∏ i : n,
    HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hA.eigenvalues i) : 𝕜)))
  0
Tactic: rw [hA.charpoly_eq, Polynomial.roots_prod]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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 =
    Multiset.map (α := Fin (Fintype.card n)) (RCLike.ofReal ∘ hA.eigenvalues₀) (Finset.val Finset.univ)
have 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))
Tactic: rw [hA.roots_charpoly_eq_eigenvalues]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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 (RCLike.ofReal ∘ hA.eigenvalues) (Finset.val Finset.univ))
    (Multiset.map (α := Fin (Fintype.card n)) (RCLike.ofReal ∘ hA.eigenvalues₀) (Finset.val Finset.univ))
have 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 sorry)) : (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 only [← Multiset.map_map, eigenvalues, ← Function.comp_apply (f := hA.eigenvalues₀)]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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
⊢ (Multiset.sort (Multiset.map (⇑RCLike.re : (a : 𝕜) → ℝ) (Polynomial.roots A.charpoly)) fun (x1 x2 : ℝ) ↦ x1 ≥ x2) =
    List.ofFn (n := Fintype.card n) hA.eigenvalues₀
have 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₀
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]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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.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₀
have 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: apply List.mergeSort_of_pairwise
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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.Pairwise (fun (a b : ℝ) ↦ decide (a ≥ b) = true)
    (List.ofFn (n := Fintype.card n) fun (x : Fin (Fintype.card n)) ↦ hA.eigenvalues₀ x)
have x : List.SortedGE (α := ℝ) (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]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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
⊢ hA.eigenvalues = hB.eigenvalues ↔ Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
have mp : hA.eigenvalues = hB.eigenvalues → Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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
⊢ hA.eigenvalues = hB.eigenvalues ↔ Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
have mpr : Eq (α := Polynomial 𝕜) A.charpoly B.charpoly → hA.eigenvalues = hB.eigenvalues
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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
⊢ Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
have mp : Eq (α := Polynomial 𝕜)
  (∏ i : n,
    HSub.hSub (α := Polynomial 𝕜) Polynomial.X ((Polynomial.C : (a : 𝕜) → Polynomial 𝕜) (↑(hA.eigenvalues i) : 𝕜)))
  B.charpoly
Tactic: rw [hA.charpoly_eq, hB.charpoly_eq, h]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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
⊢ Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
have 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) : 𝕜)))
Tactic: rw [hA.charpoly_eq, hB.charpoly_eq, h]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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) : 𝕜)))
⊢ Eq (α := Polynomial 𝕜) A.charpoly B.charpoly
have 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) : 𝕜)))
Tactic: rw [hA.charpoly_eq, hB.charpoly_eq, h]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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₀
⊢ 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)
have rw : Eq.{u_2 + 1} (α := n → ℝ)
  (fun (i : n) ↦
    hB.eigenvalues₀
      (((Equiv.symm (Fintype.equivOfCardEq sorry) : n ≃ Fin (Fintype.card n)) : (a : n) → Fin (Fintype.card n)) i))
  fun (i : n) ↦
  hB.eigenvalues₀
    (((Equiv.symm (Fintype.equivOfCardEq sorry) : n ≃ Fin (Fintype.card n)) : (a : n) → Fin (Fintype.card n)) i)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Spectrum (goal)
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
⊢ hA.eigenvalues = hB.eigenvalues
have mpr : Eq (α := Fin (Fintype.card n) → ℝ) hA.eigenvalues₀ hB.eigenvalues₀
Tactic: suffices hA.eigenvalues₀ = hB.eigenvalues₀ by unfold eigenvalues; rw [this]