awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  Eq (α := M)
    ((HSub.hSub (α := End R M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
              (HSMul.hSMul (β := End R M) μ 1) ^
            k :
          (a : M) → M)
        x :
      M)
    (0 : M)
j : n
⊢ HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
      (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
    (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d - diagonal (HSMul.hSMul (β := n → R) μ 1))

Tactic:
simp [one_eq_id]

Premises used: Module.End.one_eq_id
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  Eq (α := M)
    ((HSub.hSub (α := End R M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
              (HSMul.hSMul (β := End R M) μ 1) ^
            k :
          (a : M) → M)
        x :
      M)
    (0 : M)
j : n
⊢ HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
      (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
    (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal (d - HSMul.hSMul (β := n → R) μ 1))

Tactic:
have aux : (diagonal d).toLin b b - μ • 1 = (diagonal (d - μ • 1)).toLin b b := by
      rw [Pi.sub_def, ← diagonal_sub]; simp [one_eq_id]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  Eq (α := M)
    ((HSub.hSub (α := End R M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
              (HSMul.hSMul (β := End R M) μ 1) ^
            k :
          (a : M) → M)
        x :
      M)
    (0 : M)
j : n
aux :
  HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
      (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
    (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal (d - HSMul.hSMul (β := n → R) μ 1))
rw :
  ∀
    (hk :
      ∀ (j : n),
        (diagonal ((d - HSMul.hSMul (β := n → R) μ 1) ^ k) *ᵥ (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R))
            j =
          0)
    (j : n)
    (aux :
      HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
          (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
        (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal (d - HSMul.hSMul (β := n → R) μ 1))),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
⊢ Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0

Tactic:
rw [aux, ← toLin_pow, diagonal_pow, toLin_apply_eq_zero_iff] at hk

Premises used: Matrix.diagonal_pow, Matrix.toLin_pow, Matrix.toLin_apply_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    (diagonal ((d - HSMul.hSMul (β := n → R) μ 1) ^ k) *ᵥ (⇑((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R)) j =
      0
j : n
aux :
  HSub.hSub (α := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
      (HSMul.hSMul (β := M →ₗ[R] M) μ 1) =
    (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal (d - HSMul.hSMul (β := n → R) μ 1))
⊢ Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0

Tactic:
simpa [mulVec_eq_sum, diagonal_apply, sub_eq_zero] using hk j

Premises used: sub_eq_zero, Matrix.mulVec_eq_sum, Matrix.diagonal_apply
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  Eq (α := M)
    ((HSub.hSub (α := End R M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M)
              (HSMul.hSMul (β := End R M) μ 1) ^
            k :
          (a : M) → M)
        x :
      M)
    (0 : M)
⊢ ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0

Tactic:
replace hk (j : n) : b.repr x j = 0 ∨ d j = μ ∧ k ≠ 0 := by
    have aux : (diagonal d).toLin b b - μ • 1 = (diagonal (d - μ • 1)).toLin b b := by
      rw [Pi.sub_def, ← diagonal_sub]; simp [one_eq_id]
    rw [aux, ← toLin_pow, diagonal_pow, toLin_apply_eq_zero_iff] at hk
    simpa [mulVec_eq_sum, diagonal_apply, sub_eq_zero] using hk j
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
j : n
inl :
  ∀ (hj : Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R)),
    HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
        ((b : (a : n) → M) j : M) =
      μ •
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
          ((b : (a : n) → M) j : M)
inr :
  ∀ (hj : d j = μ ∧ k ≠ 0),
    HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
        ((b : (a : n) → M) j : M) =
      μ •
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
          ((b : (a : n) → M) j : M)
⊢ HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)

Tactic:
rcases hk j with hj | hj
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
j : n
hj : Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R)
⊢ HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)

Tactic:
simp [hj]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
j : n
hj : d j = μ ∧ k ≠ 0
inr :
  HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    d j •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
inr₁ :
  HSMul.hSMul (β := M) (HMul.hMul (β := R) (d j) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R))
      ((b : (a : n) → M) j : M) =
    d j •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
inr₂ inr₃ :
  d j •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M) =
    d j •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)
⊢ HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
      ((b : (a : n) → M) j : M) =
    μ •
      HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
        ((b : (a : n) → M) j : M)

Tactic:
rw [← hj.1, mul_comm, mul_smul]

Premises used: And.left, mul_comm, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
⊢ ∀ (j : n),
    HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
        ((b : (a : n) → M) j : M) =
      μ •
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
          ((b : (a : n) → M) j : M)

Tactic:
have aux (j : n) : (b.repr x j * d j) • b j = μ • (b.repr x j • b j) := by
    rcases hk j with hj | hj
    · simp [hj]
    · rw [← hj.1, mul_comm, mul_smul]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
x : M
hx :
  Membership.mem (γ := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
k : ℕ
hk :
  ∀ (j : n),
    Eq.{u_1 + 1} (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (0 : R) ∨ d j = μ ∧ k ≠ 0
aux :
  ∀ (j : n),
    HSMul.hSMul (β := M) (HMul.hMul (α := R) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R) (d j))
        ((b : (a : n) → M) j : M) =
      μ •
        HSMul.hSMul.{u_1, u_3, u_3} (α := R) (β := M) ((((b.repr : (a : M) → n →₀ R) x : n →₀ R) : (a : n) → R) j : R)
          ((b : (a : n) → M) j : M)
⊢ Membership.mem (γ := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x

Tactic:
simp [toLin_apply, mulVec_eq_sum, diagonal_apply, aux, ← Finset.smul_sum]

Premises used: Matrix.toLin_apply, Matrix.mulVec_eq_sum, Matrix.diagonal_apply, Finset.smul_sum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
d : n → R
μ : R
inst_3 : IsDomain R
⊢ Eq (α := Submodule R (n → R))
    (maxGenEigenspace (M := n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal d)) μ :
      Submodule R (n → R))
    (eigenspace (M := n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal d)) μ : Submodule R (n → R))

Tactic:
maxGenEigenspace_toLin_diagonal_eq_eigenspace d <| Pi.basisFun R n

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Pi.basisFun, Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace, Matrix.mulVec, Finset.sum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
f : M →ₗ[R] M
b : Basis n R M
⊢ spectrum R (A := Matrix n n R) ((LinearMap.toMatrix b b : (a : M →ₗ[R] M) → Matrix n n R) f : Matrix n n R) =
    spectrum R f

Tactic:
AlgEquiv.spectrum_eq (LinearMap.toMatrixAlgEquiv b) f

Premises used: AlgEquiv.spectrum_eq, LinearMap.toMatrixAlgEquiv
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
f : (n → R) →ₗ[R] n → R
⊢ spectrum R (A := Matrix n n R) ((LinearMap.toMatrix' : (a : (n → R) →ₗ[R] n → R) → Matrix n n R) f : Matrix n n R) =
    spectrum R f

Tactic:
AlgEquiv.spectrum_eq LinearMap.toMatrixAlgEquiv' f

Premises used: LinearMap.toMatrixAlgEquiv', AlgEquiv.spectrum_eq
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
M : Type u_3
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
A : Matrix n n R
b : Basis n R M
⊢ spectrum.{u_1, u_3} R (A := M →ₗ[R] M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) A : M →ₗ[R] M) = spectrum R A

Tactic:
AlgEquiv.spectrum_eq (Matrix.toLinAlgEquiv b) A

Premises used: AlgEquiv.spectrum_eq, Matrix.toLinAlgEquiv
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : CommRing R
A : Matrix n n R
⊢ spectrum R (A := (n → R) →ₗ[R] n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) A : (n → R) →ₗ[R] n → R) =
    spectrum R A

Tactic:
AlgEquiv.spectrum_eq Matrix.toLinAlgEquiv' A

Premises used: AlgEquiv.spectrum_eq, Matrix.toLinAlgEquiv'
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Field R
d : n → R
h : ∀ (μ : R), μ ∈ spectrum R (diagonal d) ↔ μ ∈ Set.range d
⊢ spectrum R (diagonal d) = Set.range d

Tactic:
ext μ
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Field R
d : n → R
μ : R
h :
  HasEigenvalue (M := n → R) ((toLinAlgEquiv (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal d))
      μ ↔
    μ ∈ Set.range d
⊢ μ ∈ spectrum R (diagonal d) ↔ μ ∈ Set.range d

Tactic:
rw [← AlgEquiv.spectrum_eq (toLinAlgEquiv <| Pi.basisFun R n), ← hasEigenvalue_iff_mem_spectrum]

Premises used: AlgEquiv.spectrum_eq, Matrix.toLinAlgEquiv, Pi.basisFun, Module.End.hasEigenvalue_iff_mem_spectrum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Field R
d : n → R
μ : R
⊢ HasEigenvalue (M := n → R) ((toLinAlgEquiv (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal d))
      μ ↔
    μ ∈ Set.range d

Tactic:
hasEigenvalue_toLin'_diagonal_iff d

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Set.Mem, setOf, hasEigenvalue_toLin'_diagonal_iff, Set.range, Matrix.mulVec, Finset.sum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Matrix
Goal:
R : Type u_1
n : Type u_2
inst : DecidableEq n
inst_1 : Fintype n
inst_2 : Field R
d : n → R
μ : R
⊢ HasEigenvalue (M := n → R) ((toLinAlgEquiv (Pi.basisFun R n) : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal d))
      μ ↔
    μ ∈ Set.range d

Tactic:
exact hasEigenvalue_toLin'_diagonal_iff d

Premises used: hasEigenvalue_toLin'_diagonal_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : End R M
c : R[X]ˣ
m : M
hm : Eq (α := M) ((((aeval f : (a : R[X]) → End R M) (↑c : R[X]) : End R M) : (a : M) → M) m : M) (0 : M)
⊢ m = 0

Tactic:
simpa [← mul_apply, ← aeval_mul] using congr(c⁻¹.1.aeval f $hm)

Premises used: Polynomial.aeval_mul, Module.End.mul_apply
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x

Tactic:
p.induction_on ?_ ?_ ?_

Premises used: Polynomial.induction_on
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
refine_1 :
  ∀ (a : R),
    (((aeval f : (a : R[X]) → End R M) ((C : (a : R) → R[X]) a) : End R M) : (a : M) → M) x =
      eval μ ((C : (a : R) → R[X]) a) • x
refine_2 :
  ∀ (p q : R[X]),
    (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x →
      (((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) x = eval μ q • x →
        (((aeval f : (a : R[X]) → End R M) (p + q) : End R M) : (a : M) → M) x = eval μ (p + q) • x
refine_3 :
  ∀ (n : ℕ) (a : R),
    (((aeval f : (a : R[X]) → End R M)
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
              End R M) :
            (a : M) → M)
          x =
        eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x →
      (((aeval f : (a : R[X]) → End R M)
                (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
              End R M) :
            (a : M) → M)
          x =
        eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) • x
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x

Tactic:
refine p.induction_on ?_ ?_ ?_
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
a : R
⊢ (((aeval f : (a : R[X]) → End R M) ((C : (a : R) → R[X]) a) : End R M) : (a : M) → M) x =
    eval μ ((C : (a : R) → R[X]) a) • x

Tactic:
simp [Module.algebraMap_end_apply]

Premises used: Module.algebraMap_end_apply
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p_1 : R[X]
h : f.HasEigenvector μ x
p q : R[X]
hp : (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x
hq : (((aeval f : (a : R[X]) → End R M) q : End R M) : (a : M) → M) x = eval μ q • x
⊢ (((aeval f : (a : R[X]) → End R M) (p + q) : End R M) : (a : M) → M) x = eval μ (p + q) • x

Tactic:
simp [hp, hq, add_smul]

Premises used: add_smul
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
n : ℕ
a : R
hna :
  (((aeval f : (a : R[X]) → End R M)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
          End R M) :
        (a : M) → M)
      x =
    eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x
refine_3 :
  (((aeval f : (a : R[X]) → End R M) X : End R M) : (a : M) → M)
      (eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x) =
    eval μ (X * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x
⊢ (((aeval f : (a : R[X]) → End R M)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
          End R M) :
        (a : M) → M)
      x =
    eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) • x

Tactic:
rw [mul_comm, pow_succ', mul_assoc, map_mul, Module.End.mul_apply, mul_comm, hna]

Premises used: mul_assoc, map_mul, mul_comm, Module.End.mul_apply, pow_succ'
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
h : f.HasEigenvector μ x
n : ℕ
a : R
hna :
  (((aeval f : (a : R[X]) → End R M)
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) :
          End R M) :
        (a : M) → M)
      x =
    eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x
⊢ (((aeval f : (a : R[X]) → End R M) X : End R M) : (a : M) → M)
      (eval μ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x) =
    eval μ (X * HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)) • x

Tactic:
simp only [mem_eigenspace_iff.1 h.1, smul_smul, aeval_X, eval_mul, eval_C, eval_pow, eval_X,
      map_smulₛₗ, RingHom.id_apply, mul_comm]

Premises used: RingHom.id_apply, Polynomial.eval_C, Polynomial.eval_X, Polynomial.eval_pow, smul_smul, MulActionSemiHomClass.map_smulₛₗ, Polynomial.eval_mul, Module.End.mem_eigenspace_iff, And.left, Iff.mp, mul_comm, Polynomial.aeval_X
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
hx : (f : (a : M) → M) x = μ • x
inl :
  ∀ (hx : (f : (a : M) → M) 0 = HSMul.hSMul (β := M) μ 0),
    (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) 0 = HSMul.hSMul (β := M) (eval μ p) 0
inr : ∀ (hne : x ≠ 0), (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x

Tactic:
rcases eq_or_ne x 0 with rfl | hne

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
p : R[X]
hx : (f : (a : M) → M) 0 = HSMul.hSMul (β := M) μ 0
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) 0 = HSMul.hSMul (β := M) (eval μ p) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
hx : (f : (a : M) → M) x = μ • x
hne : x ≠ 0
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x

Tactic:
aeval_apply_of_hasEigenvector ⟨mem_eigenspace_iff.mpr hx, hne⟩

Premises used: Iff.mpr, Module.End.aeval_apply_of_hasEigenvector, Module.End.mem_eigenspace_iff, And.intro
-- Module: Mathlib.LinearAlgebra.Eigenspace.Minpoly
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
p : R[X]
hx : (f : (a : M) → M) x = μ • x
hne : x ≠ 0
⊢ (((aeval f : (a : R[X]) → End R M) p : End R M) : (a : M) → M) x = eval μ p • x

Tactic:
exact aeval_apply_of_hasEigenvector ⟨mem_eigenspace_iff.mpr hx, hne⟩

Premises used: Iff.mpr, Module.End.aeval_apply_of_hasEigenvector, Module.End.mem_eigenspace_iff, And.intro