awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ LE.le (α := Submodule K V)
    (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V)
        (finrank K V) :
      Submodule K V)
    (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) n :
      Submodule K V)

Tactic:
exact (f.genEigenspace μ).monotone <| WithTop.coeOrderHom.monotone hn

Premises used: OrderEmbedding.monotone, OrderHom.monotone, WithTop.coeOrderHom, Module.End.genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
hm : ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).ker ≤ ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V).ker
⊢ LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑n : ℕ∞) : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)

Tactic:
rw [genEigenspace_nat, genEigenspace_nat]

Premises used: Module.End.genEigenspace_nat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).ker ≤ ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V).ker

Tactic:
apply ker_pow_le_ker_pow_finrank

Premises used: Module.End.ker_pow_le_ker_pow_finrank
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤ : Submodule K V)

Tactic:
(f.genEigenspace _).monotone le_top

Premises used: OrderHom.monotone, Set.Mem, le_top, Module.End.genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
rw :
  LE.le (α := Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
⊢ LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤ : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)

Tactic:
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]

Premises used: Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ LE.le (α := ℕ∞) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) (↑(finrank K V) : ℕ∞)

Tactic:
simpa using maxUnifEigenspaceIndex_le_finrank f μ

Premises used: Module.End.maxUnifEigenspaceIndex_le_finrank
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ LE.le (α := Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)

Tactic:
exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ

Premises used: OrderHom.monotone, Module.End.genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
calc :
  LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤ : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
⊢ LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)

Tactic:
calc f.genEigenspace μ k
      ≤ f.genEigenspace μ ⊤ := (f.genEigenspace _).monotone le_top
    _ ≤ f.genEigenspace μ (finrank K V) := by
      rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
      exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ

Premises used: OrderHom.monotone, Nat.cast, le_top, Module.End.genEigenspace, Top.top, DFunLike.coe, Module.finrank
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
k : ℕ
hk : finrank K V ≤ k
⊢ LE.le (α := ℕ∞) (↑(finrank K V) : ℕ∞) (↑k : ℕ∞)

Tactic:
simpa using hk
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
hx : x ∈ (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
simp :
  ∀
    (hx :
      ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)),
    ∃ (l : ℕ),
      (↑l : ℕ∞) ≤ k ∧
        Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
⊢ Membership.mem (α := M) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
    ((g : (a : M) → M) x : M)

Tactic:
simp only [SetLike.mem_coe, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢

Premises used: LinearMap.mem_ker, SetLike.mem_coe, Module.End.mem_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
hx : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
rcases :
  ∀ (l : ℕ) (hl : (↑l : ℕ∞) ≤ k)
    (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)),
    ∃ (l : ℕ),
      (↑l : ℕ∞) ≤ k ∧
        Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)

Tactic:
rcases hx with ⟨l, hl, hx⟩
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
l : ℕ
hl : (↑l : ℕ∞) ≤ k
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
⊢ Commute ((f - HSMul.hSMul (β := End R M) μ 1) ^ l) g

Tactic:
replace h : Commute ((f - μ • (1 : End R M)) ^ l) g :=
    (h.sub_left <| Algebra.commute_algebraMap_left μ g).pow_left l
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : (↑l : ℕ∞) ≤ k
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
h : Commute ((f - HSMul.hSMul (β := End R M) μ 1) ^ l) g
right : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)

Tactic:
use l, hl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
x : M
l : ℕ
hl : (↑l : ℕ∞) ≤ k
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
h : Commute ((f - HSMul.hSMul (β := End R M) μ 1) ^ l) g
right : Eq (α := M) ((((f - HSMul.hSMul (β := End R M) μ 1) ^ l) ∘ₗ g : (a : M) → M) x : M) (0 : M)
right₁ : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l * g : (a : M) → M) x : M) (0 : M)
right₂ : Eq (α := M) ((g * (f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
right₃ : Eq (α := M) ((g ∘ₗ (f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
right₄ : Eq (α := M) ((g : (a : M) → M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) : M) (0 : M)
right₅ : Eq (α := M) ((g : (a : M) → M) 0 : M) (0 : M)
right₆ right₇ : Eq.{w + 1} (α := M) 0 0
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)

Tactic:
rw [← LinearMap.comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp,
    LinearMap.comp_apply, hx, map_zero]

Premises used: Module.End.mul_eq_comp, LinearMap.comp_apply, map_zero, Commute.eq
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
h :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
h₁ : LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h ^ k = 0
⊢ IsNilpotent (LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h)

Tactic:
use k
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
h :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
h₁ :
  ∀ (x : M)
    (hx :
      Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x),
    Eq.{w + 1} (α := M)
      (↑((LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h ^ k :
              (a : ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞))) →
                ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞)))
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Submodule R M)
                ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
              x hx)) :
        M)
      (↑((0 :
              (a : ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞))) →
                ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞)))
            (Subtype.mk (p := fun (x : M) ↦
              Membership.mem (γ := Submodule R M)
                ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
              x hx)) :
        M)
⊢ LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h ^ k = 0

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
h :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
x : M
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x
⊢ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker

Tactic:
rw [mem_genEigenspace_nat] at hx

Premises used: Module.End.mem_genEigenspace_nat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
h :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
x : M
hx_1 : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
h₁ :
  Eq (α := ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M))
    (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M)
          x)
        (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
          (↑(Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule R M)
                  ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
                x hx_1) :
            M))
        ⋯ :
      ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M))
    (0 : ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M))
⊢ Eq.{w + 1} (α := M)
    (↑((LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h ^ k :
            (a : ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞))) →
              ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞)))
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule R M)
              ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
            x hx_1)) :
      M)
    (↑((0 :
            (a : ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞))) →
              ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞)))
          (Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule R M)
              ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
            x hx_1)) :
      M)

