awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : T0Space M
inst_5 : ContinuousConstSMul R M
inst_6 : IsTopologicalAddGroup M
f : M →L[R] M
μ : R
n : ℕ
⊢ IsClosed (↑(eigenspace (↑f : M →ₗ[R] M) μ) : Set M)

Tactic:
isClosed_genEigenspace f μ 1

Premises used: Set.Mem, ContinuousLinearMap.isClosed_genEigenspace, setOf, WithTop.some, OfNat.ofNat
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
i : n
b : Basis n R M
⊢ (((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M) : (a : M) → M) ((b : (a : n) → M) i : M) =
    HSMul.hSMul (β := M) (d i) ((b : (a : n) → M) i : M)

Tactic:
simp [diagonal]

Premises used: Matrix.diagonal
-- 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
inst_3 : Nontrivial R
d : n → R
i : n
⊢ HasEigenvector (M := n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal d) : (n → R) →ₗ[R] n → R)
    (d i) ((Pi.basisFun R n : (a : n) → n → R) i : n → R)

Tactic:
hasEigenvector_toLin_diagonal _ _ (Pi.basisFun R n)

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Pi.basisFun, Matrix.mulVec, Finset.sum, hasEigenvector_toLin_diagonal
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
⊢ ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)

Tactic:
have (i : n) : HasEigenvalue (toLin b b (diagonal d)) (d i) :=
    hasEigenvalue_of_hasEigenvector <| hasEigenvector_toLin_diagonal d i b
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
mp :
  HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ → ∃ (i : n), d i = μ
mpr :
  (∃ (i : n), d i = μ) → HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
⊢ HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ ↔ ∃ (i : n), d i = μ

Tactic:
constructor
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
mp :
  (∀ (i : n), d i ≠ μ) →
    ¬HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
⊢ HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ → ∃ (i : n), d i = μ

Tactic:
contrapose!
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
rw :
  Set.range.{u_3, u_2 + 1} (ι := n) (⇑b : (a : n) → M) ⊆
    (↑(⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) : Set M)
⊢ Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤

Tactic:
rw [eq_top_iff, ← b.span_eq, Submodule.span_le]

Premises used: eq_top_iff, Module.Basis.span_eq, Submodule.span_le
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
i : n
apply :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (⨆ (_ : d i ∈ Set.range d), eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i))
    ((b : (a : n) → M) i : M)
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)
    ((b : (a : n) → M) i : M)

Tactic:
apply Submodule.mem_iSup_of_mem (d i)

Premises used: Submodule.mem_iSup_of_mem
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
i : n
apply :
  Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)) ((b : (a : n) → M) i : M)
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (⨆ (_ : d i ∈ Set.range d), eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i))
    ((b : (a : n) → M) i : M)

Tactic:
apply Submodule.mem_iSup_of_mem ⟨i, rfl⟩

Premises used: Submodule.mem_iSup_of_mem
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
i : n
rw :
  (((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M) : (a : M) → M) ((b : (a : n) → M) i : M) =
    HSMul.hSMul (β := M) (d i) ((b : (a : n) → M) i : M)
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)) ((b : (a : n) → M) i : M)

Tactic:
rw [mem_eigenspace_iff]

Premises used: Module.End.mem_eigenspace_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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
i : n
⊢ (((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M) : (a : M) → M) ((b : (a : n) → M) i : M) =
    HSMul.hSMul (β := M) (d i) ((b : (a : n) → M) i : M)

Tactic:
(hasEigenvector_toLin_diagonal d i b).apply_eq_smul

Premises used: Module.End.HasEigenvector.apply_eq_smul, hasEigenvector_toLin_diagonal
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
i : n
⊢ (((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d) : M →ₗ[R] M) : (a : M) → M) ((b : (a : n) → M) i : M) =
    HSMul.hSMul (β := M) (d i) ((b : (a : n) → M) i : M)

Tactic:
exact (hasEigenvector_toLin_diagonal d i b).apply_eq_smul

Premises used: Module.End.HasEigenvector.apply_eq_smul, hasEigenvector_toLin_diagonal
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
⊢ Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤

Tactic:
have h_iSup : ⨆ μ ∈ Set.range d, eigenspace (toLin b b (diagonal d)) μ = ⊤ := by
      rw [eq_top_iff, ← b.span_eq, Submodule.span_le]
      rintro - ⟨i, rfl⟩
      simp only [SetLike.mem_coe]
      apply Submodule.mem_iSup_of_mem (d i)
      apply Submodule.mem_iSup_of_mem ⟨i, rfl⟩
      rw [mem_eigenspace_iff]
      exact (hasEigenvector_toLin_diagonal d i b).apply_eq_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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
h_iSup :
  Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤
⊢ μ ∉ Set.range d

Tactic:
simpa using fun i ↦ (hμ i)
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
h_iSup :
  Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤
⊢ μ ∉ Set.range d

Tactic:
have hμ_notMem : μ ∉ Set.range d := by simpa using fun i ↦ (hμ i)
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
h_iSup :
  Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤
hμ_notMem : μ ∉ Set.range d
⊢ Disjoint.{u_3} (α := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)
    (⨆ i ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) i)

