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 : 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)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
have induction : ∀ ⦃x : M⦄ (hk : (↑0 : ℕ∞) ≤ n)
  (hx : Eq (α := M) ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) x : M) (0 : M)),
  Eq (α := M) ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) ((f : (a : M) → M) x : M) : M)
    (0 : M)
Tactic: induction k generalizing x
Cleared hypotheses: x, k, hk, 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)
induction :
  ∀ ⦃x : M⦄ (hk : (↑0 : ℕ∞) ≤ n)
    (hx : Eq (α := M) ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) x : M) (0 : M)),
    Eq (α := M)
      ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
have succ : ∀ (n_1 : ℕ),
  (∀ ⦃x : M⦄ (hk : (↑n_1 : ℕ∞) ≤ n)
      (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ n_1 : (a : M) → M) x : M) (0 : M)),
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ n_1 : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)) →
    ∀ ⦃x : M⦄ (hk : (↑(n_1 + 1) : ℕ∞) ≤ n)
      (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ (n_1 + 1) : (a : M) → M) x : M) (0 : M)),
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ (n_1 + 1) : (a : M) → M) ((f : (a : M) → M) x : M) : M)
        (0 : M)
Tactic: induction k generalizing x
Cleared hypotheses: x, k, hk, 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 : ℕ∞
k : ℕ
ih :
  ∀ ⦃x : M⦄ (hk : (↑k : ℕ∞) ≤ n)
    (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)),
    Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
x : M
hk : (↑(k + 1) : ℕ∞) ≤ n
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ (k + 1) : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ (k + 1) : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
have rw : ∀
  (hx :
    Eq (α := M)
      (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
          ((f - HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) x : M) :
        M)
      (0 : M)),
  Eq (α := M)
    (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
        ((f - HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) ((f : (a : M) → M) x : M) : M) :
      M)
    (0 : M)
Tactic: rw [pow_succ, mul_apply] 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
⊢ LinearMap.restrict f ⋯ = HSMul.hSMul (β := ↥(f.eigenspace μ) →ₗ[R] ↥(f.eigenspace μ)) μ LinearMap.id
have h : ∀ (x : ↥(f.eigenspace μ)),
  Eq.{w + 1} (α := M) (↑((LinearMap.restrict f sorry : (a : ↥(f.eigenspace μ)) → ↥(f.eigenspace μ)) x) : M)
    (↑((HSMul.hSMul (β := ↥(f.eigenspace μ) →ₗ[R] ↥(f.eigenspace μ)) μ LinearMap.id :
            (a : ↥(f.eigenspace μ)) → ↥(f.eigenspace μ))
          x) :
      M)
Tactic: ext x
-- 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.maxGenEigenspace μ = (f - HSMul.hSMul (β := End R M) μ 1).maxGenEigenspace 0
have h : ∀ (x : M), x ∈ f.maxGenEigenspace μ ↔ x ∈ (f - HSMul.hSMul (β := End R M) μ 1).maxGenEigenspace 0
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ f.maxGenEigenspace μ = (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
have apply : 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: apply le_antisymm _ <| (f.genEigenspace μ).monotone le_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ 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)
have 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)
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
inst_3 : IsNoetherian R M
f : End R M
μ : R
h :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
⊢ IsNilpotent
    (LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) h)
have apply : f.maxGenEigenspace μ ≤ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞)
Tactic: apply isNilpotent_restrict_of_le (q := f.genEigenspace μ (maxUnifEigenspaceIndex f μ))
    _ (isNilpotent_restrict_genEigenspace_nat f μ (maxUnifEigenspaceIndex f μ))
-- 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 (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
⊢ f.maxGenEigenspace μ ≤ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞)
have rw : LE.le (α := Submodule R M)
  ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxGenEigenspaceIndex μ) : ℕ∞) : Submodule R M)
  ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxGenEigenspaceIndex μ) : ℕ∞) : Submodule R M)
Tactic: rw [maxGenEigenspace_eq]
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
⊢ Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) l : Submodule R M)
have rw : Disjoint.{w} (α := Submodule R M)
  (⨆ (l : { l : ℕ // (↑l : ℕ∞) ≤ k }), (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑(↑l : ℕ) : ℕ∞))
  (⨆ (l_1 : { l_1 : ℕ // (↑l_1 : ℕ∞) ≤ l }), (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑(↑l_1 : ℕ) : ℕ∞))
Tactic: rw [genEigenspace_eq_iSup_genEigenspace_nat, genEigenspace_eq_iSup_genEigenspace_nat]
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
⊢ Disjoint.{w} (α := Submodule R M)
    (⨆ (l : { l : ℕ // (↑l : ℕ∞) ≤ k }), (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑(↑l : ℕ) : ℕ∞))
    (⨆ (l_1 : { l_1 : ℕ // (↑l_1 : ℕ∞) ≤ l }), (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑(↑l_1 : ℕ) : ℕ∞))
have simp_rw : ∀ (i : { l : ℕ // (↑l : ℕ∞) ≤ k }) (i_1 : { l_1 : ℕ // (↑l_1 : ℕ∞) ≤ l }),
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑(↑i : ℕ) : ℕ∞) : Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑(↑i_1 : ℕ) : ℕ∞) : Submodule R M)
Tactic: simp_rw [genEigenspace_directed.disjoint_iSup_left, genEigenspace_directed.disjoint_iSup_right]
-- 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
⊢ Disjoint (α := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M)
        (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ k_1) k property) : ℕ) : ℕ∞) :
      Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M)
        (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ l_1) l property_1) : ℕ) : ℕ∞) :
      Submodule R M)
have a : Nontrivial M
Tactic: nontriviality M
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
⊢ Disjoint (α := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M)
        (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ k_1) k property) : ℕ) : ℕ∞) :
      Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M)
        (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ l_1) l property_1) : ℕ) : ℕ∞) :
      Submodule R M)
