awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R 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) ⊥
t : R
x : L
by_contra : ∀ (contra : ¬μ (t • x) = t • μ x), False
⊢ μ (t • x) = t • μ x

Tactic:
by_contra contra
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R 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) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
g : L → Submodule R M := fun (x : L) ↦ (genEigenspace ((f : (a : L) → End R M) x) (μ x) : (a : ℕ∞) → Submodule R M) k
⊢ ⨅ (x : L), g x ≤ g x ⊓ g (t • x)

Tactic:
have : ⨅ x, g x ≤ g x ⊓ g (t • x) := le_inf_iff.mpr ⟨iInf_le g x, iInf_le g (t • x)⟩
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R 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) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
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 (t • x)
⊢ False

Tactic:
h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))

Premises used: Iff.mpr, Iff.mp, disjoint_iff_inf_le, eq_bot_iff, le_trans
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R 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) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
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 (t • x)
refine : Disjoint (g x) (g (t • x))
⊢ False

Tactic:
refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))

Premises used: Iff.mpr, Iff.mp, disjoint_iff_inf_le, eq_bot_iff, le_trans
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R 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) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
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 (t • x)
apply :
  Disjoint
    (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (t * μ x) :
        (a : ℕ∞) → Submodule R M)
      k)
    (g (t • x))
⊢ Disjoint (g x) (g (t • x))

Tactic:
apply Disjoint.mono_left (genEigenspace_le_smul (f x) (μ x) t k)

Premises used: Disjoint.mono_left, DFunLike.coe, Module.End.genEigenspace_le_smul
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R 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) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
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 (t • x)
simp :
  Disjoint (α := Submodule R M)
    (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (t * μ x) :
          (a : ℕ∞) → Submodule R M)
        k :
      Submodule R M)
    (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (μ (t • x)) :
          (a : ℕ∞) → Submodule R M)
        k :
      Submodule R M)
⊢ Disjoint
    (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (t * μ x) :
        (a : ℕ∞) → Submodule R M)
      k)
    (g (t • x))

Tactic:
simp only [g, map_smul]

Premises used: map_smul
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R 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) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
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 (t • x)
⊢ Disjoint (α := Submodule R M)
    (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (t * μ x) :
          (a : ℕ∞) → Submodule R M)
        k :
      Submodule R M)
    (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (μ (t • x)) :
          (a : ℕ∞) → Submodule R M)
        k :
      Submodule R M)

Tactic:
disjoint_genEigenspace (t • f x) (Ne.symm contra) k k

Premises used: Ne.symm, Module.End.disjoint_genEigenspace, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : SMul R L
inst_6 : FunLike.{u_2 + 1, u_1 + 1, w + 1} F L (End R M)
inst_7 : MulActionHomClass.{u_2, v, u_1, w} F R 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) ⊥
t : R
x : L
contra : ¬μ (t • x) = t • μ x
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 (t • x)
⊢ Disjoint (α := Submodule R M)
    (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (t * μ x) :
          (a : ℕ∞) → Submodule R M)
        k :
      Submodule R M)
    (((HSMul.hSMul (β := End R M) t ((f : (a : L) → End R M) x : End R M)).genEigenspace (μ (t • x)) :
          (a : ℕ∞) → Submodule R M)
        k :
      Submodule R M)

Tactic:
exact disjoint_genEigenspace (t • f x) (Ne.symm contra) k k

Premises used: Ne.symm, Module.End.disjoint_genEigenspace, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
by_contra : ∀ (contra : ¬μ (x + y) = μ x + μ y), False
⊢ μ (x + y) = μ x + μ y

Tactic:
by_contra contra
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
⊢ ⨅ (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)⟩
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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

Tactic:
h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))

Premises used: Iff.mpr, Iff.mp, disjoint_iff_inf_le, eq_bot_iff, le_trans
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
refine : Disjoint (g x ⊓ g y) (g (x + y))
⊢ False

Tactic:
refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))

Premises used: Iff.mpr, Iff.mp, disjoint_iff_inf_le, eq_bot_iff, le_trans
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
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))
⊢ Disjoint (g x ⊓ g y) (g (x + y))

Tactic:
apply Disjoint.mono_left (genEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) k k (h x y))

