awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun (i j : ι) ↦ Commute (f i) (f j)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
⊢ Eq.{u_4 + 1} (α := Submodule K M) (⨆ (χ : ι → K), ⨅ (i : ι), (f i).maxGenEigenspace (χ i)) ⊤
have refine : ∀ (i j : ι), Commute (f j) (f i)
Tactic: refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo _
    (fun i j ↦ Module.End.mapsTo_maxGenEigenspace_of_comm ?_) h'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun (i j : ι) ↦ Commute (f i) (f j)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
i j : ι
⊢ Commute (f j) (f i)
have inl : Commute (f j) (f j)
Tactic: rcases eq_or_ne j i with rfl | hij
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Pi (goal)
Goal:
ι : Type u_1
K : Type u_3
M : Type u_4
inst : Field K
inst_1 : AddCommGroup M
inst_2 : Module K M
inst_3 : FiniteDimensional K M
f : ι → End K M
h : Pairwise fun (i j : ι) ↦ Commute (f i) (f j)
h' : ∀ (i : ι), Eq.{u_4 + 1} (α := Submodule K M) (⨆ (μ : K), (f i).maxGenEigenspace μ) ⊤
i j : ι
inl : Commute (f j) (f j)
⊢ Commute (f j) (f i)
have inr : ∀ (hij : j ≠ i), Commute (f j) (f i)
Tactic: rcases eq_or_ne j i with rfl | hij
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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
hm : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) m
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ (g : (a : M) → M) m = μ • m
have hm₁ : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
Tactic: rw [f.mem_genEigenspace] at hm
Cleared hypotheses: hm, hfg, hss, hnil
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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
hm : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
⊢ (g : (a : M) → M) m = μ • m
have obtain : ∀ (l : ℕ) (hm : m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker), (g : (a : M) → M) m = μ • m
Tactic: obtain ⟨l, -, hm⟩ := hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
hm : m ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ (g : (a : M) → M) m = μ • m
have hm₁ : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) m
Tactic: rw [← f.mem_genEigenspace_nat] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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
hfg : Commute f g
hss : g.IsFinitelySemisimple
hnil : IsNilpotent (f - g)
l : ℕ
p : Submodule R M := (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hm : m ∈ p
⊢ (g : (a : M) → M) m = μ • m
have h₁ : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
Tactic: have h₁ : MapsTo g p p := mapsTo_genEigenspace_of_comm hfg μ l
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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
hfg : Commute f g
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)
⊢ (g : (a : M) → M) m = μ • m
have 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)
Tactic: have h₂ : MapsTo (g - algebraMap R (End R M) μ) p p :=
    mapsTo_genEigenspace_of_comm (hfg.sub_right <| Algebra.commute_algebraMap_right μ f) μ l
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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
hfg : Commute f g
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)
⊢ (g : (a : M) → M) m = μ • m
have h₃ : MapsTo (⇑(f - g) : (a : M) → M) (↑p : Set M) (↑p : Set M)
Tactic: have h₃ : MapsTo (f - g) p p :=
    mapsTo_genEigenspace_of_comm (Commute.sub_right rfl hfg) μ l
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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
hfg : Commute f g
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)
⊢ (g : (a : M) → M) m = μ • m
have 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)
Tactic: have h₄ : MapsTo (f - algebraMap R (End R M) μ) p p :=
    mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ l
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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
hfg : Commute f g
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)
⊢ (g : (a : M) → M) m = μ • m
have hfg₁ : Commute (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) (f - g)
Tactic: replace hfg : Commute (f - algebraMap R (End R M) μ) (f - g) :=
    (Commute.sub_right rfl hfg).sub_left <| Algebra.commute_algebraMap_left μ (f - g)
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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)
this :
  IsNilpotent
    (LinearMap.restrict (HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) h₂)
⊢ (g : (a : M) → M) m = μ • m
have this₁ : HSub.hSub (β := End R ↥p) (LinearMap.restrict g h₁) ((algebraMap R (End R ↥p) : (a : R) → End R ↥p) μ : End R ↥p) = 0
Tactic: replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
      eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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)
⊢ (g : (a : M) → M) m = μ • m
have suffices : IsNilpotent
  (LinearMap.restrict (HSub.hSub (β := End R M) g ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) h₂)
Tactic: suffices IsNilpotent ((g - algebraMap R (End R M) μ).restrict h₂) by
    replace this : g.restrict h₁ - algebraMap R (End R p) μ = 0 :=
      eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _)
    simpa [LinearMap.restrict_apply, sub_eq_zero] using LinearMap.congr_fun this ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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 μ
