-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem independent_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) :
    iSupIndep (f.genEigenspace · k)

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
k : ℕ∞
this : ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
⊢ iSupIndep fun x => (f.genEigenspace x) k

Tactic:
simp_rw [iSupIndep_iff_supIndep_of_injOn (injOn_genEigenspace f k),
  Finset.supIndep_iff_disjoint_erase]

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
k : ℕ∞
this : ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
⊢ ∀ (s : Finset R), ∀ i ∈ s, Disjoint ((f.genEigenspace i) k) ((s.erase i).sup fun x => (f.genEigenspace x) k)

Proof state:
case insert.intro.intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
x : M
hx : x ∈ ↑((f.genEigenspace μ₁) k)
hx' : x ∈ ↑((f.genEigenspace μ₂) k ⊔ s.sup fun μ => (f.genEigenspace μ) k)
⊢ x = 0

Tactic:
simp only [SetLike.mem_coe] at hx hx'

Result:
case insert.intro.intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
x : M
hx : x ∈ (f.genEigenspace μ₁) k
hx' : x ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ => (f.genEigenspace μ) k
⊢ x = 0

Proof state:
case insert.intro.intro.intro.intro.intro.intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
y : M
hy : y ∈ (f.genEigenspace μ₂) k
z : M
hz : z ∈ s.sup fun μ => (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
⊢ y + z ∈ (f.genEigenspace μ₂) k

Tactic:
let g := f - μ₂ • 1

Result:
case insert.intro.intro.intro.intro.intro.intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
y : M
hy : y ∈ (f.genEigenspace μ₂) k
z : M
hz : z ∈ s.sup fun μ => (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
⊢ y + z ∈ (f.genEigenspace μ₂) k

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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
x : M
hx : x ∈ (f.genEigenspace μ₁) k
hx' : x ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ => (f.genEigenspace μ) k
this : x ∈ (f.genEigenspace μ₂) k
⊢ x = 0

Tactic:
rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]

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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
x : M
hx : x ∈ (f.genEigenspace μ₁) k
hx' : x ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ => (f.genEigenspace μ) k
this : x ∈ (f.genEigenspace μ₂) k
⊢ x ∈ (f.genEigenspace μ₁) k ⊓ (f.genEigenspace μ₂) k

Proof state:
case insert.intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
⊢ ∀ x ∈ (f.genEigenspace μ₁) k ⊓ ((f.genEigenspace μ₂) k ⊔ s.sup fun μ => (f.genEigenspace μ) k), x = 0

Tactic:
rintro x ⟨hx, hx'⟩

Result:
case insert.intro.intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
x : M
hx : x ∈ ↑((f.genEigenspace μ₁) k)
hx' : x ∈ ↑((f.genEigenspace μ₂) k ⊔ s.sup fun μ => (f.genEigenspace μ) k)
⊢ x = 0

Proof state:
case insert.intro.intro.intro.intro.intro.intro.h.h
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
y z : M
hz : z ∈ s.sup fun μ => (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)
l : ℕ
hlk : ↑l ≤ k
hl : y ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)
⊢ y + z ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)

Tactic:
simp only [mem_genEigenspace_nat, LinearMap.mem_ker] at hl

Result:
case insert.intro.intro.intro.intro.intro.intro.h.h
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
y z : M
hz : z ∈ s.sup fun μ => (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ∃ (_ : ↑l ≤ k), y ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ₂ • 1) ^ l) y = 0
⊢ y + z ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)

Proof state:
case insert
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
hμ₁₂ : μ₁ ∉ insert μ₂ s
⊢ Disjoint ((f.genEigenspace μ₁) k) ((insert μ₂ s).sup fun μ => (f.genEigenspace μ) k)

Tactic:
obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂

Result:
case insert.intro
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
⊢ Disjoint ((f.genEigenspace μ₁) k) ((insert μ₂ s).sup fun μ => (f.genEigenspace μ) k)