awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
k : ℕ∞
m : K →₀ V
hm₂ :
  ∀ (i : K),
    Membership.mem (α := V) (γ := Submodule K V) ((f.genEigenspace i : (a : ℕ∞) → Submodule K V) k : Submodule K V)
      ((m : (a : K) → V) i : V)
hm₀ : (m.sum fun (_i : K) (xi : V) ↦ xi) ∈ p
hm₁ :
  Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
    (m.sum fun (_i : K) (xi : V) ↦ xi)
μ : K
hμ : μ ∈ m.support
l : (i : K) → ℕ
hlk : ∀ (i : K), (↑(l i) : ℕ∞) ≤ k
hl : ∀ (i : K), Membership.mem (α := V) ((f - HSMul.hSMul (β := End K V) i 1) ^ l i).ker ((m : (a : K) → V) i : V)
l₀ : ℕ := m.support.sup l
h_comm :
  ∀ (μ₁ μ₂ : K),
    Commute (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀)
      (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₂ : End K V) ^ l₀)
g : End K V :=
  (m.support.erase μ).noncommProd
    (fun (μ₁ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀) ⋯
hfg : Commute f g
hg₀ :
  Eq (α := V) ((g : (a : V) → V) (m.sum fun (_μ : K) (mμ : V) ↦ mμ) : V)
    ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)
