awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
V : Type u_2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst_5 : AddCommGroup V] [inst_6 : Module K V] [FiniteDimensional K V] (f : End K V)
      (h_dim : finrank K V = m), Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
ER : Submodule K V := f.genEigenrange μ₀ (↑(finrank K V) : ℕ∞)
h_f_ER : ∀ x ∈ ER, Membership.mem (α := V) ER ((f : (a : V) → V) x : V)
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank.{u_1, u_2} K ↥ES
h_dim_add : finrank.{u_1, u_2} K ↥ER + finrank.{u_1, u_2} K ↥ES = finrank K V
h_dim_ER : finrank.{u_1, u_2} K ↥ER < n.succ
ih_ER : Eq.{u_2 + 1} (α := Submodule K ↥ER) (⨆ (μ : K), f'.maxGenEigenspace μ) ⊤
ih_ER' : ⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
⊢ ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ

Tactic:
have hER : ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ := by
      rw [← ih_ER']
      exact iSup_mono hff'
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
V : Type u_2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst_5 : AddCommGroup V] [inst_6 : Module K V] [FiniteDimensional K V] (f : End K V)
      (h_dim : finrank K V = m), Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
ER : Submodule K V := f.genEigenrange μ₀ (↑(finrank K V) : ℕ∞)
h_f_ER : ∀ x ∈ ER, Membership.mem (α := V) ER ((f : (a : V) → V) x : V)
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank.{u_1, u_2} K ↥ES
h_dim_add : finrank.{u_1, u_2} K ↥ER + finrank.{u_1, u_2} K ↥ES = finrank K V
h_dim_ER : finrank.{u_1, u_2} K ↥ER < n.succ
ih_ER : Eq.{u_2 + 1} (α := Submodule K ↥ER) (⨆ (μ : K), f'.maxGenEigenspace μ) ⊤
ih_ER' : ⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ
⊢ ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ

Tactic:
have hES : ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ :=
      ((f.genEigenspace μ₀).mono le_top).trans (le_iSup f.maxGenEigenspace μ₀)
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
V : Type u_2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst_5 : AddCommGroup V] [inst_6 : Module K V] [FiniteDimensional K V] (f : End K V)
      (h_dim : finrank K V = m), Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
ER : Submodule K V := f.genEigenrange μ₀ (↑(finrank K V) : ℕ∞)
h_f_ER : ∀ x ∈ ER, Membership.mem (α := V) ER ((f : (a : V) → V) x : V)
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank.{u_1, u_2} K ↥ES
h_dim_add : finrank.{u_1, u_2} K ↥ER + finrank.{u_1, u_2} K ↥ES = finrank K V
h_dim_ER : finrank.{u_1, u_2} K ↥ER < n.succ
ih_ER : Eq.{u_2 + 1} (α := Submodule K ↥ER) (⨆ (μ : K), f'.maxGenEigenspace μ) ⊤
ih_ER' : ⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ
hES : ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ
⊢ Disjoint ER ES

Tactic:
have h_disjoint : Disjoint ER ES := generalized_eigenvec_disjoint_range_ker f μ₀
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
V : Type u_2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst_5 : AddCommGroup V] [inst_6 : Module K V] [FiniteDimensional K V] (f : End K V)
      (h_dim : finrank K V = m), Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
ER : Submodule K V := f.genEigenrange μ₀ (↑(finrank K V) : ℕ∞)
h_f_ER : ∀ x ∈ ER, Membership.mem (α := V) ER ((f : (a : V) → V) x : V)
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank.{u_1, u_2} K ↥ES
h_dim_add : finrank.{u_1, u_2} K ↥ER + finrank.{u_1, u_2} K ↥ES = finrank K V
h_dim_ER : finrank.{u_1, u_2} K ↥ER < n.succ
ih_ER : Eq.{u_2 + 1} (α := Submodule K ↥ER) (⨆ (μ : K), f'.maxGenEigenspace μ) ⊤
ih_ER' : ⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ
hES : ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ
h_disjoint : Disjoint ER ES
h : ER ⊔ ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤

Tactic:
rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add.ge h_disjoint]

Premises used: Eq.ge, Submodule.eq_top_of_disjoint, top_le_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
V : Type u_2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ m < n + 1,
    ∀ {V : Type u_2} [inst_5 : AddCommGroup V] [inst_6 : Module K V] [FiniteDimensional K V] (f : End K V)
      (h_dim : finrank K V = m), Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
h_dim : finrank K V = n + 1
this : Nontrivial V
μ₀ : K
hμ₀ : f.HasEigenvalue μ₀
ES : Submodule K V := (f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
ER : Submodule K V := f.genEigenrange μ₀ (↑(finrank K V) : ℕ∞)
h_f_ER : ∀ x ∈ ER, Membership.mem (α := V) ER ((f : (a : V) → V) x : V)
f' : End K ↥ER := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank.{u_1, u_2} K ↥ES
h_dim_add : finrank.{u_1, u_2} K ↥ER + finrank.{u_1, u_2} K ↥ES = finrank K V
h_dim_ER : finrank.{u_1, u_2} K ↥ER < n.succ
ih_ER : Eq.{u_2 + 1} (α := Submodule K ↥ER) (⨆ (μ : K), f'.maxGenEigenspace μ) ⊤
ih_ER' : ⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
hER : ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ
hES : ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ
h_disjoint : Disjoint ER ES
⊢ ER ⊔ ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ

Tactic:
apply sup_le hER hES

Premises used: sup_le
-- 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 : ℕ∞
⊢ p ⊓ ⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k =
    ⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k

Tactic:
le_antisymm (fun m hm ↦ ?_)
    (le_inf_iff.mpr ⟨iSup_le fun μ ↦ inf_le_left, iSup_mono fun μ ↦ inf_le_right⟩)

Premises used: Iff.mpr, inf_le_right, le_inf_iff, le_antisymm, And.intro, iSup_le, inf_le_left, iSup_mono
-- 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 : V
hm : m ∈ p ⊓ ⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
⊢ m ∈ p

Tactic:
obtain ⟨hm₀ : m ∈ p, hm₁ : m ∈ ⨆ μ, f.genEigenspace μ k⟩ := hm
-- 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 : V
hm : m ∈ p ⊓ ⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
hm₀ : m ∈ p
⊢ Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) m

Tactic:
obtain ⟨hm₀ : m ∈ p, hm₁ : m ∈ ⨆ μ, f.genEigenspace μ k⟩ := hm
-- 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 : V
hm₀ : m ∈ p
hm₁ : Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) m
obtain :
  ∀ (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)),
    Membership.mem (γ := Submodule K V) (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
      (m.sum fun (_i : K) (xi : V) ↦ xi)
⊢ Membership.mem (γ := Submodule K V) (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) m

Tactic:
obtain ⟨m, hm₂, rfl⟩ := (mem_iSup_iff_exists_finsupp _ _).mp hm₁

Premises used: Submodule.mem_iSup_iff_exists_finsupp, Iff.mp, 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)
this : ∀ (μ : K), Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
⊢ Membership.mem (γ := Submodule K V) (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
    (m.sum fun (_i : K) (xi : V) ↦ xi)

Tactic:
(mem_iSup_iff_exists_finsupp _ _).mpr ⟨m, fun μ ↦ mem_inf.mp ⟨this μ, hm₂ μ⟩, rfl⟩

Premises used: Iff.mpr, Submodule.mem_iSup_iff_exists_finsupp, Submodule.mem_inf, And.intro, Exists.intro, Iff.mp, 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)
this : ∀ (μ : K), Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
⊢ Membership.mem (γ := Submodule K V) (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
    (m.sum fun (_i : K) (xi : V) ↦ xi)

Tactic:
exact (mem_iSup_iff_exists_finsupp _ _).mpr ⟨m, fun μ ↦ mem_inf.mp ⟨this μ, hm₂ μ⟩, rfl⟩

Premises used: Iff.mpr, Submodule.mem_iSup_iff_exists_finsupp, And.intro, Exists.intro, 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)
suffices : ∀ (μ : K), Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
⊢ Membership.mem (γ := Submodule K V) (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
    (m.sum fun (_i : K) (xi : V) ↦ xi)

Tactic:
suffices ∀ μ, (m μ : V) ∈ p by
    exact (mem_iSup_iff_exists_finsupp _ _).mpr ⟨m, fun μ ↦ mem_inf.mp ⟨this μ, hm₂ μ⟩, 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
pos : ∀ (hμ : μ ∈ m.support), Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
neg : ∀ (hμ : μ ∉ m.support), Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
⊢ Membership.mem (α := V) p ((m : (a : K) → V) μ : V)

Tactic:
by_cases hμ : μ ∈ m.support

Premises used: Finsupp.support
-- 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
⊢ Membership.mem (α := V) p ((m : (a : K) → V) μ : V)

Tactic:
simp only [Finsupp.notMem_support_iff.mp hμ, p.zero_mem]

Premises used: Finsupp.notMem_support_iff, Submodule.zero_mem, Iff.mp
-- 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
⊢ ∀ (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)

Tactic:
have hm₂_aux := hm₂
-- 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
hm₂_aux :
  ∀ (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)
⊢ ∀ (i : K),
    ∃ (l : ℕ),
      (↑l : ℕ∞) ≤ k ∧ Membership.mem (α := V) ((f - HSMul.hSMul (β := End K V) i 1) ^ l).ker ((m : (a : K) → V) i : V)

Tactic:
simp_rw [Module.End.mem_genEigenspace] at hm₂_aux

Premises used: Module.End.mem_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)
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
hm₂_aux :
  ∀ (i : K),
    ∃ (l : ℕ),
      (↑l : ℕ∞) ≤ k ∧ Membership.mem (α := V) ((f - HSMul.hSMul (β := End K V) i 1) ^ l).ker ((m : (a : K) → V) i : V)
