awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
μ' : K
h_1 : μ' ∈ m.support.erase μ
suffices :
  MapsTo (⇑(HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V)) : (a : V) → V)
    (↑p : Set V) (↑p : Set V)
⊢ MapsTo (⇑(HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀) : (a : V) → V)
    (↑p : Set V) (↑p : Set V)

Tactic:
suffices MapsTo (f - algebraMap K (End K V) μ') p p by
      simp only [Module.End.coe_pow, this.iterate l₀]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
μ' : K
h_1 : μ' ∈ m.support.erase μ
x : V
hx : x ∈ (↑p : Set V)
rw : HSub.hSub (α := V) ((f : (a : V) → V) x : V) (μ' • x) ∈ (↑p : Set V)
⊢ Membership.mem (α := V) (↑p : Set V)
    ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) : (a : V) → V) x : V)

Tactic:
rw [LinearMap.sub_apply, algebraMap_end_apply]

Premises used: Module.algebraMap_end_apply, LinearMap.sub_apply
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
μ' : K
h_1 : μ' ∈ m.support.erase μ
x : V
hx : x ∈ (↑p : Set V)
⊢ HSub.hSub (α := V) ((f : (a : V) → V) x : V) (μ' • x) ∈ (↑p : Set V)

Tactic:
p.sub_mem (h _ hx) (smul_mem p μ' hx)

Premises used: Set.Mem, Submodule.sub_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
μ' : K
h_1 : μ' ∈ m.support.erase μ
x : V
hx : x ∈ (↑p : Set V)
⊢ HSub.hSub (α := V) ((f : (a : V) → V) x : V) (μ' • x) ∈ (↑p : Set V)

Tactic:
exact p.sub_mem (h _ hx) (smul_mem p μ' hx)

Premises used: Submodule.sub_mem, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
⊢ MapsTo (⇑g : (a : V) → V) (↑p : Set V) (↑p : Set V)

Tactic:
have hg₁ : MapsTo g p p := Finset.noncommProd_induction _ _ _ (fun g' : End K V ↦ MapsTo g' p p)
      (fun f₁ f₂ ↦ MapsTo.comp) (mapsTo_id _) fun μ' _ ↦ by
    suffices MapsTo (f - algebraMap K (End K V) μ') p p by
      simp only [Module.End.coe_pow, this.iterate l₀]
    intro x hx
    rw [LinearMap.sub_apply, algebraMap_end_apply]
    exact p.sub_mem (h _ hx) (smul_mem p μ' hx)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
⊢ 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)

Tactic:
have hg₂ : MapsTo g ↑(f.genEigenspace μ k) ↑(f.genEigenspace μ k) :=
    f.mapsTo_genEigenspace_of_comm hfg μ k
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
apply : Disjoint ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) (LinearMap.ker g)
⊢ InjOn (β := V) (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)

Tactic:
apply LinearMap.injOn_of_disjoint_ker subset_rfl

Premises used: LinearMap.injOn_of_disjoint_ker, subset_rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
⊢ iSupIndep.{u_1 + 1, u_2} (α := Submodule K V) fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k

Tactic:
have this := f.independent_genEigenspace k
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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 : (↑l₀ : ℕ∞) ≤ k
⊢ LE.le (α := Submodule K V) ((f.genEigenspace μ' : (a : ℕ∞) → Submodule K V) (↑l₀ : ℕ∞) : Submodule K V)
    ((f.genEigenspace μ' : (a : ℕ∞) → Submodule K V) k : Submodule K V)

Tactic:
apply (f.genEigenspace μ').mono

Premises used: OrderHom.mono, Module.End.genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
m : K →₀ V
hm₀ : (m.sum fun (_i : K) (xi : V) ↦ xi) ∈ p
μ : K
hμ : μ ∈ m.support
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)
μ' : K
_hμ' : μ' ∈ m.support.erase μ
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

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
m : K →₀ V
hm₀ : (m.sum fun (_i : K) (xi : V) ↦ xi) ∈ p
μ : K
hμ : μ ∈ m.support
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)
μ' : K
_hμ' : μ' ∈ m.support.erase μ
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

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
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)
m : K →₀ V
hm₀ : (m.sum fun (_i : K) (xi : V) ↦ xi) ∈ p
μ : K
hμ : μ ∈ m.support
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)
μ' : K
_hμ' : μ' ∈ m.support.erase μ
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:
Nat.cast_le.2 <| Finset.sup_le fun i _ ↦ Nat.cast_le.1 <| hlk i

Premises used: Iff.mpr, Finset.sup_le, WithTop.some, Iff.mp, Nat.cast_le