have 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
Tactic: refine le_antisymm (fun m hm ↦ mem_eigenspace_iff.mpr ?_) (f.genEigenspace μ |>.mono ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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
⊢ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k = f.eigenspace μ
have refine_2 : 1 ≤ k
Tactic: refine le_antisymm (fun m hm ↦ mem_eigenspace_iff.mpr ?_) (f.genEigenspace μ |>.mono ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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
⊢ (f : (a : M) → M) m = μ • m
have refine_1 : IsNilpotent (f - f)
Tactic: apply apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hm rfl hf
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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
⊢ f = 0 ↔ ∀ (μ : K), f.HasEigenvalue μ → μ = 0
have mp : f = 0 → ∀ (μ : K), f.HasEigenvalue μ → μ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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
⊢ f = 0 ↔ ∀ (μ : K), f.HasEigenvalue μ → μ = 0
have mpr : (∀ (μ : K), f.HasEigenvalue μ → μ = 0) → f = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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 μ
⊢ μ = 0
have mp : ∀ (hμ0 : ¬μ = 0), False
Tactic: by_contra hμ0
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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
⊢ False
have 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
Tactic: obtain ⟨x, hx, hx_ne⟩ := (Submodule.ne_bot_iff _).mp hμ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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
⊢ False
have hx₁ : (0 : (a : V) → V) x = μ • x
Tactic: rw [mem_eigenspace_iff] at hx
Cleared hypotheses: hx, hx_ne
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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 = ⊤
⊢ f = 0
have rwa : ∀ (this : LinearMap.ker f = ⊤), f = 0
Tactic: rwa [eigenspace_zero, LinearMap.ker_eq_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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
⊢ f = 0
have rwa₁ : ∀ (this : f = 0), f = 0
Tactic: rwa [eigenspace_zero, LinearMap.ker_eq_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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 = 0
have mpr : f.eigenspace 0 = ⊤
Tactic: suffices f.eigenspace 0 = ⊤ by rwa [eigenspace_zero, LinearMap.ker_eq_top] at this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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 = ⊤
have mpr : f.eigenspace 0 = ⨆ (μ : K), f.eigenspace μ
Tactic: rw [← hf.iSup_eigenspace_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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 μ
have mpr : ∀ (μ : K), f.eigenspace μ ≤ f.eigenspace 0
Tactic: refine le_antisymm (le_iSup _ 0) (iSup_le fun μ ↦ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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
⊢ f.eigenspace μ ≤ f.eigenspace 0
have mpr : f.eigenspace 0 ≤ f.eigenspace 0
Tactic: rcases eq_or_ne μ 0 with rfl | hμ
Cleared hypotheses: μ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (goal)
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
⊢ f.eigenspace μ ≤ f.eigenspace 0
have mpr₁ : ∀ (hμ : μ ≠ 0), f.eigenspace μ ≤ f.eigenspace 0
Tactic: rcases eq_or_ne μ 0 with rfl | hμ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Semisimple (hypothesis)
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 μ ≤ f.eigenspace 0
have this : f.eigenspace μ = ⊥
Tactic: have : f.eigenspace μ = ⊥ := not_not.mp (hasEigenvalue_iff.not.mp fun he ↦ hμ (h μ he))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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), f.HasEigenvalue μ
have h : ∀ (μ : R) (hμ : f.HasUnifEigenvalue μ k), f.HasEigenvalue μ
Tactic: peel this with μ hμ
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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.HasEigenvalue μ
have suffices : ∃ (μ : R), f.HasUnifEigenvalue μ k
Tactic: suffices ∃ μ, f.HasUnifEigenvalue μ k by
    peel this with μ hμ
    exact HasUnifEigenvalue.lt zero_lt_one 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
inst_3 : IsAlgClosed K
inst_4 : FiniteDimensional K V
inst_5 : Nontrivial V
f : End K V
⊢ ∃ (c : K), f.HasEigenvalue c
have simp_rw : ∃ (c : K), c ∈ spectrum K f
Tactic: simp_rw [hasEigenvalue_iff_mem_spectrum]
-- 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
inst_3 : IsAlgClosed K
inst_4 : FiniteDimensional K V
f : End K V
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have suffices : ∀ (n : ℕ), finrank K V = n → Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
Tactic: suffices ∀ n, finrank K V = n → ⨆ (μ : K), f.maxGenEigenspace μ = ⊤ by exact this _ rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have 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 μ) ⊤
Tactic: rcases n with - | n
Cleared hypotheses: n, ih, h_dim
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Triangularizable (goal)
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 μ) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have 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 μ) ⊤
Tactic: rcases n with - | n
Cleared hypotheses: n, ih, h_dim
-- 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
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 μ) ⊤
have h : LE.le.{u_2} (α := Submodule K V) ⊤ (⨆ (μ : K), f.maxGenEigenspace μ)
Tactic: rw [← top_le_iff]
-- 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
⊢ 0 < finrank K V
have rw : 0 < n + 1
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
⊢ Eq.{u_2 + 1} (α := Submodule K V) (⨆ (μ : K), f.maxGenEigenspace μ) ⊤
have this : Nontrivial V
Tactic: haveI : Nontrivial V := finrank_pos_iff.1 (by rw [h_dim]; apply Nat.zero_lt_succ)