awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
μ : R
k : ℕ∞
m : M
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₂ :
  MapsTo (⇑(HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
h₃ : MapsTo (⇑(f - g) : (a : M) → M) (↑p : Set M) (↑p : Set M)
h₄ :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑p : Set M) (↑p : Set M)
hfg : Commute (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) (f - g)
⊢ IsNilpotent
    (LinearMap.restrict (HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) h₂)

Tactic:
simpa [LinearMap.restrict_sub h₄ h₃] using (LinearMap.restrict_commute hfg h₄ h₃).isNilpotent_sub
    (f.isNilpotent_restrict_sub_algebraMap μ l) (Module.End.isNilpotent.restrict h₃ hnil)

Premises used: Module.End.mapsTo_genEigenspace_of_comm, LinearMap.restrict_commute, LinearMap.restrict_sub, Algebra.mul_sub_algebraMap_commutes, Nat.cast, Module.End.isNilpotent_restrict_sub_algebraMap, Module.End.isNilpotent.restrict, Commute.isNilpotent_sub, Submodule.sub_mem
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
⊢ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k = f.eigenspace μ

Tactic:
le_antisymm (fun m hm ↦ mem_eigenspace_iff.mpr ?_) (f.genEigenspace μ |>.mono ?_)

Premises used: Iff.mpr, le_antisymm, OrderHom.mono, Module.End.mem_eigenspace_iff, Module.End.genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
refine_1 :
  ∀ (m : M)
    (hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) m),
    (f : (a : M) → M) m = μ • m
refine_2 : 1 ≤ k
⊢ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k = f.eigenspace μ

Tactic:
refine le_antisymm (fun m hm ↦ mem_eigenspace_iff.mpr ?_) (f.genEigenspace μ |>.mono ?_)

Premises used: le_antisymm, OrderHom.mono, Module.End.genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
m : M
hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) m
refine_1 : IsNilpotent (f - f)
⊢ (f : (a : M) → M) m = μ • m

Tactic:
apply apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hm rfl hf

Premises used: Module.End.apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil, rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
m : M
hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) m
⊢ IsNilpotent (f - f)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
⊢ 1 ≤ k

Tactic:
Order.one_le_iff_pos.mpr hk

Premises used: Iff.mpr, Order.one_le_iff_pos
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
k : ℕ∞
hk : 0 < k
⊢ 1 ≤ k

Tactic:
exact Order.one_le_iff_pos.mpr hk

Premises used: Iff.mpr, Order.one_le_iff_pos
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
hf : f.IsFinitelySemisimple
μ : R
⊢ f.maxGenEigenspace μ = f.eigenspace μ

Tactic:
hf.genEigenspace_eq_eigenspace μ ENat.top_pos

Premises used: ENat.top_pos, Module.End.IsFinitelySemisimple.genEigenspace_eq_eigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
⊢ Eq.{u_4 + 1} (α := Submodule K V) (⨆ (μ : K), f.eigenspace μ) ⊤

Tactic:
simpa only [(isFinitelySemisimple_iff_isSemisimple.mpr hf).maxGenEigenspace_eq_eigenspace] using
    iSup_maxGenEigenspace_eq_top f

Premises used: Iff.mpr, Module.End.isFinitelySemisimple_iff_isSemisimple, Module.End.iSup_maxGenEigenspace_eq_top, Module.End.IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
mp : f = 0 → ∀ (μ : K), f.HasEigenvalue μ → μ = 0
mpr : (∀ (μ : K), f.HasEigenvalue μ → μ = 0) → f = 0
⊢ f = 0 ↔ ∀ (μ : K), f.HasEigenvalue μ → μ = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
hf : IsSemisimple.{u_3, u_4} (R := K) (M := V) 0
μ : K
hμ : HasEigenvalue.{u_3, u_4} (M := V) 0 μ
mp : ∀ (hμ0 : ¬μ = 0), False
⊢ μ = 0