Premises used: Module.End.genEigenspace_inf_le_add, Disjoint.mono_left, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
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)
⊢ 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:
simp only [g, map_add]

Premises used: map_add
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 (α := 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:
disjoint_genEigenspace (f x + f y) (Ne.symm contra) _ k

Premises used: Ne.symm, Module.End.disjoint_genEigenspace, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 (α := 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:
exact disjoint_genEigenspace (f x + f y) (Ne.symm contra) _ k

Premises used: Ne.symm, Module.End.disjoint_genEigenspace, HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly
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
rw :
  HPow.hPow (α := R) (-1) (finrank R M) * (f - HSMul.hSMul (β := End R M) μ 1).charpoly.coeff 0 = 0 ↔
    (charpoly f).IsRoot μ
⊢ f.HasEigenvalue μ ↔ (charpoly f).IsRoot μ

Tactic:
rw [hasEigenvalue_iff, eigenspace_def, ← det_eq_zero_iff_ker_ne_bot, det_eq_sign_charpoly_coeff]

Premises used: Module.End.hasEigenvalue_iff, LinearMap.det_eq_zero_iff_ker_ne_bot, Module.End.eigenspace_def, LinearMap.det_eq_sign_charpoly_coeff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly
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
⊢ HPow.hPow (α := R) (-1) (finrank R M) * (f - HSMul.hSMul (β := End R M) μ 1).charpoly.coeff 0 = 0 ↔
    (charpoly f).IsRoot μ

Tactic:
simp [Polynomial.coeff_zero_eq_eval_zero, charpoly_sub_smul]

Premises used: Polynomial.coeff_zero_eq_eval_zero, LinearMap.charpoly_sub_smul
-- Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly
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 μ
rw₁ rw₂ : (charpoly f).IsRoot μ ↔ (charpoly f).IsRoot μ
⊢ μ ∈ spectrum K f ↔ (charpoly f).IsRoot μ

Tactic:
rw [← hasEigenvalue_iff_mem_spectrum, hasEigenvalue_iff_isRoot_charpoly]

Premises used: Module.End.hasEigenvalue_iff_isRoot_charpoly, Module.End.hasEigenvalue_iff_mem_spectrum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly
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
⊢ Polynomial.Splits.{u_3} (R := K)
    (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))

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly
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
rw₂ rw₃ : (charpoly f).roots.prod = (charpoly f).roots.prod
⊢ (LinearMap.det : (a : V →ₗ[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]

Premises used: Matrix.det_eq_prod_roots_charpoly_of_splits, LinearMap.det_toMatrix, Module.Free.chooseBasis, LinearMap.charpoly_toMatrix
-- Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly
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
⊢ Polynomial.Splits.{u_3} (R := K)
    (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))

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.Eigenspace.Charpoly
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
rw₂ rw₃ : (charpoly f).roots.sum = (charpoly f).roots.sum
⊢ (trace K V : (a : V →ₗ[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]

Premises used: Matrix.trace_eq_sum_roots_charpoly_of_splits, LinearMap.trace_eq_matrix_trace, Module.Free.chooseBasis, LinearMap.charpoly_toMatrix
-- 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 : ℕ
rw : IsClosed (↑(↑((f - HSMul.hSMul (β := M →L[R] M) μ (ContinuousLinearMap.id R M)) ^ n) : M →ₗ[R] M).ker : Set M)
⊢ IsClosed (↑((genEigenspace (↑f : M →ₗ[R] M) μ : (a : ℕ∞) → Submodule R M) (↑n : ℕ∞) : Submodule R M) : Set M)

Tactic:
rw [genEigenspace_nat, one_eq_id, ← coe_id, ← coe_smul, ← coe_sub, ← coe_pow]

Premises used: Module.End.one_eq_id, ContinuousLinearMap.coe_pow, ContinuousLinearMap.coe_sub, Module.End.genEigenspace_nat, ContinuousLinearMap.coe_smul, ContinuousLinearMap.coe_id
-- 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 (↑(↑((f - HSMul.hSMul (β := M →L[R] M) μ (ContinuousLinearMap.id R M)) ^ n) : M →ₗ[R] M).ker : Set M)

Tactic:
apply isClosed_ker

Premises used: ContinuousLinearMap.isClosed_ker