awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
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)
⊢ 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₂⟩

Premises used: And.intro, Module.End.genEigenspace, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
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
pos pos₁ pos₂ pos₃ : y ∈ p
⊢ Membership.mem (α := V) p ((m : (a : K) → V) μ : V)

Tactic:
rwa [← hg₃ hy₁ hm₂ hy₂]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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 ⊓ ⊤
rw₂ rw₃ : p = p
⊢ p = ⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k

Tactic:
rw [← inf_iSup_genEigenspace h, h', inf_top_eq]

Premises used: inf_top_eq, Submodule.inf_iSup_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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) ⊤
⊢ 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')
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
⊢ Injective (α := ↥p) (β := V) (⇑p.subtype : (a : ↥p) → V)

Tactic:
have h_inj : Function.Injective p.subtype := Subtype.coe_injective
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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) ⊤
    (⨆ (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

Premises used: Submodule.map_iSup, Submodule.comap_map_eq_of_injective, Submodule.inf_genEigenspace, Submodule.comap_subtype_self
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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) ⊤
h_inj : Injective (α := ↥p) (β := V) (⇑p.subtype : (a : ↥p) → V)
this :
  Eq.{u_2 + 1} (α := Submodule K ↥p) ⊤
    (⨆ (i : K), (genEigenspace (LinearMap.restrict f h) i : (a : ℕ∞) → Submodule K ↥p) k)
⊢ Eq.{u_2 + 1} (α := Submodule K ↥p)
    (⨆ (μ : K), (genEigenspace (LinearMap.restrict f h) μ : (a : ℕ∞) → Submodule K ↥p) k) ⊤

Tactic:
this.symm

Premises used: Set.Mem, setOf, Eq.symm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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) ⊤
h_inj : Injective (α := ↥p) (β := V) (⇑p.subtype : (a : ↥p) → V)
this :
  Eq.{u_2 + 1} (α := Submodule K ↥p) ⊤
    (⨆ (i : K), (genEigenspace (LinearMap.restrict f h) i : (a : ℕ∞) → Submodule K ↥p) k)
⊢ Eq.{u_2 + 1} (α := Submodule K ↥p)
    (⨆ (μ : K), (genEigenspace (LinearMap.restrict f h) μ : (a : ℕ∞) → Submodule K ↥p) k) ⊤

Tactic:
exact this.symm

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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 φ
rw : LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (finrank R M) = 0
⊢ LinearMap.charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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 φ
h₁ : IsNilpotent (LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (finrank R M))
⊢ LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (finrank R M) = 0

Tactic:
apply IsNilpotent.eq_zero

Premises used: IsNilpotent.eq_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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 φ
h₁ : IsNilpotent (LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (Fintype.card.{u_3} (ChooseBasisIndex R M)))
⊢ IsNilpotent (LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (finrank R M))

Tactic:
rw [finrank_eq_card_chooseBasisIndex]

Premises used: Module.finrank_eq_card_chooseBasisIndex
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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 φ
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)
⊢ IsNilpotent (LinearMap.charpoly φ - HPow.hPow (α := R[X]) X (Fintype.card.{u_3} (ChooseBasisIndex R M)))

Tactic:
apply Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent

Premises used: Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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 (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:
h.map (LinearMap.toMatrixAlgEquiv (chooseBasis R M))

Premises used: IsNilpotent.map, LinearMap.toMatrixAlgEquiv, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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 (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:
exact h.map (LinearMap.toMatrixAlgEquiv (chooseBasis R M))

Premises used: IsNilpotent.map, LinearMap.toMatrixAlgEquiv, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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)
rw₂ rw₃ : Eq.{u_3 + 1} (α := End R M) 0 0
⊢ φ ^ finrank R M = 0

Tactic:
rw [← @aeval_X_pow R, ← h, aeval_self_charpoly φ]

Premises used: Polynomial.aeval_X_pow, LinearMap.aeval_self_charpoly
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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 φ

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
⊢ charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
⊢ ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
⊢ ∀ (a : IsNilpotent φ), charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)

Tactic:
tfae_have 1 → 2 := IsNilpotent.charpoly_eq_X_pow_finrank

Premises used: IsNilpotent.charpoly_eq_X_pow_finrank
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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)
⊢ charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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)
⊢ ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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)
⊢ ∀ (a : charpoly φ = HPow.hPow (α := R[X]) X (finrank R M)) (m : M),
    ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
h₁ : Eq (α := M) ((φ ^ finrank R M : (a : M) → M) m : M) (0 : M)
⊢ ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)

Tactic:
use finrank R M

Premises used: Module.finrank
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
this : φ ^ finrank R M = 0
⊢ Eq (α := M) ((φ ^ finrank R M : (a : M) → M) m : M) (0 : M)

Tactic:
simp only [this, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
h₁ : φ ^ finrank R M = 0
⊢ Eq (α := M) ((φ ^ finrank R M : (a : M) → M) m : M) (0 : M)

Tactic:
suffices φ ^ finrank R M = 0 by simp only [this, LinearMap.zero_apply]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
⊢ φ ^ finrank R M = 0

Tactic:
simpa only [h, map_pow, aeval_X] using φ.aeval_self_charpoly

Premises used: map_pow, LinearMap.aeval_self_charpoly, Polynomial.aeval_X
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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)
⊢ ∀ (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
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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)
⊢ ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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)
⊢ IsNilpotent φ

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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)
⊢ ∀ (a : ∀ (m : M), ∃ (n : ℕ), Eq (α := M) ((φ ^ n : (a : M) → M) m : M) (0 : M)), IsNilpotent φ

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
obtain : ∀ (n : ℕ) (hn : ∀ b ≥ n, ⨆ (m : ℕ), (φ ^ m).ker = (φ ^ b).ker), IsNilpotent φ
⊢ IsNilpotent φ

Tactic:
obtain ⟨n, hn⟩ := Filter.eventually_atTop.mp <| φ.eventually_iSup_ker_pow_eq

Premises used: LinearMap.eventually_iSup_ker_pow_eq, Iff.mp, Filter.eventually_atTop
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
h₁ : φ ^ n = 0
⊢ IsNilpotent φ

Tactic:
use n
-- Module: Mathlib.LinearAlgebra.Eigenspace.Zero
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
h₁ : ∀ (x : M), Eq (α := M) ((φ ^ n : (a : M) → M) x : M) ((0 : (a : M) → M) x : M)
⊢ φ ^ n = 0

Tactic:
ext x