Tactic:
by_contra hμ0
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
hf : IsSemisimple.{u_3, u_4} (R := K) (M := V) 0
μ : K
hμ : HasEigenvalue.{u_3, u_4} (M := V) 0 μ
hμ0 : ¬μ = 0
mp :
  ∀ (x : V)
    (hx : Membership.mem (γ := Submodule K V) ((genEigenspace 0 μ : (a : ℕ∞) → Submodule K V) 1 : Submodule K V) x)
    (hx_ne : x ≠ 0), False
⊢ False

Tactic:
obtain ⟨x, hx, hx_ne⟩ := (Submodule.ne_bot_iff _).mp hμ

Premises used: Submodule.ne_bot_iff, Iff.mp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
hf : IsSemisimple.{u_3, u_4} (R := K) (M := V) 0
μ : K
hμ : HasEigenvalue.{u_3, u_4} (M := V) 0 μ
hμ0 : ¬μ = 0
x : V
hx : Membership.mem (γ := Submodule K V) ((genEigenspace 0 μ : (a : ℕ∞) → Submodule K V) 1 : Submodule K V) x
hx_ne : x ≠ 0
⊢ (0 : (a : V) → V) x = μ • x

Tactic:
rw [mem_eigenspace_iff] at hx

Premises used: Module.End.mem_eigenspace_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
hf : IsSemisimple.{u_3, u_4} (R := K) (M := V) 0
μ : K
hμ : HasEigenvalue.{u_3, u_4} (M := V) 0 μ
hμ0 : ¬μ = 0
x : V
hx : Membership.mem (γ := Submodule K V) ((genEigenspace 0 μ : (a : ℕ∞) → Submodule K V) 1 : Submodule K V) x
hx_ne : x ≠ 0
hx₁ : (0 : (a : V) → V) x = μ • x
⊢ x ≠ 0

Tactic:
rw [mem_eigenspace_iff] at hx

Premises used: Module.End.mem_eigenspace_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
hf : IsSemisimple.{u_3, u_4} (R := K) (M := V) 0
μ : K
hμ : HasEigenvalue.{u_3, u_4} (M := V) 0 μ
hμ0 : ¬μ = 0
x : V
hx : (0 : (a : V) → V) x = μ • x
hx_ne : x ≠ 0
⊢ False

Tactic:
hx_ne ((smul_eq_zero.mp hx.symm).resolve_left hμ0)

Premises used: Or.resolve_left, Iff.mp, Eq.symm, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
hf : IsSemisimple.{u_3, u_4} (R := K) (M := V) 0
μ : K
hμ : HasEigenvalue.{u_3, u_4} (M := V) 0 μ
hμ0 : ¬μ = 0
x : V
hx : (0 : (a : V) → V) x = μ • x
hx_ne : x ≠ 0
⊢ False

Tactic:
exact hx_ne ((smul_eq_zero.mp hx.symm).resolve_left hμ0)

Premises used: Or.resolve_left, Iff.mp, Eq.symm, smul_eq_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
this : f.eigenspace 0 = ⊤
rwa : ∀ (this : LinearMap.ker f = ⊤), f = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : f = 0), f = 0
⊢ f = 0

Tactic:
rwa [eigenspace_zero, LinearMap.ker_eq_top] at this

Premises used: LinearMap.ker_eq_top, Module.End.eigenspace_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
mpr : f.eigenspace 0 = ⊤
⊢ f = 0

Tactic:
suffices f.eigenspace 0 = ⊤ by rwa [eigenspace_zero, LinearMap.ker_eq_top] at this
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
mpr : f.eigenspace 0 = ⨆ (μ : K), f.eigenspace μ
⊢ f.eigenspace 0 = ⊤

Tactic:
rw [← hf.iSup_eigenspace_eq_top]

Premises used: Module.End.IsSemisimple.iSup_eigenspace_eq_top
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
⊢ f.eigenspace 0 = ⨆ (μ : K), f.eigenspace μ

