-- Mathlib/LinearAlgebra/Eigenspace/Pi.lean
lemma independent_iInf_maxGenEigenspace_of_forall_mapsTo
    (h : ∀ i j φ, MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ)) :
    iSupIndep fun χ : ι → R ↦ ⨅ i, (f i).maxGenEigenspace (χ i)

Proof state:
case insert.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
χ : ι → R
x✝ : χ ∈ s
u : M
hu : u ∈ ↑(⨅ i, (f i).maxGenEigenspace (χ i))
⊢ MapsTo ⇑(f l) ↑(⨅ i, (f i).maxGenEigenspace (χ i)) ↑(⨅ i, (f i).maxGenEigenspace (χ i))

Tactic:
simp only [Submodule.iInf_coe]

Result:
case insert.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
k : ℕ
hk : (g ^ k) y = 0
aux :
  ∀ (f : End R M) (φ : R) (k : ℕ) (p : Submodule R M),
    MapsTo ⇑f ↑p ↑p → MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p
χ : ι → R
x✝ : χ ∈ s
u : M
hu : u ∈ ↑(⨅ i, (f i).maxGenEigenspace (χ i))
⊢ MapsTo (⇑(f l)) (⋂ i, ↑((f i).maxGenEigenspace (χ i))) (⋂ i, ↑((f i).maxGenEigenspace (χ i)))

Proof state:
case insert.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
⊢ ∃ k,
    ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)

Tactic:
let g : Module.End R M := f l - algebraMap R (Module.End R M) (χ₂ l)

Result:
case insert.intro.intro.intro.intro.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h : ∀ (l : ι) (χ : ι → R), MapsTo (⇑(f l)) (⨅ i, ↑((f i).maxGenEigenspace (χ i))) (⨅ i, ↑((f i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i))
y : M
hy : y ∈ ⨅ i, (f i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f l - (algebraMap R (End R M)) (χ₂ l)
⊢ ∃ k,
    ((f l - (algebraMap R (End R M)) (χ₂ l)) ^ k) (y + z) ∈
      (⨅ i, (f i).maxGenEigenspace (χ₁ i)) ⊓ s.sup fun χ => ⨅ i, (f i).maxGenEigenspace (χ i)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f✝ : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (⇑(f✝ l)) (⨅ i, ↑((f✝ i).maxGenEigenspace (χ i))) (⨅ i, ↑((f✝ i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f✝ i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f✝ i).maxGenEigenspace (χ i))
y : M
hy : y ∈ ⨅ i, (f✝ i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ => ⨅ i, (f✝ i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f✝ i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f✝ l - (algebraMap R (End R M)) (χ₂ l)
k✝ : ℕ
hk : (g ^ k✝) y = 0
f : End R M
φ : R
k : ℕ
p : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
⊢ MapsTo ⇑((f - (algebraMap R (End R M)) φ) ^ k) ↑p ↑p

Tactic:
rw [LinearMap.coe_pow]

Result:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
f✝ : ι → End R M
inst✝ : NoZeroSMulDivisors R M
h :
  ∀ (l : ι) (χ : ι → R),
    MapsTo (⇑(f✝ l)) (⨅ i, ↑((f✝ i).maxGenEigenspace (χ i))) (⨅ i, ↑((f✝ i).maxGenEigenspace (χ i)))
χ₁ χ₂ : ι → R
s : Finset (ι → R)
_n : χ₂ ∉ s
hχ₁₂✝ : χ₁ ∉ insert χ₂ s
hχ₁₂ : χ₁ ≠ χ₂
hχ₁ : χ₁ ∉ s
ih : Disjoint (⨅ i, (f✝ i).maxGenEigenspace (χ₁ i)) (s.sup fun χ => ⨅ i, (f✝ i).maxGenEigenspace (χ i))
y : M
hy : y ∈ ⨅ i, (f✝ i).maxGenEigenspace (χ₂ i)
z : M
hz : z ∈ s.sup fun χ => ⨅ i, (f✝ i).maxGenEigenspace (χ i)
hx : y + z ∈ ⨅ i, (f✝ i).maxGenEigenspace (χ₁ i)
l : ι
g : End R M := f✝ l - (algebraMap R (End R M)) (χ₂ l)
k✝ : ℕ
hk : (g ^ k✝) y = 0
f : End R M
φ : R
k : ℕ
p : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
⊢ MapsTo (⇑(f - (algebraMap R (End R M)) φ))^[k] ↑p ↑p