-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
p : Submodule K V
f : End K V
inst_3 : FiniteDimensional K V
h : ∀ x ∈ p, Membership.mem (α := V) p ((f : (a : V) → V) x : V)
k : ℕ∞
m : K →₀ V
hm₂ :
  ∀ (i : K),
    Membership.mem (α := V) (γ := Submodule K V) ((f.genEigenspace i : (a : ℕ∞) → Submodule K V) k : Submodule K V)
      ((m : (a : K) → V) i : V)
hm₀ : (m.sum fun (_i : K) (xi : V) ↦ xi) ∈ p
hm₁ :
  Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
    (m.sum fun (_i : K) (xi : V) ↦ xi)
μ : K
hμ : μ ∈ m.support
l : (i : K) → ℕ
hlk : ∀ (i : K), (↑(l i) : ℕ∞) ≤ k
hl : ∀ (i : K), Membership.mem (α := V) ((f - HSMul.hSMul (β := End K V) i 1) ^ l i).ker ((m : (a : K) → V) i : V)
l₀ : ℕ := m.support.sup l
h_comm :
  ∀ (μ₁ μ₂ : K),
    Commute (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀)
      (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₂ : End K V) ^ l₀)
g : End K V :=
  (m.support.erase μ).noncommProd
    (fun (μ₁ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ₁ : End K V) ^ l₀) ⋯
hfg : Commute f g
hg₀ :
  Eq (α := V) ((g : (a : V) → V) (m.sum fun (_μ : K) (mμ : V) ↦ mμ) : V)
    ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)
hg₁ : MapsTo (⇑g : (a : V) → V) (↑p : Set V) (↑p : Set V)
hg₂ :
  MapsTo (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
this : iSupIndep.{u_1 + 1, u_2} (α := Submodule K V) fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
μ' : K
_hμ' : μ' ∈ m.support.erase μ
a :
  ∀
    (hm₂ :
      ∀ (i : K),
        Membership.mem (α := V) (γ := Submodule K V)
          ((f.genEigenspace i : (a : ℕ∞) → Submodule K V) none : Submodule K V) ((m : (a : K) → V) i : V))
    (hm₁ :
      Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) none)
        (m.sum fun (_i : K) (xi : V) ↦ xi))
    (hlk : ∀ (i : K), LE.le (α := ℕ∞) (↑(l i) : ℕ∞) none)
    (hg₂ :
      MapsTo (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) none : Submodule K V) : Set V)
        (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) none : Submodule K V) : Set V))
    (this :
      iSupIndep.{u_1 + 1, u_2} (α := Submodule K V) fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) none),
    LE.le (α := ℕ∞) (↑l₀ : ℕ∞) none
⊢ (↑l₀ : ℕ∞) ≤ k
have a₁ : ∀ (k : ℕ)
  (hm₂ :
    ∀ (i : K),
      Membership.mem (α := V) (γ := Submodule K V)
        ((f.genEigenspace i : (a : ℕ∞) → Submodule K V) (some k) : Submodule K V) ((m : (a : K) → V) i : V))
  (hm₁ :
    Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (some k))
      (m.sum fun (_i : K) (xi : V) ↦ xi))
  (hlk : ∀ (i : K), (↑(l i) : ℕ∞) ≤ some k)
  (hg₂ :
    MapsTo (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (some k) : Submodule K V) : Set V)
      (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (some k) : Submodule K V) : Set V))
  (this :
    iSupIndep.{u_1 + 1, u_2} (α := Submodule K V) fun (x : K) ↦
      (f.genEigenspace x : (a : ℕ∞) → Submodule K V) (some k)),
  (↑l₀ : ℕ∞) ≤ some k
Tactic: obtain _ | k := k
Cleared hypotheses: k, hm₂, hm₁, hlk, hg₂, this