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

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
⊢ (g ^ l) (y + z) ∈ ↑(s.sup fun μ => (f.genEigenspace μ) k)

Tactic:
rw [SetLike.mem_coe, map_add, hl, zero_add]

Result:
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
⊢ (g ^ l) z ∈ 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 : ℕ∞
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)

Tactic:
exact fun s μ _ ↦ this _ _ (s.not_mem_erase μ)

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
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

Tactic:
exact ⟨hx, this⟩

Result:
no goals

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 : ((f - μ₂ • 1) ^ l) y = 0
hyz : (g ^ l) (y + z) ∈ (f.genEigenspace μ₁) k ⊓ s.sup fun μ => (f.genEigenspace μ) k
⊢ y + z ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)

Tactic:
rwa [ih.eq_bot, Submodule.mem_bot] at hyz

Result:
no goals

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

Tactic:
exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l

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 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, ∃ (_ : ↑l ≤ k), y + z ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)

Tactic:
peel hy with l hlk 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 : y ∈ LinearMap.ker ((f - μ₂ • 1) ^ l)
⊢ y + z ∈ LinearMap.ker ((f - μ₂ • 1) ^ 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
k : ℕ∞
⊢ ∀ (μ₁ : R) (s : Finset R), μ₁ ∉ s → Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ => (f.genEigenspace μ) k)

Tactic:
intro μ₁ s

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:
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

Tactic:
simp_rw [mem_genEigenspace, ← exists_prop] at hy ⊢

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 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, ∃ (_ : ↑l ≤ k), y + z ∈ LinearMap.ker ((f - μ₂ • 1) ^ 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
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
this : Submodule.map (g ^ l) (s.sup fun μ => (f.genEigenspace μ) k) ≤ s.sup fun μ => (f.genEigenspace μ) k
⊢ (g ^ l) z ∈ s.sup fun μ => (f.genEigenspace μ) k

Tactic:
exact this (Submodule.mem_map_of_mem hz)

Result:
no goals