awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
⊢ Membership.mem (α := V) (γ := Submodule K V)
    ((f.genEigenspace μ' : (a : ℕ∞) → Submodule K V) (↑l₀ : ℕ∞) : Submodule K V) ((m : (a : K) → V) μ' : V)
have hl₁ : ∀ (i : K),
  Membership.mem (α := V) (γ := Submodule K V)
    ((f.genEigenspace i : (a : ℕ∞) → Submodule K V) (↑(l i) : ℕ∞) : Submodule K V) ((m : (a : K) → V) i : V)
Tactic: simp_rw [← End.mem_genEigenspace_nat] at hl
Cleared hypotheses: hl
-- 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
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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
hl :
  ∀ (i : K),
    Membership.mem (α := V) (γ := Submodule K V)
      ((f.genEigenspace i : (a : ℕ∞) → Submodule K V) (↑(l i) : ℕ∞) : Submodule K V) ((m : (a : K) → V) i : V)
⊢ Membership.mem (α := V) (γ := Submodule K V)
    ((f.genEigenspace μ' : (a : ℕ∞) → Submodule K V) (↑l₀ : ℕ∞) : Submodule K V) ((m : (a : K) → V) μ' : V)
have suffices : LE.le (α := ℕ∞) (↑(l μ') : ℕ∞) (↑l₀ : ℕ∞)
Tactic: suffices (l μ' : ℕ∞) ≤ l₀ from (f.genEigenspace μ').mono this (hl μ')
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
⊢ Eq (α := V) ((g : (a : V) → V) ((m : (a : K) → V) μ' : V) : V) (0 : V)
have hl₀ : Eq (α := V)
  ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ : (a : V) → V)
      ((m : (a : K) → V) μ' : V) :
    V)
  (0 : V)
Tactic: have hl₀ : ((f - algebraMap K (End K V) μ') ^ l₀) (m μ') = 0 := by
      rw [← LinearMap.mem_ker, Algebra.algebraMap_eq_smul_one, ← End.mem_genEigenspace_nat]
      simp_rw [← End.mem_genEigenspace_nat] at hl
      suffices (l μ' : ℕ∞) ≤ l₀ from (f.genEigenspace μ').mono this (hl μ')
      simpa only [Nat.cast_le] using Finset.le_sup hμ'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
hl₀ :
  Eq (α := V)
    ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ : (a : V) → V)
        ((m : (a : K) → V) μ' : V) :
      V)
    (0 : V)
⊢ Eq (α := V) ((g : (a : V) → V) ((m : (a : K) → V) μ' : V) : V) (0 : V)
have this : ((m.support.erase μ).erase μ').noncommProd
      (fun (μ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ l₀) sorry *
    HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ =
  g
Tactic: have : _ = g := (m.support.erase μ).noncommProd_erase_mul (Finset.mem_erase.mpr ⟨hμμ', hμ'⟩)
      (fun μ ↦ (f - algebraMap K (End K V) μ) ^ l₀) (fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂)
-- 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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
hl₀ :
  Eq (α := V)
    ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ : (a : V) → V)
        ((m : (a : K) → V) μ' : V) :
      V)
    (0 : V)
this :
  ((m.support.erase μ).erase μ').noncommProd
        (fun (μ : K) ↦ 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
⊢ Eq (α := V) ((g : (a : V) → V) ((m : (a : K) → V) μ' : V) : V) (0 : V)
have neg : Eq (α := V)
  ((((m.support.erase μ).erase μ').noncommProd
            (fun (μ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ l₀)
            sorry *
          HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ :
        (a : V) → V)
      ((m : (a : K) → V) μ' : V) :
    V)
  (0 : V)
Tactic: rw [← this, Module.End.mul_apply, hl₀, _root_.map_zero]
-- 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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
hl₀ :
  Eq (α := V)
    ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ : (a : V) → V)
        ((m : (a : K) → V) μ' : V) :
      V)
    (0 : V)
this :
  ((m.support.erase μ).erase μ').noncommProd
        (fun (μ : K) ↦ 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
neg :
  Eq (α := V)
    ((((m.support.erase μ).erase μ').noncommProd
              (fun (μ : K) ↦ 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₀ :
          (a : V) → V)
        ((m : (a : K) → V) μ' : V) :
      V)
    (0 : V)
⊢ Eq (α := V) ((g : (a : V) → V) ((m : (a : K) → V) μ' : V) : V) (0 : V)
have neg₁ : Eq (α := V)
  ((((m.support.erase μ).erase μ').noncommProd
          (fun (μ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ l₀) sorry :
        (a : V) → V)
      ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ : (a : V) → V)
          ((m : (a : K) → V) μ' : V) :
        V) :
    V)
  (0 : V)
Tactic: rw [← this, Module.End.mul_apply, hl₀, _root_.map_zero]
-- 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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
hl₀ :
  Eq (α := V)
    ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ : (a : V) → V)
        ((m : (a : K) → V) μ' : V) :
      V)
    (0 : V)
this :
  ((m.support.erase μ).erase μ').noncommProd
        (fun (μ : K) ↦ 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
neg :
  Eq (α := V)
    ((((m.support.erase μ).erase μ').noncommProd
              (fun (μ : K) ↦ 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₀ :
          (a : V) → V)
        ((m : (a : K) → V) μ' : V) :
      V)
    (0 : V)
neg₁ :
  Eq (α := V)
    ((((m.support.erase μ).erase μ').noncommProd
            (fun (μ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ l₀)
            ⋯ :
          (a : V) → V)
        ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ : (a : V) → V)
            ((m : (a : K) → V) μ' : V) :
          V) :
      V)
    (0 : V)
⊢ Eq (α := V) ((g : (a : V) → V) ((m : (a : K) → V) μ' : V) : V) (0 : V)
have neg₂ : Eq.{u_2 + 1} (α := V)
  ((((m.support.erase μ).erase μ').noncommProd
          (fun (μ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ l₀) sorry :
        (a : V) → V)
      0 :
    V)
  (0 : V)
Tactic: rw [← this, Module.End.mul_apply, hl₀, _root_.map_zero]
-- 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
μ' : K
hμ' : μ' ∈ m.support
hμμ' : ¬μ' = μ
hl₀ :
  Eq (α := V)
    ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ : (a : V) → V)
        ((m : (a : K) → V) μ' : V) :
      V)
    (0 : V)
this :
  ((m.support.erase μ).erase μ').noncommProd
        (fun (μ : K) ↦ 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
neg :
  Eq (α := V)
    ((((m.support.erase μ).erase μ').noncommProd
              (fun (μ : K) ↦ 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₀ :
          (a : V) → V)
        ((m : (a : K) → V) μ' : V) :
      V)
    (0 : V)
neg₁ :
  Eq (α := V)
    ((((m.support.erase μ).erase μ').noncommProd
            (fun (μ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ l₀)
            ⋯ :
          (a : V) → V)
        ((HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀ : (a : V) → V)
            ((m : (a : K) → V) μ' : V) :
          V) :
      V)
    (0 : V)
neg₂ :
  Eq.{u_2 + 1} (α := V)
    ((((m.support.erase μ).erase μ').noncommProd
            (fun (μ : K) ↦ HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ l₀)
            ⋯ :
          (a : V) → V)
        0 :
      V)
    (0 : V)
⊢ Eq (α := V) ((g : (a : V) → V) ((m : (a : K) → V) μ' : V) : V) (0 : V)
have neg₃ : Eq.{u_2 + 1} (α := V) 0 0
Tactic: rw [← this, Module.End.mul_apply, hl₀, _root_.map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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
⊢ Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
have 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)
Tactic: have hg₀ : g (m.sum fun _μ mμ ↦ mμ) = g (m μ) := by
    suffices ∀ μ' ∈ m.support, g (m μ') = if μ' = μ then g (m μ) else 0 by
      rw [map_finsuppSum, Finsupp.sum_congr (g2 := fun μ' _ ↦ if μ' = μ then g (m μ) else 0) this,
        Finsupp.sum_ite_eq', if_pos hμ]
    rintro μ' hμ'
    split_ifs with hμμ'
    · rw [hμμ']
    have hl₀ : ((f - algebraMap K (End K V) μ') ^ l₀) (m μ') = 0 := by
      rw [← LinearMap.mem_ker, Algebra.algebraMap_eq_smul_one, ← End.mem_genEigenspace_nat]
      simp_rw [← End.mem_genEigenspace_nat] at hl
      suffices (l μ' : ℕ∞) ≤ l₀ from (f.genEigenspace μ').mono this (hl μ')
      simpa only [Nat.cast_le] using Finset.le_sup hμ'
    have : _ = g := (m.support.erase μ).noncommProd_erase_mul (Finset.mem_erase.mpr ⟨hμμ', hμ'⟩)
      (fun μ ↦ (f - algebraMap K (End K V) μ) ^ l₀) (fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂)
    rw [← this, Module.End.mul_apply, hl₀, _root_.map_zero]
-- 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)
μ' : K
h_1 : μ' ∈ m.support.erase μ
⊢ (fun (g' : End K V) ↦ MapsTo (⇑g' : (a : V) → V) (↑p : Set V) (↑p : Set V))
    (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀)
have 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)
Tactic: suffices MapsTo (f - algebraMap K (End K V) μ') p p by
      simp only [Module.End.coe_pow, this.iterate l₀]