-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma disjoint_genEigenspace [NoZeroSMulDivisors R M]
    (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) (k l : ℕ∞) :
    Disjoint (f.genEigenspace μ₁ k) (f.genEigenspace μ₂ l)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this✝ : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
this : IsNilpotent (f₂ - f₁)
⊢ f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)

Tactic:
ext

Result:
case h.a
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this✝ : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
this : IsNilpotent (f₂ - f₁)
x✝ : ↥p
⊢ ↑((f₂ - f₁) x✝) = ↑(((algebraMap R (End R ↥p)) (μ₁ - μ₂)) x✝)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
⊢ ∀ (i : { l // ↑l ≤ k }) (i_1 : { l_1 // ↑l_1 ≤ l }), Disjoint ((f.genEigenspace μ₁) ↑↑i) ((f.genEigenspace μ₂) ↑↑i_1)

Tactic:
rintro ⟨k, -⟩ ⟨l, -⟩

Result:
case mk.mk
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
⊢ Disjoint ((f.genEigenspace μ₁) ↑↑⟨k, property✝¹⟩) ((f.genEigenspace μ₂) ↑↑⟨l, property✝⟩)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
⊢ MapsTo ⇑(f - (algebraMap R (End R M)) μ₁) ↑((f.genEigenspace μ₁) ↑k) ↑((f.genEigenspace μ₁) ↑k)

R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ?m.446472)

Tactic:
apply mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f _)

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
⊢ IsNilpotent (LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯)

Proof state:
case h.a
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this✝ : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
this : IsNilpotent (f₂ - f₁)
x✝ : ↥p
⊢ ↑((f₂ - f₁) x✝) = ↑(((algebraMap R (End R ↥p)) (μ₁ - μ₂)) x✝)

Tactic:
simp [f₁, f₂, sub_smul]

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this✝ : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
this : μ₁ = μ₂
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p)) (μ₁ - μ₂)
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
case h.a
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
f₁ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₁) ⋯
f₂ : End R ↥p := LinearMap.restrict (f - (algebraMap R (End R M)) μ₂) ⋯
x✝ : ↥p
⊢ ↑((f₂ * f₁) x✝) = ↑((f₁ * f₂) x✝)

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

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
⊢ Disjoint (⨆ l, (f.genEigenspace μ₁) ↑↑l) (⨆ l_1, (f.genEigenspace μ₂) ↑↑l_1)

Tactic:
simp_rw [genEigenspace_directed.disjoint_iSup_left, genEigenspace_directed.disjoint_iSup_right]

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
⊢ ∀ (i : { l // ↑l ≤ k }) (i_1 : { l_1 // ↑l_1 ≤ l }), Disjoint ((f.genEigenspace μ₁) ↑↑i) ((f.genEigenspace μ₂) ↑↑i_1)

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : ¬p = ⊥
⊢ False

Tactic:
replace hp : Nontrivial p := Submodule.nontrivial_iff_ne_bot.mpr hp

Result:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
this : IsReduced R
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
⊢ False