have rw : Eq (α := Submodule R M)
  ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M)
        (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ k_1) k property) : ℕ) : ℕ∞) ⊓
      (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M)
        (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ l_1) l property_1) : ℕ) : ℕ∞) :
    Submodule R M)
  (⊥ : Submodule R M)
Tactic: rw [disjoint_iff]
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
⊢ Eq (α := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M)
          (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ k_1) k property) : ℕ) : ℕ∞) ⊓
        (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M)
          (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ l_1) l property_1) : ℕ) : ℕ∞) :
      Submodule R M)
    (⊥ : Submodule R M)
have set : let p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞);
p = ⊥
Tactic: set p := f.genEigenspace μ₁ k ⊓ f.genEigenspace μ₂ l
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
⊢ p = ⊥
have by_contra : ∀ (hp : ¬p = ⊥), False
Tactic: by_contra hp
-- 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : ¬p = ⊥
⊢ False
have hp₁ : Nontrivial.{w} ↥p
Tactic: replace hp : Nontrivial p := Submodule.nontrivial_iff_ne_bot.mpr hp
Cleared hypotheses: hp
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
⊢ IsNilpotent (f₂ - f₁)
have apply : Commute f₂ f₁
Tactic: apply Commute.isNilpotent_sub (x := f₂) (y := f₁) _
      (isNilpotent_restrict_of_le inf_le_right _)
      (isNilpotent_restrict_of_le inf_le_left _)
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
apply : Commute f₂ f₁
⊢ IsNilpotent (f₂ - f₁)
have apply₁ : MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) : (a : M) → M)
  (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) : Set M)
  (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) : Set M)
Tactic: apply Commute.isNilpotent_sub (x := f₂) (y := f₁) _
      (isNilpotent_restrict_of_le inf_le_right _)
      (isNilpotent_restrict_of_le inf_le_left _)
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
apply : Commute f₂ f₁
apply₁ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) : (a : M) → M)
    (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) : Set M)
⊢ IsNilpotent (f₂ - f₁)
have apply₂ : IsNilpotent (R :=
  ↥((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) →ₗ[R]
    ↥((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M))
  (LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) sorry)
Tactic: apply Commute.isNilpotent_sub (x := f₂) (y := f₁) _
      (isNilpotent_restrict_of_le inf_le_right _)
      (isNilpotent_restrict_of_le inf_le_left _)
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
apply : Commute f₂ f₁
apply₁ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) : (a : M) → M)
    (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) : Set M)
apply₂ :
  IsNilpotent (R :=
    ↥((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) →ₗ[R]
      ↥((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M))
    (LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯)
⊢ IsNilpotent (f₂ - f₁)
have apply₃ : MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) : (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)
Tactic: apply Commute.isNilpotent_sub (x := f₂) (y := f₁) _
      (isNilpotent_restrict_of_le inf_le_right _)
      (isNilpotent_restrict_of_le inf_le_left _)
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
apply : Commute f₂ f₁
apply₁ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) : (a : M) → M)
    (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) : Set M)
apply₂ :
  IsNilpotent (R :=
    ↥((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) →ₗ[R]
      ↥((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M))
    (LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯)
apply₃ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) : (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 (f₂ - f₁)
have apply₄ : IsNilpotent (R :=
  ↥((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) →ₗ[R]
    ↥((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M))
  (LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) sorry)
Tactic: apply Commute.isNilpotent_sub (x := f₂) (y := f₁) _
      (isNilpotent_restrict_of_le inf_le_right _)
      (isNilpotent_restrict_of_le inf_le_left _)
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
⊢ Commute f₂ f₁
have h : ∀ (x : ↥p), Eq.{w + 1} (α := M) (↑((f₂ * f₁ : (a : ↥p) → ↥p) x) : M) (↑((f₁ * f₂ : (a : ↥p) → ↥p) x) : M)
Tactic: ext
-- 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
⊢ False
have this : IsNilpotent (f₂ - f₁)
Tactic: have : IsNilpotent (f₂ - f₁) := by
    apply Commute.isNilpotent_sub (x := f₂) (y := f₁) _
      (isNilpotent_restrict_of_le inf_le_right _)
      (isNilpotent_restrict_of_le inf_le_left _)
    · ext; simp [f₁, f₂, smul_sub, sub_sub, smul_comm μ₁, add_sub_left_comm]
    · apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)
    · apply isNilpotent_restrict_genEigenspace_nat
    · apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)
    apply isNilpotent_restrict_genEigenspace_nat
-- 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 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
this : IsNilpotent (f₂ - f₁)
⊢ f₂ - f₁ = (algebraMap R (End R ↥p) : (a : R) → End R ↥p) (μ₁ - μ₂)
have h : ∀ (x : ↥p),
  Eq.{w + 1} (α := M) (↑((f₂ - f₁ : (a : ↥p) → ↥p) x) : M)
    (↑((((algebraMap R (End R ↥p) : (a : R) → End R ↥p) (μ₁ - μ₂) : End R ↥p) : (a : ↥p) → ↥p) x) : M)
Tactic: ext