Tactic:
rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero,
    Module.End.pow_restrict, LinearMap.restrict_apply]

Premises used: ZeroMemClass.coe_eq_zero, Module.End.pow_apply_mem_of_forall_mem, LinearMap.zero_apply, Module.End.pow_restrict, ZeroMemClass.coe_zero, LinearMap.restrict_apply
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
h :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
x : M
hx_1 : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
h₁ :
  Eq (α := M)
    ((↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule R M)
              ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
            (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
              (↑(Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := Submodule R M)
                      ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
                    x hx_1) :
                M))
            ⋯) :
        M) :
      M)
    ((↑0 : M) : M)
⊢ Eq (α := ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M))
    (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M)
          x)
        (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
          (↑(Subtype.mk (p := fun (x : M) ↦
                Membership.mem (γ := Submodule R M)
                  ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
                x hx_1) :
            M))
        ⋯ :
      ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M))
    (0 : ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
h :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
x : M
hx_1 : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
⊢ Eq (α := M)
    ((↑(Subtype.mk (p := fun (x : M) ↦
            Membership.mem (γ := Submodule R M)
              ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
            (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
              (↑(Subtype.mk (p := fun (x : M) ↦
                    Membership.mem (γ := Submodule R M)
                      ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x)
                    x hx_1) :
                M))
            ⋯) :
        M) :
      M)
    ((↑0 : M) : M)

Tactic:
simpa
-- 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 : IsNoetherian R M
f : End R M
μ : R
h :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M) : Set M)
h₁ :
  LE.le (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M)
hf :
  IsNilpotent (R :=
    ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M) →ₗ[R]
      ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M))
    (LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) ⋯)
q : Submodule R M
hq :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M) : Set M)
⊢ IsNilpotent (LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h)

Tactic:
apply isNilpotent_restrict_of_le

Premises used: Module.End.isNilpotent_restrict_of_le
-- 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 : IsNoetherian R M
f : End R M
μ : R
h :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M) : Set M)
⊢ IsNilpotent (R :=
    ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M) →ₗ[R]
      ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M))
    (LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) ⋯)

Tactic:
apply isNilpotent_restrict_genEigenspace_nat f μ (maxUnifEigenspaceIndex f μ)

Premises used: Module.End.isNilpotent_restrict_genEigenspace_nat, Module.End.mapsTo_genEigenspace_of_comm, Module.End.maxUnifEigenspaceIndex, Algebra.mul_sub_algebraMap_commutes, Nat.cast
-- 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 : IsNoetherian R M
f : End R M
μ : R
h :
  MapsTo (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M) : Set M)
h₁ h₂ :
  LE.le (α := Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M)
⊢ LE.le (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M)

Tactic:
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]

Premises used: Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
rw : (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 = (f - HSMul.hSMul (β := End R M) μ 1).ker
rw₁ rw₂ : (f - HSMul.hSMul (β := End R M) μ 1).ker = (f - HSMul.hSMul (β := End R M) μ 1).ker
⊢ f.eigenspace μ = (f - HSMul.hSMul (β := End R M) μ 1).ker

Tactic:
rw [eigenspace, genEigenspace_one]

Premises used: Module.End.eigenspace, Module.End.genEigenspace_one
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
⊢ f.eigenspace 0 = LinearMap.ker f

Tactic:
simp only [eigenspace, ← Nat.cast_one (R := ℕ∞), genEigenspace_zero_nat, pow_one]

Premises used: Module.End.eigenspace, Module.End.genEigenspace_zero_nat, pow_one, Nat.cast_one
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
⊢ f.HasEigenvector μ x ↔ x ∈ f.eigenspace μ ∧ x ≠ 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Module.End.HasUnifEigenvector
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
⊢ f.HasEigenvalue μ ↔ f.eigenspace μ ≠ ⊥

Tactic:
Iff.rfl

Premises used: Iff.rfl, Module.End.HasUnifEigenvalue
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
h : f.HasEigenvalue μ
⊢ (↑f : f.Eigenvalues → R) (Subtype.mk (p := fun (μ : R) ↦ f.HasUnifEigenvalue μ 1) μ h) = μ

Tactic:
rfl

Premises used: Module.End.UnifEigenvalues.val, rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : f.Eigenvalues
⊢ Subtype.mk (p := fun (μ : R) ↦ f.HasUnifEigenvalue μ 1) ((↑f : f.Eigenvalues → R) μ) ⋯ = μ

Tactic:
rfl

Premises used: Module.End.UnifEigenvalues.val, Module.End.UnifEigenvalues, rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
h : f.HasEigenvector μ x
⊢ f.HasEigenvalue μ

Tactic:
h.hasUnifEigenvalue

Premises used: Module.End.HasUnifEigenvector.hasUnifEigenvalue
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
⊢ x ∈ f.eigenspace μ ↔ (f : (a : M) → M) x = μ • x

Tactic:
mem_genEigenspace_one

Premises used: Set.Mem, Module.End.mem_genEigenspace_one
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
hx : f.HasEigenvector μ x
⊢ (f : (a : M) → M) x = μ • x

Tactic:
hx.apply_eq_smul

Premises used: Module.End.HasUnifEigenvector.apply_eq_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
f : End R M
μ : R
v : M
hv : f.HasEigenvector μ v
n : ℕ
⊢ (f ^ n : (a : M) → M) v = μ ^ n • v

Tactic:
hv.pow_apply n

Premises used: Module.End.HasUnifEigenvector.pow_apply