Tactic:
le_antisymm (le_iSup _ 0) (iSup_le fun μ ↦ ?_)

Premises used: le_iSup, le_antisymm, iSup_le, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
mpr : ∀ (μ : K), f.eigenspace μ ≤ f.eigenspace 0
⊢ f.eigenspace 0 = ⨆ (μ : K), f.eigenspace μ

Tactic:
refine le_antisymm (le_iSup _ 0) (iSup_le fun μ ↦ ?_)

Premises used: le_iSup, le_antisymm, iSup_le, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
μ : K
mpr : f.eigenspace 0 ≤ f.eigenspace 0
mpr₁ : ∀ (hμ : μ ≠ 0), f.eigenspace μ ≤ f.eigenspace 0
⊢ f.eigenspace μ ≤ f.eigenspace 0

Tactic:
rcases eq_or_ne μ 0 with rfl | hμ

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
⊢ f.eigenspace 0 ≤ f.eigenspace 0

Tactic:
le_refl _

Premises used: le_refl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
⊢ f.eigenspace 0 ≤ f.eigenspace 0

Tactic:
exact le_refl _

Premises used: le_refl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
μ : K
hμ : μ ≠ 0
⊢ f.eigenspace μ = ⊥

Tactic:
have : f.eigenspace μ = ⊥ := not_not.mp (hasEigenvalue_iff.not.mp fun he ↦ hμ (h μ he))
-- Module: Mathlib.LinearAlgebra.Eigenspace.Semisimple
Goal:
K : Type u_3
V : Type u_4
inst : Field K
inst_1 : IsAlgClosed K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
hf : f.IsSemisimple
h : ∀ (μ : K), f.HasEigenvalue μ → μ = 0
μ : K
hμ : μ ≠ 0
this : f.eigenspace μ = ⊥
⊢ f.eigenspace μ ≤ f.eigenspace 0

Tactic:
simp [this]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
f : End R M
k : ℕ∞
hf : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (μ : R), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ⊤
this : ∃ (μ : R), f.HasUnifEigenvalue μ k
h : ∀ (μ : R) (hμ : f.HasUnifEigenvalue μ k), f.HasEigenvalue μ
⊢ ∃ (μ : R), f.HasEigenvalue μ

Tactic:
peel this with μ hμ
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
f : End R M
k : ℕ∞
hf : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (μ : R), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ⊤
this : ∃ (μ : R), f.HasUnifEigenvalue μ k
μ : R
hμ : f.HasUnifEigenvalue μ k
⊢ f.HasEigenvalue μ

Tactic:
HasUnifEigenvalue.lt zero_lt_one hμ

Premises used: zero_lt_one, Module.End.HasUnifEigenvalue.lt
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
f : End R M
k : ℕ∞
hf : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (μ : R), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ⊤
this : ∃ (μ : R), f.HasUnifEigenvalue μ k
μ : R
hμ : f.HasUnifEigenvalue μ k
⊢ f.HasEigenvalue μ

Tactic:
exact HasUnifEigenvalue.lt zero_lt_one hμ

Premises used: zero_lt_one, Module.End.HasUnifEigenvalue.lt
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
f : End R M
k : ℕ∞
hf : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (μ : R), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ⊤
suffices : ∃ (μ : R), f.HasUnifEigenvalue μ k
⊢ ∃ (μ : R), f.HasEigenvalue μ

