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
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
⊢ ∃ (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)
have right : 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
-- 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
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
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
have right : Eq (α := M) ((((f - HSMul.hSMul (β := End R M) μ 1) ^ l) ∘ₗ g : (a : M) → M) x : 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]
-- 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
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)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
have right₁ : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l * g : (a : M) → M) x : 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]
-- 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
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)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
have right₂ : Eq (α := M) ((g * (f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : 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]
-- 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
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)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
have right₃ : Eq (α := M) ((g ∘ₗ (f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : 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]
-- 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
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)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
have right₄ : Eq (α := M) ((g : (a : M) → M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (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]
-- 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
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)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
have right₅ : Eq (α := M) ((g : (a : M) → M) 0 : 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]
-- 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
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)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
have right₆ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [← LinearMap.comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp,
    LinearMap.comp_apply, hx, map_zero]
-- 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
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)
⊢ IsNilpotent (LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h)
have h₁ : LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h ^ k = 0
Tactic: use k
-- 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
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)
⊢ LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h ^ k = 0
have 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)
Tactic: ext ⟨x, hx⟩
-- 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
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
⊢ 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)
have hx₁ : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
Tactic: rw [mem_genEigenspace_nat] at hx
-- 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
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.{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)
have 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))
      sorry :
    ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M))
  (0 : ↥((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M))
Tactic: rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero,
    Module.End.pow_restrict, LinearMap.restrict_apply]
-- 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
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 (α := ↥((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))
have 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))
          sorry) :
      M) :
    M)
  ((↑0 : M) : M)
Tactic: ext
-- 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 : 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 (LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h)
have 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)
Tactic: apply isNilpotent_restrict_of_le
-- 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 : 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)
⊢ IsNilpotent (LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h)
have 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) sorry)
Tactic: apply isNilpotent_restrict_of_le
-- 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 : 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) ⋯)
⊢ IsNilpotent (LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h)
have q : Submodule R M
Tactic: apply isNilpotent_restrict_of_le
-- 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 : 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
⊢ IsNilpotent (LinearMap.restrict (f - HSMul.hSMul (β := End R M) μ 1) h)
have 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)
Tactic: apply isNilpotent_restrict_of_le
-- 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 : 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)
⊢ 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)
have 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)
Tactic: rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
-- 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
f : End R M
μ : R
⊢ f.eigenspace μ = (f - HSMul.hSMul (β := End R M) μ 1).ker
have rw : (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 = (f - HSMul.hSMul (β := End R M) μ 1).ker
Tactic: rw [eigenspace, genEigenspace_one]
-- 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
f : End R M
μ : R
rw : (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 = (f - HSMul.hSMul (β := End R M) μ 1).ker
⊢ f.eigenspace μ = (f - HSMul.hSMul (β := End R M) μ 1).ker
have rw₁ : (f - HSMul.hSMul (β := End R M) μ 1).ker = (f - HSMul.hSMul (β := End R M) μ 1).ker
Tactic: rw [eigenspace, genEigenspace_one]
-- 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
f : End R M
μ : R
n : ℕ∞
x : M
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) n : Submodule R M) x
⊢ x ∈ Submodule.comap f ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) n)
have simp : ∀
  (hx :
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ n ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)),
  ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ n ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
Tactic: simp only [Submodule.mem_comap, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢
Cleared hypotheses: hx
-- 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
f : End R M
μ : R
n : ℕ∞
x : M
hx : ∃ (l : ℕ), (↑l : ℕ∞) ≤ n ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ n ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
have obtain : ∀ (k : ℕ) (hk : (↑k : ℕ∞) ≤ n)
  (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)),
  ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ n ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
Tactic: obtain ⟨k, hk, hx⟩ := hx
Cleared hypotheses: hx
-- 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
f : End R M
μ : R
n : ℕ∞
x : M
k : ℕ
hk : (↑k : ℕ∞) ≤ n
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ n ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
have refine : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
Tactic: refine ⟨k, hk, ?_⟩