hg₁ : MapsTo (⇑g : (a : V) → V) (↑p : Set V) (↑p : Set V)
hg₂ :
  MapsTo (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
hg₃ : InjOn (β := V) (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
this :
  MapsTo (⇑g : (a : V) → V) (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
    (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
⊢ SurjOn (⇑g : (a : V) → V) (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
    (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
have rw : InjOn (β := V) (⇑g : (a : V) → V) (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
Tactic: rw [← LinearMap.injOn_iff_surjOn this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
k : ℕ∞
m : K →₀ V
hm₂ :
  ∀ (i : K),
    Membership.mem (α := V) (γ := Submodule K V) ((f.genEigenspace i : (a : ℕ∞) → Submodule K V) k : Submodule K V)
      ((m : (a : K) → V) i : V)
hm₀ : (m.sum fun (_i : K) (xi : V) ↦ xi) ∈ p
hm₁ :
  Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
    (m.sum fun (_i : K) (xi : V) ↦ xi)
μ : K
hμ : μ ∈ m.support
l : (i : K) → ℕ
hlk : ∀ (i : K), (↑(l i) : ℕ∞) ≤ k
hl : ∀ (i : K), Membership.mem (α := V) ((f - HSMul.hSMul (β := End K V) i 1) ^ l i).ker ((m : (a : K) → V) i : V)
l₀ : ℕ := m.support.sup l
h_comm :
  ∀ (μ₁ μ₂ : K),
    Commute (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀)
      (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₂ : End K V) ^ l₀)
g : End K V :=
  (m.support.erase μ).noncommProd
    (fun (μ₁ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀) ⋯
hfg : Commute f g
hg₀ :
  Eq (α := V) ((g : (a : V) → V) (m.sum fun (_μ : K) (mμ : V) ↦ mμ) : V)
    ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)
hg₁ : MapsTo (⇑g : (a : V) → V) (↑p : Set V) (↑p : Set V)
hg₂ :
  MapsTo (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
hg₃ : InjOn (β := V) (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
⊢ Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
have hg₄ : SurjOn (⇑g : (a : V) → V) (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
  (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
Tactic: have hg₄ : SurjOn g
      ↑(p ⊓ f.genEigenspace μ k) ↑(p ⊓ f.genEigenspace μ k) := by
    have : MapsTo g
        ↑(p ⊓ f.genEigenspace μ k) ↑(p ⊓ f.genEigenspace μ k) :=
      hg₁.inter_inter hg₂
    rw [← LinearMap.injOn_iff_surjOn this]
    exact hg₃.mono inter_subset_right
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
k : ℕ∞
m : K →₀ V
hm₂ :
  ∀ (i : K),
    Membership.mem (α := V) (γ := Submodule K V) ((f.genEigenspace i : (a : ℕ∞) → Submodule K V) k : Submodule K V)
      ((m : (a : K) → V) i : V)
hm₀ : (m.sum fun (_i : K) (xi : V) ↦ xi) ∈ p
hm₁ :
  Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
    (m.sum fun (_i : K) (xi : V) ↦ xi)
μ : K
hμ : μ ∈ m.support
l : (i : K) → ℕ
hlk : ∀ (i : K), (↑(l i) : ℕ∞) ≤ k
hl : ∀ (i : K), Membership.mem (α := V) ((f - HSMul.hSMul (β := End K V) i 1) ^ l i).ker ((m : (a : K) → V) i : V)
l₀ : ℕ := m.support.sup l
h_comm :
  ∀ (μ₁ μ₂ : K),
    Commute (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀)
      (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₂ : End K V) ^ l₀)
g : End K V :=
  (m.support.erase μ).noncommProd
    (fun (μ₁ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀) ⋯
hfg : Commute f g
hg₀ :
  Eq (α := V) ((g : (a : V) → V) (m.sum fun (_μ : K) (mμ : V) ↦ mμ) : V)
    ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)
hg₁ : MapsTo (⇑g : (a : V) → V) (↑p : Set V) (↑p : Set V)
hg₂ :
  MapsTo (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
hg₃ : InjOn (β := V) (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
hg₄ :
  SurjOn (⇑g : (a : V) → V) (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
    (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
⊢ Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
have hm₃ : Membership.mem (α := V) (γ := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
  ((m : (a : K) → V) μ : V)
Tactic: specialize hm₂ μ
Cleared hypotheses: hm₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
k : ℕ∞
m : K →₀ V
hm₀ : (m.sum fun (_i : K) (xi : V) ↦ xi) ∈ p
hm₁ :
  Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
    (m.sum fun (_i : K) (xi : V) ↦ xi)
μ : K
hμ : μ ∈ m.support
l : (i : K) → ℕ
hlk : ∀ (i : K), (↑(l i) : ℕ∞) ≤ k
hl : ∀ (i : K), Membership.mem (α := V) ((f - HSMul.hSMul (β := End K V) i 1) ^ l i).ker ((m : (a : K) → V) i : V)
l₀ : ℕ := m.support.sup l
h_comm :
  ∀ (μ₁ μ₂ : K),
    Commute (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀)
      (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₂ : End K V) ^ l₀)
g : End K V :=
  (m.support.erase μ).noncommProd
    (fun (μ₁ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀) ⋯
hfg : Commute f g
hg₀ :
  Eq (α := V) ((g : (a : V) → V) (m.sum fun (_μ : K) (mμ : V) ↦ mμ) : V)
    ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)
hg₁ : MapsTo (⇑g : (a : V) → V) (↑p : Set V) (↑p : Set V)
hg₂ :
  MapsTo (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
hg₃ : InjOn (β := V) (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
hg₄ :
  SurjOn (⇑g : (a : V) → V) (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
    (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
hm₂ :
  Membership.mem (α := V) (γ := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
    ((m : (a : K) → V) μ : V)
⊢ Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
have pos : ∀ (y : V) (hy₂ : Eq (α := V) ((g : (a : V) → V) y : V) ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)) (hy₀ : y ∈ p)
  (hy₁ : Membership.mem (γ := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) y),
  Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
Tactic: obtain ⟨y, ⟨hy₀ : y ∈ p, hy₁ : y ∈ f.genEigenspace μ k⟩, hy₂ : g y = g (m μ)⟩ :=
    hg₄ ⟨(hg₀ ▸ hg₁ hm₀), hg₂ hm₂⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) ⊤
⊢ p = ⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
have rw : p = p ⊓ ⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
Tactic: rw [← inf_iSup_genEigenspace h, h', inf_top_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) ⊤
rw : p = p ⊓ ⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
⊢ p = ⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
have rw₁ : p = p ⊓ ⊤
Tactic: rw [← inf_iSup_genEigenspace h, h', inf_top_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) ⊤
rw : p = p ⊓ ⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
rw₁ : p = p ⊓ ⊤
⊢ p = ⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
have rw₂ : p = p
Tactic: rw [← inf_iSup_genEigenspace h, h', inf_top_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K ↥p)
    (⨆ (μ : K), (genEigenspace (LinearMap.restrict f h) μ : (a : ℕ∞) → Submodule K ↥p) k) ⊤
have this : Submodule.comap p.subtype p =
  Submodule.comap p.subtype (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
Tactic: have := congr_arg (Submodule.comap p.subtype) (Submodule.eq_iSup_inf_genEigenspace k h h')
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) ⊤
this :
  Submodule.comap p.subtype p =
    Submodule.comap p.subtype (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
⊢ Eq.{u_2 + 1} (α := Submodule K ↥p)
    (⨆ (μ : K), (genEigenspace (LinearMap.restrict f h) μ : (a : ℕ∞) → Submodule K ↥p) k) ⊤
have h_inj : Injective (α := ↥p) (β := V) (⇑p.subtype : (a : ↥p) → V)
Tactic: have h_inj : Function.Injective p.subtype := Subtype.coe_injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
k : ℕ∞
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
h' : Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) ⊤
this :
  Submodule.comap p.subtype p =
    Submodule.comap p.subtype (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
h_inj : Injective (α := ↥p) (β := V) (⇑p.subtype : (a : ↥p) → V)
⊢ Eq.{u_2 + 1} (α := Submodule K ↥p)
    (⨆ (μ : K), (genEigenspace (LinearMap.restrict f h) μ : (a : ℕ∞) → Submodule K ↥p) k) ⊤
have this₁ : Eq.{u_2 + 1} (α := Submodule K ↥p) ⊤
  (⨆ (i : K), (genEigenspace (LinearMap.restrict f h) i : (a : ℕ∞) → Submodule K ↥p) k)
Tactic: simp_rw [Submodule.inf_genEigenspace f p h, Submodule.comap_subtype_self,
    ← Submodule.map_iSup, Submodule.comap_map_eq_of_injective h_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
φ : End R M
h : IsNilpotent φ
⊢ LinearMap.charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
have rw : LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (finrank R M) = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
φ : End R M
h : IsNilpotent φ
⊢ LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (finrank R M) = 0
have h₁ : IsNilpotent (LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (finrank R M))
Tactic: apply IsNilpotent.eq_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent (LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (finrank R M))
have h₁ : IsNilpotent (LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (Fintype.card.{u_3} (ChooseBasisIndex R M)))
Tactic: rw [finrank_eq_card_chooseBasisIndex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
φ : End R M
h : IsNilpotent φ
⊢ IsNilpotent (LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (Fintype.card.{u_3} (ChooseBasisIndex R M)))
have h₁ : IsNilpotent (R := Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
  ((LinearMap.toMatrix (chooseBasis R M) (chooseBasis R M) :
        (a : M →ₗ[R] M) → Matrix (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
      φ :
    Matrix.{u_3, u_3, u_1} (ChooseBasisIndex R M) (ChooseBasisIndex R M) R)
Tactic: apply Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
φ : End R M
h : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
⊢ φ ^ finrank R M = 0
have rw : Eq.{u_3 + 1} (α := End R M) ((aeval φ : (a : R[X]) → End R M) (HPow.hPow (α := R[X]) X (finrank R M)) : End R M)
  (0 : End R M)
Tactic: rw [← @aeval_X_pow R, ← h, aeval_self_charpoly φ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
φ : End R M
h : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
rw :
  Eq.{u_3 + 1} (α := End R M) ((aeval φ : (a : R[X]) → End R M) (HPow.hPow (α := R[X]) X (finrank R M)) : End R M)
    (0 : End R M)
⊢ φ ^ finrank R M = 0
have rw₁ : Eq.{u_3 + 1} (α := End R M) ((aeval φ : (a : R[X]) → End R M) (charpoly φ) : End R M) (0 : End R M)
Tactic: rw [← @aeval_X_pow R, ← h, aeval_self_charpoly φ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
φ : End R M
h : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
rw :
  Eq.{u_3 + 1} (α := End R M) ((aeval φ : (a : R[X]) → End R M) (HPow.hPow (α := R[X]) X (finrank R M)) : End R M)
    (0 : End R M)
rw₁ : Eq.{u_3 + 1} (α := End R M) ((aeval φ : (a : R[X]) → End R M) (charpoly φ) : End R M) (0 : End R M)
⊢ φ ^ finrank R M = 0
have rw₂ : Eq.{u_3 + 1} (α := End R M) 0 0
Tactic: rw [← @aeval_X_pow R, ← h, aeval_self_charpoly φ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
⊢ [IsNilpotent φ, charpoly φ = HPow.hPow (α := R[X]) X (finrank R M),
      ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M),
      (charpoly φ).natTrailingDegree = finrank R M].TFAE
have tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
Tactic: tfae_have 1 → 2 := IsNilpotent.charpoly_eq_X_pow_finrank
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
h : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
m : M
⊢ ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
have h₁ : Eq (α := M) ((φ ^ finrank R M : (a : M) → M) m : M) (0 : M)
Tactic: use finrank R M
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
h : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
m : M
⊢ Eq (α := M) ((φ ^ finrank R M : (a : M) → M) m : M) (0 : M)
have h₁ : φ ^ finrank R M = 0
Tactic: suffices φ ^ finrank R M = 0 by simp only [this, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (hypothesis)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
⊢ [IsNilpotent φ, charpoly φ = HPow.hPow (α := R[X]) X (finrank R M),
      ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M),
      (charpoly φ).natTrailingDegree = finrank R M].TFAE
have tfae_2_to_3 : ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
  ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
Tactic: tfae_have 2 → 3
  | h, m => by
    use finrank R M
    suffices φ ^ finrank R M = 0 by simp only [this, LinearMap.zero_apply]
    simpa only [h, map_pow, aeval_X] using φ.aeval_self_charpoly
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h_1 : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M) := h_1
⊢ IsNilpotent φ
have obtain : ∀ (n : ℕ) (hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker), IsNilpotent φ
Tactic: obtain ⟨n, hn⟩ := Filter.eventually_atTop.mp <| φ.eventually_iSup_ker_pow_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h_1 : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M) := h_1
n : ℕ
hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker
⊢ IsNilpotent φ
have h₁ : φ ^ n = 0
Tactic: use n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h_1 : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M) := h_1
n : ℕ
hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker
⊢ φ ^ n = 0
have h₁ : ∀ (x : M), Eq (α := M) ((φ ^ n : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Zero (goal)
Goal:
R : Type u_1
M : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Free R M
inst_6 : IsNoetherian R M
φ : End R M
tfae_1_to_2 : ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)
tfae_2_to_3 :
  ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h_1 : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)
h : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M) := h_1
n : ℕ
hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker
x : M
⊢ Eq (α := M) ((φ ^ n : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
have h₁ : Membership.mem (γ := Submodule R M) (⨆ (m : ℕ), (φ ^ m).ker) x
Tactic: rw [zero_apply, ← mem_ker, ← hn n le_rfl]