-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem independent_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) :
    iSupIndep (f.genEigenspace · 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 ∈ (f.genEigenspace μ₂) k

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'

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
hx' : y + z ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ => (f.genEigenspace μ) k
⊢ 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 : ℕ∞
⊢ iSupIndep fun x => (f.genEigenspace x) k

Tactic:
suffices ∀ μ₁ (s : Finset R), μ₁ ∉ s → Disjoint (f.genEigenspace μ₁ k)
  (s.sup fun μ ↦ f.genEigenspace μ k) by
  simp_rw [iSupIndep_iff_supIndep_of_injOn (injOn_genEigenspace f k),
    Finset.supIndep_iff_disjoint_erase]
  exact fun s μ _ ↦ this _ _ (s.not_mem_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 : ℕ∞
⊢ ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (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
ih : μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
hμ₁₂ : μ₁ ∉ insert μ₂ s
⊢ ?m.486544

Tactic:
rwa [Finset.mem_insert, not_or] at hμ₁₂

Result:
no goals

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
hx' : y + z ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ => (f.genEigenspace μ) k
⊢ y + z ∈ (f.genEigenspace μ₂) k

Tactic:
clear hx'

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
⊢ y + z ∈ (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
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)

Tactic:
specialize ih 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
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)
⊢ Disjoint ((f.genEigenspace μ₁) k) ((insert μ₂ s).sup fun μ => (f.genEigenspace μ) k)

Proof state:
case empty
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
⊢ μ₁ ∉ ∅ → Disjoint ((f.genEigenspace μ₁) k) (∅.sup fun μ => (f.genEigenspace μ) k)

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
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
⊢ Commute f (g ^ l)

Tactic:
exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l

Result:
no goals

Proof state:
case refine_2
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
μ : R
x✝ : μ ∈ s
⊢ Submodule.map (g ^ l) ((f.genEigenspace μ) k) ≤ (f.genEigenspace μ) k

Tactic:
rintro - ⟨u, hu, rfl⟩

Result:
case refine_2.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 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
μ : R
x✝ : μ ∈ s
u : M
hu : u ∈ ↑((f.genEigenspace μ) k)
⊢ (g ^ l) u ∈ (f.genEigenspace μ) k