pos :
  ∀ (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)),
    Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
⊢ Membership.mem (α := V) p ((m : (a : K) → V) μ : V)

Tactic:
choose l hlk hl using hm₂_aux
-- 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
⊢ ∀ (μ₁ μ₂ : 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₀)

Tactic:
have h_comm : ∀ (μ₁ μ₂ : K),
    Commute ((f - algebraMap K (End K V) μ₁) ^ l₀)
            ((f - algebraMap K (End K V) μ₂) ^ l₀) := fun μ₁ μ₂ ↦
    ((Commute.sub_right rfl <| Algebra.commute_algebraMap_right _ _).sub_left
      (Algebra.commute_algebraMap_left _ _)).pow_pow _ _
-- 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₀) ⋯
⊢ Commute f g

Tactic:
have hfg : Commute f g := Finset.noncommProd_commute _ _ _ _ fun μ' _ ↦
    (Commute.sub_right rfl <| Algebra.commute_algebraMap_right _ _).pow_right _
-- 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
this :
  ∀ μ' ∈ m.support,
    Eq (α := V) ((g : (a : V) → V) ((m : (a : K) → V) μ' : V) : V)
      (if μ' = μ then (g : (a : V) → V) ((m : (a : K) → V) μ : V) else 0 : V)
rw : Eq (α := V) (m.sum fun (a : K) (b : V) ↦ (g : (a : V) → V) b : V) ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)
rw₁ :
  Eq (α := V) (m.sum fun (μ' : K) (x : V) ↦ if μ' = μ then (g : (a : V) → V) ((m : (a : K) → V) μ : V) else 0 : V)
    ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)
rw₂ :
  Eq (α := V) (if μ ∈ m.support then (g : (a : V) → V) ((m : (a : K) → V) μ : V) else 0 : V)
    ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)
rw₃ rw₄ :
  Eq (α := V) ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V) ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)
⊢ Eq (α := V) ((g : (a : V) → V) (m.sum fun (_μ : K) (mμ : V) ↦ mμ) : V)
    ((g : (a : V) → V) ((m : (a : K) → V) μ : V) : V)

Tactic:
rw [map_finsuppSum, Finsupp.sum_congr (g2 := fun μ' _ ↦ if μ' = μ then g (m μ) else 0) this,
        Finsupp.sum_ite_eq', if_pos hμ]

Premises used: Finsupp.sum_ite_eq', Finsupp.sum_congr, if_pos, map_finsuppSum