awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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
set :
  let p : Submodule R M :=
    (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓
      (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞);
  p = ⊥
⊢ 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:
set p := f.genEigenspace μ₁ k ⊓ f.genEigenspace μ₂ l

Premises used: Nat.cast, Module.End.genEigenspace, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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 : ℕ∞)
by_contra : ∀ (hp : ¬p = ⊥), False
⊢ p = ⊥

Tactic:
by_contra hp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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 = ⊥
⊢ Nontrivial.{w} ↥p

Tactic:
replace hp : Nontrivial p := Submodule.nontrivial_iff_ne_bot.mpr hp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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)
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)) ⋯)
⊢ IsNilpotent (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 _)

Premises used: inf_le_right, inf_le_left, Module.End.isNilpotent_restrict_of_le, Commute.isNilpotent_sub
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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_1 : 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)) ⋯
h : ∀ (x : ↥p), Eq.{w + 1} (α := M) (↑((f₂ * f₁ : (a : ↥p) → ↥p) x) : M) (↑((f₁ * f₂ : (a : ↥p) → ↥p) x) : M)
⊢ Commute f₂ f₁

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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)) ⋯
x : ↥p
⊢ Eq.{w + 1} (α := M) (↑((f₂ * f₁ : (a : ↥p) → ↥p) x) : M) (↑((f₁ * f₂ : (a : ↥p) → ↥p) x) : M)

Tactic:
simp [f₁, f₂, smul_sub, sub_sub, smul_comm μ₁, add_sub_left_comm]

Premises used: add_sub_left_comm, sub_sub, smul_sub, SMulCommClass.smul_comm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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)) ⋯
⊢ 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 mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)

Premises used: Module.End.mapsTo_genEigenspace_of_comm, Algebra.mul_sub_algebraMap_commutes
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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 (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)) ⋯)

Tactic:
apply isNilpotent_restrict_genEigenspace_nat

Premises used: Module.End.isNilpotent_restrict_genEigenspace_nat, Module.End.mapsTo_genEigenspace_of_comm, Algebra.mul_sub_algebraMap_commutes, Nat.cast
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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)) ⋯
⊢ 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 mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)

Premises used: Module.End.mapsTo_genEigenspace_of_comm, Algebra.mul_sub_algebraMap_commutes
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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 (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)) ⋯)

Tactic:
apply isNilpotent_restrict_genEigenspace_nat

Premises used: Module.End.isNilpotent_restrict_genEigenspace_nat, Module.End.mapsTo_genEigenspace_of_comm, Algebra.mul_sub_algebraMap_commutes, Nat.cast
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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₁)

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
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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_1 : 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₁)
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)
⊢ f₂ - f₁ = (algebraMap R (End R ↥p) : (a : R) → End R ↥p) (μ₁ - μ₂)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
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₁)
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:
simp [f₁, f₂]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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) (μ₁ - μ₂)

Tactic:
have hf₁₂ : f₂ - f₁ = algebraMap R (End R p) (μ₁ - μ₂) := by ext; simp [f₁, f₂]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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₁)
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p) : (a : R) → End R ↥p) (μ₁ - μ₂)
⊢ μ₁ = μ₂

Tactic:
rw [hf₁₂, IsNilpotent.map_iff (FaithfulSMul.algebraMap_injective R (End R p)),
    isNilpotent_iff_eq_zero, sub_eq_zero] at this

Premises used: sub_eq_zero, Membership.mem, Subtype, isNilpotent_iff_eq_zero, FaithfulSMul.algebraMap_injective, IsNilpotent.map_iff, Module.End
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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₁)
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p) : (a : R) → End R ↥p) (μ₁ - μ₂)
this₁ : μ₁ = μ₂
⊢ f₂ - f₁ = (algebraMap R (End R ↥p) : (a : R) → End R ↥p) (μ₁ - μ₂)

Tactic:
rw [hf₁₂, IsNilpotent.map_iff (FaithfulSMul.algebraMap_injective R (End R p)),
    isNilpotent_iff_eq_zero, sub_eq_zero] at this

Premises used: sub_eq_zero, Membership.mem, Subtype, isNilpotent_iff_eq_zero, FaithfulSMul.algebraMap_injective, IsNilpotent.map_iff, Module.End
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : 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 : μ₁ = μ₂
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p) : (a : R) → End R ↥p) (μ₁ - μ₂)
⊢ False

Tactic:
contradiction
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
h :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₁
μ₂ : R
hμ₂ :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₂
hμ₁₂ :
  Eq.{w + 1} (α := Submodule R M)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₁)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₂)
by_contra : ∀ (contra : ¬μ₁ = μ₂), False
⊢ μ₁ = μ₂

Tactic:
by_contra contra
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
h :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₁
μ₂ : R
hμ₂ :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₂
hμ₁₂ :
  Eq.{w + 1} (α := Submodule R M)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₁)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₂)
contra : ¬μ₁ = μ₂
apply : Eq (α := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
⊢ False

Tactic:
apply hμ₂
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : R
h :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₁
μ₂ : R
hμ₂ :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₂
hμ₁₂ :
  Eq.{w + 1} (α := Submodule R M)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₁)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₂)
contra : ¬μ₁ = μ₂
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)

Tactic:
simpa only [hμ₁₂, disjoint_self] using f.disjoint_genEigenspace contra k k

Premises used: Module.End.disjoint_genEigenspace, disjoint_self
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
⊢ InjOn.{v, w} (β := Submodule R M) (fun (x : R) ↦ f.maxGenEigenspace x) {μ : R | f.maxGenEigenspace μ ≠ ⊥}

Tactic:
injOn_genEigenspace f ⊤

Premises used: setOf, Module.End.injOn_genEigenspace, Top.top
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
this :
  ∀ (μ₁ : R) (s : Finset R),
    μ₁ ∉ s →
      Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
        (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
simp_rw :
  ∀ (s : Finset R),
    ∀ i ∈ s,
      Disjoint (α := Submodule R M) ((f.genEigenspace i : (a : ℕ∞) → Submodule R M) k : Submodule R M)
        ((s.erase i).sup fun (x : R) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)
⊢ iSupIndep.{v + 1, w} (α := Submodule R M) fun (x : R) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule R M) k

Tactic:
simp_rw [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase]

Premises used: Finset.supIndep_iff_disjoint_erase, iSupIndep_iff_supIndep
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
this :
  ∀ (μ₁ : R) (s : Finset R),
    μ₁ ∉ s →
      Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
        (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
⊢ ∀ (s : Finset R),
    ∀ i ∈ s,
      Disjoint (α := Submodule R M) ((f.genEigenspace i : (a : ℕ∞) → Submodule R M) k : Submodule R M)
        ((s.erase i).sup fun (x : R) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)

Tactic:
fun s μ _ ↦ this _ _ (s.notMem_erase μ)

Premises used: Finset.notMem_erase, Finset.erase