-- Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
theorem inf_iSup_genEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ p) (k : ℕ∞) :
    p ⊓ ⨆ μ, f.genEigenspace μ k = ⨆ μ, p ⊓ f.genEigenspace μ k

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi => xi) ∈ p
hm₁ : (m.sum fun _i xi => xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ LinearMap.ker ((f - i • 1) ^ l i)
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ => (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ => mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
hg₃ : InjOn ⇑g ↑((f.genEigenspace μ) k)
⊢ SurjOn ⇑g ↑(p ⊓ (f.genEigenspace μ) k) ↑(p ⊓ (f.genEigenspace μ) k)

Tactic:
have : MapsTo g
    ↑(p ⊓ f.genEigenspace μ k) ↑(p ⊓ f.genEigenspace μ k) :=
  hg₁.inter_inter hg₂

Result:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi => xi) ∈ p
hm₁ : (m.sum fun _i xi => xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ LinearMap.ker ((f - i • 1) ^ l i)
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ => (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ => mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
hg₃ : InjOn ⇑g ↑((f.genEigenspace μ) k)
this : MapsTo ⇑g ↑(p ⊓ (f.genEigenspace μ) k) ↑(p ⊓ (f.genEigenspace μ) k)
⊢ SurjOn ⇑g ↑(p ⊓ (f.genEigenspace μ) k) ↑(p ⊓ (f.genEigenspace μ) k)

Proof state:
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi => xi) ∈ p
hm₁ : (m.sum fun _i xi => xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ LinearMap.ker ((f - i • 1) ^ l i)
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ => (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ => mμ) = g (m μ)
μ' : K
x✝ : μ' ∈ m.support.erase μ
this : MapsTo ⇑(f - (algebraMap K (End K V)) μ') ↑p ↑p
⊢ MapsTo (⇑(f - (algebraMap K (End K V)) μ'))^[l₀] ↑p ↑p

Tactic:
exact this.iterate l₀

Result:
no goals

Proof state:
case h
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi => xi) ∈ p
hm₁ : (m.sum fun _i xi => xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ LinearMap.ker ((f - i • 1) ^ l i)
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ => (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ => mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this✝ : iSupIndep fun x => (f.genEigenspace x) k
aux : ∀ μ' ∈ m.support.erase μ, (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k
this : (m.support.erase μ).SupIndep fun x => (f.genEigenspace x) k
⊢ (m.support.erase μ).SupIndep fun i => LinearMap.ker ((f - (algebraMap K (End K V)) i) ^ l₀)

Tactic:
apply this.antitone_fun

Result:
case h
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
k : ℕ∞
m : K →₀ V
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) k
hm₀ : (m.sum fun _i xi => xi) ∈ p
hm₁ : (m.sum fun _i xi => xi) ∈ ⨆ μ, (f.genEigenspace μ) k
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hlk : ∀ (i : K), ↑(l i) ≤ k
hl : ∀ (i : K), m i ∈ LinearMap.ker ((f - i • 1) ^ l i)
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ => (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ => mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)
this✝ : iSupIndep fun x => (f.genEigenspace x) k
aux : ∀ μ' ∈ m.support.erase μ, (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k
this : (m.support.erase μ).SupIndep fun x => (f.genEigenspace x) k
⊢ ∀ x ∈ m.support.erase μ, LinearMap.ker ((f - (algebraMap K (End K V)) x) ^ l₀) ≤ (f.genEigenspace x) k

Proof state:
case a.a
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
m : K →₀ V
hm₀ : (m.sum fun _i xi => xi) ∈ p
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hl : ∀ (i : K), m i ∈ LinearMap.ker ((f - i • 1) ^ l i)
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ => (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ => mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
μ' : K
_hμ' : μ' ∈ m.support.erase μ
k : ℕ
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) ↑k
hm₁ : (m.sum fun _i xi => xi) ∈ ⨆ μ, (f.genEigenspace μ) ↑k
hlk : ∀ (i : K), ↑(l i) ≤ ↑k
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
this : iSupIndep fun x => (f.genEigenspace x) ↑k
⊢ ∀ b ∈ m.support, l b ≤ k

Tactic:
intro i _hi

Result:
case a.a
K : Type u_1
V : Type u_2
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
p : Submodule K V
f : End K V
inst✝ : FiniteDimensional K V
h : ∀ x ∈ p, f x ∈ p
m : K →₀ V
hm₀ : (m.sum fun _i xi => xi) ∈ p
μ : K
hμ : μ ∈ m.support
l : K → ℕ
hl : ∀ (i : K), m i ∈ LinearMap.ker ((f - i • 1) ^ l i)
l₀ : ℕ := m.support.sup l
h_comm : ∀ (μ₁ μ₂ : K), Commute ((f - (algebraMap K (End K V)) μ₁) ^ l₀) ((f - (algebraMap K (End K V)) μ₂) ^ l₀)
g : End K V := (m.support.erase μ).noncommProd (fun μ₁ => (f - (algebraMap K (End K V)) μ₁) ^ l₀) ⋯
hfg : Commute f g
hg₀ : g (m.sum fun _μ mμ => mμ) = g (m μ)
hg₁ : MapsTo ⇑g ↑p ↑p
μ' : K
_hμ' : μ' ∈ m.support.erase μ
k : ℕ
hm₂ : ∀ (i : K), m i ∈ (f.genEigenspace i) ↑k
hm₁ : (m.sum fun _i xi => xi) ∈ ⨆ μ, (f.genEigenspace μ) ↑k
hlk : ∀ (i : K), ↑(l i) ≤ ↑k
hg₂ : MapsTo ⇑g ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
this : iSupIndep fun x => (f.genEigenspace x) ↑k
i : K
_hi : i ∈ m.support
⊢ l i ≤ k