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) : ℕ∞)
⊢ ∀ 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)
-- 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
dsimp :
  0 < finrank.{u_1, u_2} K ↥((f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
⊢ 0 < finrank.{u_1, u_2} K ↥ES

Tactic:
dsimp +instances only [ES]
-- 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
rw : 0 < finrank.{u_1, u_2} K ↥((f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(n + 1) : ℕ∞) : Submodule K V)
⊢ 0 < finrank.{u_1, u_2} K ↥((f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)

Tactic:
rw [h_dim]
-- 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
⊢ 0 < finrank.{u_1, u_2} K ↥((f.genEigenspace μ₀ : (a : ℕ∞) → Submodule K V) (↑(n + 1) : ℕ∞) : Submodule K V)

Tactic:
apply pos_finrank_genEigenspace_of_hasEigenvalue hμ₀ (Nat.zero_lt_succ n)

Premises used: Nat.zero_lt_succ, Module.End.pos_finrank_genEigenspace_of_hasEigenvalue
-- 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
⊢ 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)
-- 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
dsimp :
  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
⊢ finrank.{u_1, u_2} K ↥ER + finrank.{u_1, u_2} K ↥ES = finrank K V

Tactic:
dsimp +instances only [ER, ES]
-- 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
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
⊢ 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

Tactic:
rw [Module.End.genEigenspace_nat, Module.End.genEigenrange_nat]

Premises used: Module.End.genEigenrange_nat, Module.End.genEigenspace_nat
-- 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
⊢ 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:
apply LinearMap.finrank_range_add_finrank_ker

Premises used: LinearMap.finrank_range_add_finrank_ker
-- 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
⊢ 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
-- 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
⊢ finrank.{u_1, u_2} K ↥ER < n.succ

Tactic:
lia
-- 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
⊢ finrank.{u_1, u_2} K ↥ER < n.succ

Tactic:
have h_dim_ER : finrank K ER < n.succ := by lia
-- 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
⊢ 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
-- 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 μ) ⊤
⊢ ⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ) = ER

Tactic:
simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER]

Premises used: Submodule.map_iSup, Submodule.map_subtype_top, Eq.symm
-- 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 μ) ⊤
⊢ ⨆ (μ : 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]
-- 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
μ : K
rw :
  Submodule.map ER.subtype (Submodule.comap ER.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤)) ≤
    f.maxGenEigenspace μ
⊢ Submodule.map ER.subtype (f'.maxGenEigenspace μ) ≤ f.maxGenEigenspace μ

Tactic:
rw [maxGenEigenspace, genEigenspace_restrict]

Premises used: Module.End.maxGenEigenspace, Module.End.genEigenspace_restrict
-- 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
μ : K
⊢ Submodule.map ER.subtype (Submodule.comap ER.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤)) ≤
    f.maxGenEigenspace μ

Tactic:
apply Submodule.map_comap_le

Premises used: Submodule.map_comap_le
-- 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
⊢ ∀ (μ : 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
-- 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 μ
rw :
  LE.le.{u_2} (α := Submodule K V) (⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ))
    (⨆ (μ : K), f.maxGenEigenspace μ)
⊢ ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ

Tactic:
rw [← ih_ER']
-- 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 μ
⊢ LE.le.{u_2} (α := Submodule K V) (⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ))
    (⨆ (μ : K), f.maxGenEigenspace μ)

Tactic:
iSup_mono hff'

Premises used: Set.Mem, iSup_mono
-- 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 μ
⊢ LE.le.{u_2} (α := Submodule K V) (⨆ (μ : K), Submodule.map ER.subtype (f'.maxGenEigenspace μ))
    (⨆ (μ : K), f.maxGenEigenspace μ)

Tactic:
exact iSup_mono hff'

Premises used: iSup_mono