Tactic:
suffices ∃ μ, f.HasUnifEigenvalue μ k by
    peel this with μ hμ
    exact HasUnifEigenvalue.lt zero_lt_one hμ
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Nontrivial M
f : End R M
k : ℕ∞
hf : Eq.{u_4 + 1} (α := Submodule R M) (⨆ (μ : R), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ⊤
⊢ ∃ (μ : R), f.HasUnifEigenvalue μ k

Tactic:
simp [HasUnifEigenvalue, ← not_forall, ← iSup_eq_bot, hf]

Premises used: Module.End.HasUnifEigenvalue, iSup_eq_bot, Classical.not_forall
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsAlgClosed K
inst_4 : FiniteDimensional K V
inst_5 : Nontrivial V
f : End K V
simp_rw : ∃ (c : K), c ∈ spectrum K f
⊢ ∃ (c : K), f.HasEigenvalue c

Tactic:
simp_rw [hasEigenvalue_iff_mem_spectrum]

Premises used: Module.End.hasEigenvalue_iff_mem_spectrum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsAlgClosed K
inst_4 : FiniteDimensional K V
inst_5 : Nontrivial V
f : End K V
⊢ ∃ (c : K), c ∈ spectrum K f

Tactic:
spectrum.nonempty_of_isAlgClosed_of_finiteDimensional K f

Premises used: spectrum.nonempty_of_isAlgClosed_of_finiteDimensional, Set.Nonempty
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsAlgClosed K
inst_4 : FiniteDimensional K V
inst_5 : Nontrivial V
f : End K V
⊢ ∃ (c : K), c ∈ spectrum K f

Tactic:
exact spectrum.nonempty_of_isAlgClosed_of_finiteDimensional K f

Premises used: spectrum.nonempty_of_isAlgClosed_of_finiteDimensional
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsAlgClosed K
inst_4 : FiniteDimensional K V
f : End K V
this : ∀ (n : ℕ), finrank K V = n → Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤

Tactic:
this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsAlgClosed K
inst_4 : FiniteDimensional K V
f : End K V
this : ∀ (n : ℕ), finrank K V = n → Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤

Tactic:
exact this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : IsAlgClosed K
inst_4 : FiniteDimensional K V
f : End K V
suffices : ∀ (n : ℕ), finrank K V = n → Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤

Tactic:
suffices ∀ n, finrank K V = n → ⨆ (μ : K), f.maxGenEigenspace μ = ⊤ by exact this _ rfl
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
n : ℕ
ih :
  ∀ m < n,
    ∀ {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 μ) ⊤
V : Type u_2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
h_dim : finrank K V = n
h :
  ∀
    (ih :
      ∀ m < 0,
        ∀ {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 = 0), Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
h₁ :
  ∀ (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), Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤

Tactic:
rcases n with - | 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
ih :
  ∀ m < 0,
    ∀ {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 = 0
h : LE.le.{u_2} (α := Submodule K V) ⊤ (⨆ (μ : K), f.maxGenEigenspace μ)
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Goal:
K : Type u_1
inst : Field K
inst_1 : IsAlgClosed K
V : Type u_2
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
f : End K V
ih :
  ∀ m < 0,
    ∀ {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 = 0
⊢ LE.le.{u_2} (α := Submodule K V) ⊤ (⨆ (μ : K), f.maxGenEigenspace μ)

Tactic:
simp only [Submodule.finrank_eq_zero.1 (Eq.trans (finrank_top _ _) h_dim), bot_le]

Premises used: Submodule.finrank_eq_zero, finrank_top, Iff.mp, bot_le, Eq.trans
-- 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
rw : 0 < n + 1
⊢ 0 < finrank 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
⊢ 0 < n + 1

Tactic:
apply Nat.zero_lt_succ

Premises used: Nat.zero_lt_succ
-- 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
⊢ Nontrivial V

Tactic:
haveI : Nontrivial V := finrank_pos_iff.1 (by rw [h_dim]; apply Nat.zero_lt_succ)
-- 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), f.HasEigenvalue μ₀

Tactic:
exists_eigenvalue f

Premises used: Module.End.exists_eigenvalue
-- 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
h : ∀ (μ₀ : K) (hμ₀ : f.HasEigenvalue μ₀), Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤

Tactic:
obtain ⟨μ₀, hμ₀⟩ : ∃ μ₀, f.HasEigenvalue μ₀ := exists_eigenvalue f

Premises used: Module.End.exists_eigenvalue