awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : Add L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : AddHomClass.{u_2, u_1, w} F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
h : ∀ (x y : L), Commute.{w} (S := End R M) ((f : (a : L) → End R M) x : End R M) ((f : (a : L) → End R M) y : End R M)
x y : L
⊢ μ (x + y) = μ x + μ y
have by_contra : ∀ (contra : ¬μ (x + y) = μ x + μ y), False
Tactic: by_contra contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (hypothesis)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : Add L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : AddHomClass.{u_2, u_1, w} F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
h : ∀ (x y : L), Commute.{w} (S := End R M) ((f : (a : L) → End R M) x : End R M) ((f : (a : L) → End R M) y : End R M)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun (x : L) ↦ (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k
⊢ False
have this : ⨅ (x : L), g x ≤ g x ⊓ g y ⊓ g (x + y)
Tactic: have : ⨅ x, g x ≤ (g x ⊓ g y) ⊓ g (x + y) :=
    le_inf_iff.mpr ⟨le_inf_iff.mpr ⟨iInf_le g x, iInf_le g y⟩, iInf_le g (x + y)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : Add L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : AddHomClass.{u_2, u_1, w} F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
h : ∀ (x y : L), Commute.{w} (S := End R M) ((f : (a : L) → End R M) x : End R M) ((f : (a : L) → End R M) y : End R M)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun (x : L) ↦ (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k
this : ⨅ (x : L), g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ False
have refine : Disjoint (g x ⊓ g y) (g (x + y))
Tactic: refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : Add L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : AddHomClass.{u_2, u_1, w} F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
h : ∀ (x y : L), Commute.{w} (S := End R M) ((f : (a : L) → End R M) x : End R M) ((f : (a : L) → End R M) y : End R M)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun (x : L) ↦ (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k
this : ⨅ (x : L), g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint (g x ⊓ g y) (g (x + y))
have apply : Disjoint
  (((HAdd.hAdd (α := End R M) (β := End R M) ((f : (a : L) → End R M) x : End R M)
            ((f : (a : L) → End R M) y : End R M)).genEigenspace
        (μ x + μ y) :
      (a : ℕ∞) → Submodule R M)
    (k + k))
  (g (x + y))
Tactic: apply Disjoint.mono_left (genEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) k k (h x y))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
L : Type u_1
F : Type u_2
inst_5 : Add L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : AddHomClass.{u_2, u_1, w} F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne :
  Ne.{w + 1} (α := Submodule R M)
    (⨅ (x : L), (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k) ⊥
h : ∀ (x y : L), Commute.{w} (S := End R M) ((f : (a : L) → End R M) x : End R M) ((f : (a : L) → End R M) y : End R M)
x y : L
contra : ¬μ (x + y) = μ x + μ y
g : L → Submodule R M := fun (x : L) ↦ (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k
this : ⨅ (x : L), g x ≤ g x ⊓ g y ⊓ g (x + y)
⊢ Disjoint
    (((HAdd.hAdd (α := End R M) (β := End R M) ((f : (a : L) → End R M) x : End R M)
              ((f : (a : L) → End R M) y : End R M)).genEigenspace
          (μ x + μ y) :
        (a : ℕ∞) → Submodule R M)
      (k + k))
    (g (x + y))
have simp : Disjoint (α := Submodule R M)
  (((HAdd.hAdd (α := End R M) (β := End R M) ((f : (a : L) → End R M) x : End R M)
              ((f : (a : L) → End R M) y : End R M)).genEigenspace
          (μ x + μ y) :
        (a : ℕ∞) → Submodule R M)
      (k + k) :
    Submodule R M)
  (((HAdd.hAdd (α := End R M) (β := End R M) ((f : (a : L) → End R M) x : End R M)
              ((f : (a : L) → End R M) y : End R M)).genEigenspace
          (μ (x + y)) :
        (a : ℕ∞) → Submodule R M)
      k :
    Submodule R M)
Tactic: simp only [g, map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Charpoly (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Free R M
inst_5 : Module.Finite R M
f : End R M
μ : R
⊢ f.HasEigenvalue μ ↔ (charpoly f).IsRoot μ
have rw : HPow.hPow (α := R) (-1) (finrank R M) * (f - HSMul.hSMul (β := End R M) μ 1).charpoly.coeff 0 = 0 ↔
  (charpoly f).IsRoot μ
Tactic: rw [hasEigenvalue_iff, eigenspace_def, ← det_eq_zero_iff_ker_ne_bot, det_eq_sign_charpoly_coeff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Charpoly (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
f : End K V
μ : K
⊢ μ ∈ spectrum K f ↔ (charpoly f).IsRoot μ
have rw : f.HasEigenvalue μ ↔ (charpoly f).IsRoot μ
Tactic: rw [← hasEigenvalue_iff_mem_spectrum, hasEigenvalue_iff_isRoot_charpoly]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Charpoly (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
f : End K V
μ : K
rw : f.HasEigenvalue μ ↔ (charpoly f).IsRoot μ
⊢ μ ∈ spectrum K f ↔ (charpoly f).IsRoot μ
have rw₁ : (charpoly f).IsRoot μ ↔ (charpoly f).IsRoot μ
Tactic: rw [← hasEigenvalue_iff_mem_spectrum, hasEigenvalue_iff_isRoot_charpoly]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Charpoly (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
f : End K V
h : (charpoly f).Splits
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) f = (charpoly f).roots.prod
have rw : Matrix.det.{u_3, u_4} (n := Free.ChooseBasisIndex K V)
    ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
        (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
      f) =
  (charpoly f).roots.prod
Tactic: rw [← det_toMatrix (Module.Free.chooseBasis K V),
    Matrix.det_eq_prod_roots_charpoly_of_splits (by simpa using h), charpoly_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Charpoly (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
f : End K V
h : (charpoly f).Splits
rw :
  Matrix.det.{u_3, u_4} (n := Free.ChooseBasisIndex K V)
      ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
          (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
        f) =
    (charpoly f).roots.prod
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) f = (charpoly f).roots.prod
have rw₁ : Multiset.prod
    (Polynomial.roots
      (Matrix.charpoly.{u_3, u_4} (n := Free.ChooseBasisIndex K V)
        ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
            (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
          f))) =
  (charpoly f).roots.prod
Tactic: rw [← det_toMatrix (Module.Free.chooseBasis K V),
    Matrix.det_eq_prod_roots_charpoly_of_splits (by simpa using h), charpoly_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Charpoly (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
f : End K V
h : (charpoly f).Splits
rw :
  Matrix.det.{u_3, u_4} (n := Free.ChooseBasisIndex K V)
      ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
          (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
        f) =
    (charpoly f).roots.prod
rw₁ :
  Multiset.prod
      (Polynomial.roots
        (Matrix.charpoly.{u_3, u_4} (n := Free.ChooseBasisIndex K V)
          ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
              (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
            f))) =
    (charpoly f).roots.prod
⊢ (LinearMap.det : (a : V →ₗ[K] V) → K) f = (charpoly f).roots.prod
have rw₂ : (charpoly f).roots.prod = (charpoly f).roots.prod
Tactic: rw [← det_toMatrix (Module.Free.chooseBasis K V),
    Matrix.det_eq_prod_roots_charpoly_of_splits (by simpa using h), charpoly_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Charpoly (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
f : End K V
h : (charpoly f).Splits
b : Basis (Free.ChooseBasisIndex K V) K V := Free.chooseBasis K V
⊢ (trace K V : (a : V →ₗ[K] V) → K) f = (charpoly f).roots.sum
have rw : Matrix.trace.{u_4, u_3} (n := Free.ChooseBasisIndex K V)
    ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
        (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
      f) =
  (charpoly f).roots.sum
Tactic: rw [trace_eq_matrix_trace K (Module.Free.chooseBasis K V),
    Matrix.trace_eq_sum_roots_charpoly_of_splits (by simpa using h), charpoly_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Charpoly (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
f : End K V
h : (charpoly f).Splits
b : Basis (Free.ChooseBasisIndex K V) K V := Free.chooseBasis K V
rw :
  Matrix.trace.{u_4, u_3} (n := Free.ChooseBasisIndex K V)
      ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
          (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
        f) =
    (charpoly f).roots.sum
⊢ (trace K V : (a : V →ₗ[K] V) → K) f = (charpoly f).roots.sum
have rw₁ : Multiset.sum
    (Polynomial.roots
      (Matrix.charpoly.{u_3, u_4} (n := Free.ChooseBasisIndex K V)
        ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
            (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
          f))) =
  (charpoly f).roots.sum
Tactic: rw [trace_eq_matrix_trace K (Module.Free.chooseBasis K V),
    Matrix.trace_eq_sum_roots_charpoly_of_splits (by simpa using h), charpoly_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Charpoly (goal)
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : Module.Finite K V
f : End K V
h : (charpoly f).Splits
b : Basis (Free.ChooseBasisIndex K V) K V := Free.chooseBasis K V
rw :
  Matrix.trace.{u_4, u_3} (n := Free.ChooseBasisIndex K V)
      ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
          (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
        f) =
    (charpoly f).roots.sum
rw₁ :
  Multiset.sum
      (Polynomial.roots
        (Matrix.charpoly.{u_3, u_4} (n := Free.ChooseBasisIndex K V)
          ((toMatrix (Free.chooseBasis K V) (Free.chooseBasis K V) :
              (a : V →ₗ[K] V) → Matrix (Free.ChooseBasisIndex K V) (Free.ChooseBasisIndex K V) K)
            f))) =
    (charpoly f).roots.sum
⊢ (trace K V : (a : V →ₗ[K] V) → K) f = (charpoly f).roots.sum
have rw₂ : (charpoly f).roots.sum = (charpoly f).roots.sum
Tactic: rw [trace_eq_matrix_trace K (Module.Free.chooseBasis K V),
    Matrix.trace_eq_sum_roots_charpoly_of_splits (by simpa using h), charpoly_toMatrix]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap (goal)
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 (↑((genEigenspace (↑f : M →ₗ[R] M) μ : (a : ℕ∞) → Submodule R M) (↑n : ℕ∞) : Submodule R M) : Set M)
have rw : IsClosed (↑(↑((f - HSMul.hSMul (β := M →L[R] M) μ (ContinuousLinearMap.id R M)) ^ n) : M →ₗ[R] M).ker : Set M)
Tactic: rw [genEigenspace_nat, one_eq_id, ← coe_id, ← coe_smul, ← coe_sub, ← coe_pow]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (hypothesis)
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
⊢ HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ ↔ ∃ (i : n), d i = μ
have 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)
Tactic: have (i : n) : HasEigenvalue (toLin b b (diagonal d)) (d i) :=
    hasEigenvalue_of_hasEigenvector <| hasEigenvector_toLin_diagonal d i b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
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)
⊢ HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ ↔ ∃ (i : n), d i = μ
have 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 = μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
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 = μ
⊢ HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ ↔ ∃ (i : n), d i = μ
have 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)) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
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)
⊢ HasEigenvalue.{u_1, u_3} (M := M) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (diagonal d)) μ → ∃ (i : n), d i = μ
have 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)) μ
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
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)) μ) ⊤
have 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)
Tactic: rw [eq_top_iff, ← b.span_eq, Submodule.span_le]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
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
⊢ 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)
have 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)
Tactic: apply Submodule.mem_iSup_of_mem (d i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
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
⊢ 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)
have 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)
Tactic: apply Submodule.mem_iSup_of_mem ⟨i, rfl⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (goal)
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
⊢ 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)
have 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)
Tactic: rw [mem_eigenspace_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (hypothesis)
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)) μ
⊢ False
have 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)) μ) ⊤
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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (hypothesis)
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)) μ) ⊤
⊢ False
have hμ_notMem : μ ∉ Set.range d
Tactic: have hμ_notMem : μ ∉ Set.range d := by simpa using fun i ↦ (hμ i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Matrix (hypothesis)
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
⊢ False
have 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)
Tactic: have := eigenspaces_iSupIndep (toLin b b (diagonal d)) |>.disjoint_biSup hμ_notMem