awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have h : ∀ (μ₀ : K) (hμ₀ : f.HasEigenvalue μ₀), Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
Tactic: obtain ⟨μ₀, hμ₀⟩ : ∃ μ₀, f.HasEigenvalue μ₀ := exists_eigenvalue f
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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) : ℕ∞)
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have h_f_ER : ∀ x ∈ ER, Membership.mem (α := V) ER ((f : (a : V) → V) x : V)
Tactic: have h_f_ER : ∀ x : V, x ∈ ER → f x ∈ ER := fun x hx =>
      map_genEigenrange_le (Submodule.mem_map_of_mem hx)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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
⊢ 0 < finrank.{u_1, u_2} K ↥((f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
have rw : 0 < finrank.{u_1, u_2} K ↥((f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(n + 1) : ℕ∞) : Submodule K V)
Tactic: rw [h_dim]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have h_dim_ES_pos : 0 < finrank.{u_1, u_2} K ↥ES
Tactic: have h_dim_ES_pos : 0 < finrank K ES := by
      dsimp +instances only [ES]
      rw [h_dim]
      apply pos_finrank_genEigenspace_of_hasEigenvalue hμ₀ (Nat.zero_lt_succ n)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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
⊢ finrank.{u_1, u_2} K ↥(f.genEigenrange μ₀ (↑(finrank K V) : ℕ∞)) +
      finrank.{u_1, u_2} K ↥((f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V) =
    finrank K V
have rw : finrank.{u_1, u_2} K ↥((f - HSMul.hSMul (β := End K V) μ₀ 1) ^ finrank K V).range +
    finrank.{u_1, u_2} K ↥((f - HSMul.hSMul (β := End K V) μ₀ 1) ^ finrank K V).ker =
  finrank K V
Tactic: rw [Module.End.genEigenspace_nat, Module.End.genEigenrange_nat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have h_dim_add : finrank.{u_1, u_2} K ↥ER + finrank.{u_1, u_2} K ↥ES = finrank K V
Tactic: have h_dim_add : finrank K ER + finrank K ES = finrank K V := by
      dsimp +instances only [ER, ES]
      rw [Module.End.genEigenspace_nat, Module.End.genEigenrange_nat]
      apply LinearMap.finrank_range_add_finrank_ker
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have h_dim_ER : finrank.{u_1, u_2} K ↥ER < n.succ
Tactic: have h_dim_ER : finrank K ER < n.succ := by lia
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have ih_ER : Eq.{u_2 + 1} (α := Submodule K ↥ER) (⨆ (μ : K), f'.maxGenEigenspace μ) ⊤
Tactic: have ih_ER : ⨆ (μ : K), f'.maxGenEigenspace μ = ⊤ :=
      ih (finrank K ER) h_dim_ER f' rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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 μ) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have ih_ER' : ⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER
Tactic: have ih_ER' : ⨆ (μ : K), (f'.maxGenEigenspace μ).map ER.subtype = ER := by
      simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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
μ : K
⊢ Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
have rw : Submodule.map ER.subtype (Submodule.comap ER.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤)) ≤
  f.maxGenEigenspace μ
Tactic: rw [maxGenEigenspace, genEigenspace_restrict]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have hff' : ∀ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ
Tactic: have hff' :
      ∀ μ, (f'.maxGenEigenspace μ).map ER.subtype ≤ f.maxGenEigenspace μ := by
      intros
      rw [maxGenEigenspace, genEigenspace_restrict]
      apply Submodule.map_comap_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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 μ
have rw : LE.le.{u_2} (α := Submodule K V) (⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ))
  (⨆ (μ : K), f.maxGenEigenspace μ)
Tactic: rw [← ih_ER']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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 μ
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have hER : ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ
Tactic: have hER : ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ := by
      rw [← ih_ER']
      exact iSup_mono hff'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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 μ
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have hES : ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ
Tactic: have hES : ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ :=
      ((f.genEigenspace μ₀).mono le_top).trans (le_iSup f.maxGenEigenspace μ₀)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (hypothesis)
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 μ
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have h_disjoint : Disjoint ER ES
Tactic: have h_disjoint : Disjoint ER ES := generalized_eigenvec_disjoint_range_ker f μ₀
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have h : ER ⊔ ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ
Tactic: rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add.ge h_disjoint]
-- 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 : V
hm : m ∈ p ⊓ ⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
⊢ Membership.mem (γ := Submodule K V) (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) m
have hm₀ : m ∈ p
Tactic: obtain ⟨hm₀ : m ∈ p, hm₁ : m ∈ ⨆ μ, f.genEigenspace μ k⟩ := hm
Cleared hypotheses: hm
-- 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 : V
hm : m ∈ p ⊓ ⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k
hm₀ : m ∈ p
⊢ Membership.mem (γ := Submodule K V) (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) m
have hm₁ : 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
Cleared hypotheses: hm
-- 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 : V
hm₀ : m ∈ p
hm₁ : Membership.mem (γ := Submodule K V) (⨆ (μ : K), (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) m
⊢ Membership.mem (γ := Submodule K V) (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k) m
have 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)
Tactic: obtain ⟨m, hm₂, rfl⟩ := (mem_iSup_iff_exists_finsupp _ _).mp hm₁
Cleared hypotheses: m, hm₀, hm₁
-- 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)
⊢ Membership.mem (γ := Submodule K V) (⨆ (μ : K), p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k)
    (m.sum fun (_i : K) (xi : V) ↦ xi)
have suffices : ∀ (μ : K), Membership.mem (α := V) p ((m : (a : K) → V) μ : V)
Tactic: suffices ∀ μ, (m μ : V) ∈ p by
    exact (mem_iSup_iff_exists_finsupp _ _).mpr ⟨m, fun μ ↦ mem_inf.mp ⟨this μ, hm₂ μ⟩, rfl⟩