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
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
aux :
  ∀ (μ' : K) (_hμ' : μ' ∈ m.support.erase μ),
    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)
⊢ Disjoint (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
    ((m.support.erase μ).sup fun (i : K) ↦
        LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) i : End K V) ^ l₀) :
      Submodule K V)
have this₁ : Disjoint (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
  ((m.support.erase μ).sup fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k : Submodule K V)
Tactic: have := Finset.supIndep_iff_disjoint_erase.mp (this.supIndep' m.support) μ hμ
-- 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_1 : iSupIndep.{u_1 + 1, u_2} (α := Submodule K V) fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
aux :
  ∀ (μ' : K) (_hμ' : μ' ∈ m.support.erase μ),
    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)
this :
  Disjoint (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
    ((m.support.erase μ).sup fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k : Submodule K V)
⊢ Disjoint (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
    ((m.support.erase μ).sup fun (i : K) ↦
        LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) i : End K V) ^ l₀) :
      Submodule K V)
have apply : LE.le.{u_2} (α := Submodule K V)
  ((m.support.erase μ).sup fun (i : K) ↦
    LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) i : End K V) ^ l₀))
  ((m.support.erase μ).sup fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k)
Tactic: apply this.mono_right
-- 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_1 : iSupIndep.{u_1 + 1, u_2} (α := Submodule K V) fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
aux :
  ∀ (μ' : K) (_hμ' : μ' ∈ m.support.erase μ),
    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)
this :
  Disjoint (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
    ((m.support.erase μ).sup fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k : Submodule K V)
⊢ LE.le.{u_2} (α := Submodule K V)
    ((m.support.erase μ).sup fun (i : K) ↦
      LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) i : End K V) ^ l₀))
    ((m.support.erase μ).sup fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k)
have h₁ : ∀ b ∈ m.support.erase μ,
  LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) b : End K V) ^ l₀) ≤
    (f.genEigenspace b : (a : ℕ∞) → Submodule K V) k
Tactic: apply Finset.sup_mono_fun
-- 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_1 : iSupIndep.{u_1 + 1, u_2} (α := Submodule K V) fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
aux :
  ∀ (μ' : K) (_hμ' : μ' ∈ m.support.erase μ),
    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)
this :
  Disjoint (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
    ((m.support.erase μ).sup fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k : Submodule K V)
μ' : K
hμ' : μ' ∈ m.support.erase μ
⊢ LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀) ≤
    (f.genEigenspace μ' : (a : ℕ∞) → Submodule K V) k
have h₁ : 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: rw [Algebra.algebraMap_eq_smul_one, ← End.genEigenspace_nat]
-- 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
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
aux :
  ∀ (μ' : K) (_hμ' : μ' ∈ m.support.erase μ),
    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)
⊢ Finset.SupIndep.{u_2, u_1} (α := Submodule K V) (m.support.erase μ) fun (i : K) ↦
    LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) i : End K V) ^ l₀)
have this₁ : Finset.SupIndep.{u_2, u_1} (α := Submodule K V) (m.support.erase μ) fun (x : K) ↦
  (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
Tactic: have := this.supIndep' (m.support.erase μ)
-- 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_1 : iSupIndep.{u_1 + 1, u_2} (α := Submodule K V) fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
aux :
  ∀ (μ' : K) (_hμ' : μ' ∈ m.support.erase μ),
    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)
this :
  Finset.SupIndep.{u_2, u_1} (α := Submodule K V) (m.support.erase μ) fun (x : K) ↦
    (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
⊢ Finset.SupIndep.{u_2, u_1} (α := Submodule K V) (m.support.erase μ) fun (i : K) ↦
    LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) i : End K V) ^ l₀)
have h₁ : ∀ x ∈ m.support.erase μ,
  LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) x : End K V) ^ l₀) ≤
    (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
Tactic: apply this.antitone_fun
-- 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_1 : iSupIndep.{u_1 + 1, u_2} (α := Submodule K V) fun (x : K) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
aux :
  ∀ (μ' : K) (_hμ' : μ' ∈ m.support.erase μ),
    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)
this :
  Finset.SupIndep.{u_2, u_1} (α := Submodule K V) (m.support.erase μ) fun (x : K) ↦
    (f.genEigenspace x : (a : ℕ∞) → Submodule K V) k
μ' : K
hμ' : μ' ∈ m.support.erase μ
⊢ LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ' : End K V) ^ l₀) ≤
    (f.genEigenspace μ' : (a : ℕ∞) → Submodule K V) k
have h₁ : 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: rw [Algebra.algebraMap_eq_smul_one, ← End.genEigenspace_nat]
-- 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
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)
⊢ Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
have hg₃ : InjOn (β := V) (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
Tactic: have hg₃ : InjOn g ↑(f.genEigenspace μ k) := by
    apply LinearMap.injOn_of_disjoint_ker subset_rfl
    have this := f.independent_genEigenspace k
    have aux (μ') (_hμ' : μ' ∈ m.support.erase μ) :
        (f.genEigenspace μ') ↑l₀ ≤ (f.genEigenspace μ') k := by
      apply (f.genEigenspace μ').mono
      obtain _ | k := k
      · exact le_top
      · exact Nat.cast_le.2 <| Finset.sup_le fun i _ ↦ Nat.cast_le.1 <| hlk i
    rw [LinearMap.ker_noncommProd_eq_of_supIndep_ker, ← Finset.sup_eq_iSup]
    · have := Finset.supIndep_iff_disjoint_erase.mp (this.supIndep' m.support) μ hμ
      apply this.mono_right
      apply Finset.sup_mono_fun
      intro μ' hμ'
      rw [Algebra.algebraMap_eq_smul_one, ← End.genEigenspace_nat]
      apply aux μ' hμ'
    · have := this.supIndep' (m.support.erase μ)
      apply this.antitone_fun
      intro μ' hμ'
      rw [Algebra.algebraMap_eq_smul_one, ← End.genEigenspace_nat]
      apply aux μ' 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
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)
hg₃ : InjOn (β := V) (⇑g : (a : V) → V) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V) : Set V)
⊢ SurjOn (⇑g : (a : V) → V) (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
    (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
have this : MapsTo (⇑g : (a : V) → V) (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
  (↑(p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) : Set V)
Tactic: have : MapsTo g
        ↑(p ⊓ f.genEigenspace μ k) ↑(p ⊓ f.genEigenspace μ k) :=
      hg₁.inter_inter hg₂