Tactic:
have := eigenspaces_iSupIndep (toLin b b (diagonal d)) |>.disjoint_biSup hμ_notMem
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this_1 : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
h_iSup :
  Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤
hμ_notMem : μ ∉ Set.range d
this :
  Disjoint.{u_3} (α := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)
    (⨆ i ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) i)
⊢ Eq.{u_3 + 1} (α := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊥

Tactic:
rw [h_iSup, disjoint_top] at this

Premises used: disjoint_top
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this_1 : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
h_iSup :
  Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤
hμ_notMem : μ ∉ Set.range d
this : Eq.{u_3 + 1} (α := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊥
⊢ False

Tactic:
h_eig this
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
μ : R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this_1 : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
hμ : ∀ (i : n), d i ≠ μ
h_eig : HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ
h_iSup :
  Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ μ ∈ Set.range d, eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤
hμ_notMem : μ ∉ Set.range d
this : Eq.{u_3 + 1} (α := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊥
⊢ False

Tactic:
exact h_eig this
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
i : n
⊢ HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)

Tactic:
this i
-- 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 : Nontrivial R
inst_4 : AddCommGroup M
inst_5 : Module R M
d : n → R
inst_6 : IsDomain R
inst_7 : IsTorsionFree R M
b : Basis n R M
this : ∀ (i : n), HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)
i : n
⊢ HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d i)

Tactic:
exact this i
-- 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
inst_3 : Nontrivial R
inst_4 : IsDomain R
d : n → R
μ : R
⊢ HasEigenvalue (M := n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal d)) μ ↔ ∃ (i : n), d i = μ

Tactic:
hasEigenvalue_toLin_diagonal_iff _ <| Pi.basisFun R n

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Pi.basisFun, Matrix.mulVec, Finset.sum, hasEigenvalue_toLin_diagonal_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
b : Basis n R M
⊢ Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ (μ : R), eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤

Tactic:
(Submodule.eq_top_iff_forall_basis_mem b).mpr fun j ↦ ?_

Premises used: Iff.mpr, Submodule.eq_top_iff_forall_basis_mem
-- 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
b : Basis n R M
refine :
  ∀ (j : n),
    Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
      (⨆ (μ : R), eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ((b : (a : n) → M) j : M)
⊢ Eq.{u_3 + 1} (α := Submodule R M)
    (⨆ (μ : R), eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ⊤

Tactic:
refine (Submodule.eq_top_iff_forall_basis_mem b).mpr fun j ↦ ?_

Premises used: Iff.mpr, Submodule.eq_top_iff_forall_basis_mem
-- 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
b : Basis n R M
j : n
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) (d j)) ((b : (a : n) → M) j : M)

Tactic:
simp [diagonal_apply]

Premises used: 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
b : Basis n R M
j : n
⊢ Membership.mem.{u_3, u_3} (α := M) (γ := Submodule R M)
    (⨆ (μ : R), eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) ((b : (a : n) → M) j : M)

Tactic:
exact Submodule.mem_iSup_of_mem (d j) <| by simp [diagonal_apply]

Premises used: Submodule.mem_iSup_of_mem
-- 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
⊢ Eq (α := Submodule R (n → R))
    (⨆ (μ : R), eigenspace (M := n → R) ((toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (diagonal d)) μ) ⊤

Tactic:
iSup_eigenspace_toLin_diagonal_eq_top d <| Pi.basisFun R n

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Pi.basisFun, Matrix.iSup_eigenspace_toLin_diagonal_eq_top, 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
d : n → R
μ : R
b : Basis n R M
inst_5 : IsDomain R
⊢ Eq.{u_3 + 1} (α := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)
    (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)

Tactic:
le_antisymm (fun x hx ↦ ?_) eigenspace_le_maxGenEigenspace

Premises used: le_antisymm, Module.End.eigenspace_le_maxGenEigenspace
-- 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
refine :
  ∀ (x : M)
    (hx :
      Membership.mem (γ := Submodule R M)
        (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x),
    Membership.mem (γ := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
⊢ Eq.{u_3 + 1} (α := Submodule R M) (maxGenEigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)
    (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ)

Tactic:
refine le_antisymm (fun x hx ↦ ?_) eigenspace_le_maxGenEigenspace

Premises used: le_antisymm, Module.End.eigenspace_le_maxGenEigenspace
-- 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
obtain :
  ∀ (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)),
    Membership.mem (γ := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x
⊢ Membership.mem (γ := Submodule R M) (eigenspace ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ) x

Tactic:
obtain ⟨k, hk⟩ := (mem_maxGenEigenspace _ _ _).mp hx

Premises used: Iff.mp, Module.End.mem_maxGenEigenspace
-- 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
rw :
  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))
⊢ 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:
rw [Pi.sub_def, ← diagonal_sub]

Premises used: Pi.sub_def, Matrix.diagonal_sub