awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
hμ : f.HasEigenvalue μ
⊢ ∃ (v : M), f.HasEigenvector μ v

Tactic:
Submodule.exists_mem_ne_zero_of_ne_bot hμ

Premises used: Submodule.exists_mem_ne_zero_of_ne_bot, Module.End.HasUnifEigenvector
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
h : f.HasEigenvalue μ
n : ℕ
⊢ (f ^ n).HasEigenvalue (μ ^ n)

Tactic:
h.pow n

Premises used: Module.End.HasUnifEigenvalue.pow
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) n : Submodule R M) x
simp :
  ∀
    (hx :
      ∃ (l : ℕ), (↑l : ℕ∞) ≤ n ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)),
    ∃ (l : ℕ),
      (↑l : ℕ∞) ≤ n ∧
        Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
⊢ x ∈ Submodule.comap f ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) n)

Tactic:
simp only [Submodule.mem_comap, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢

Premises used: Submodule.mem_comap, LinearMap.mem_ker, Module.End.mem_genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
hx : ∃ (l : ℕ), (↑l : ℕ∞) ≤ n ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
obtain :
  ∀ (k : ℕ) (hk : (↑k : ℕ∞) ≤ n)
    (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)),
    ∃ (l : ℕ),
      (↑l : ℕ∞) ≤ n ∧
        Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ n ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)

Tactic:
obtain ⟨k, hk, hx⟩ := hx
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
k : ℕ
hk : (↑k : ℕ∞) ≤ n
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ n ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)

Tactic:
⟨k, hk, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
k : ℕ
hk : (↑k : ℕ∞) ≤ n
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)
refine : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ n ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)

Tactic:
refine ⟨k, hk, ?_⟩
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
k : ℕ
hk : (↑k : ℕ∞) ≤ n
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)
induction :
  ∀ ⦃x : M⦄ (hk : (↑0 : ℕ∞) ≤ n)
    (hx : Eq (α := M) ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) x : M) (0 : M)),
    Eq (α := M)
      ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
succ :
  ∀ (n_1 : ℕ),
    (∀ ⦃x : M⦄ (hk : (↑n_1 : ℕ∞) ≤ n)
        (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ n_1 : (a : M) → M) x : M) (0 : M)),
        Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ n_1 : (a : M) → M) ((f : (a : M) → M) x : M) : M)
          (0 : M)) →
      ∀ ⦃x : M⦄ (hk : (↑(n_1 + 1) : ℕ∞) ≤ n)
        (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ (n_1 + 1) : (a : M) → M) x : M) (0 : M)),
        Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ (n_1 + 1) : (a : M) → M) ((f : (a : M) → M) x : M) : M)
          (0 : M)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)

Tactic:
induction k generalizing x
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
hk : (↑0 : ℕ∞) ≤ n
hx : Eq (α := M) ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) ((f : (a : M) → M) x : M) : M)
    (0 : M)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
x : M
hk : (↑0 : ℕ∞) ≤ n
hx : Eq (α := M) ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0 : (a : M) → M) ((f : (a : M) → M) x : M) : M)
    (0 : M)

Tactic:
case zero => simp_all
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
k : ℕ
ih :
  ∀ ⦃x : M⦄ (hk : (↑k : ℕ∞) ≤ n)
    (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)),
    Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
x : M
hk : (↑(k + 1) : ℕ∞) ≤ n
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ (k + 1) : (a : M) → M) x : M) (0 : M)
rw :
  ∀
    (hx :
      Eq (α := M)
        (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
            ((f - HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) x : M) :
          M)
        (0 : M)),
    Eq (α := M)
      (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
          ((f - HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) ((f : (a : M) → M) x : M) : M) :
        M)
      (0 : M)
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ (k + 1) : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)

Tactic:
rw [pow_succ, mul_apply] at hx ⊢

Premises used: pow_succ, Module.End.mul_apply
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
k : ℕ
ih :
  ∀ ⦃x : M⦄ (hk : (↑k : ℕ∞) ≤ n)
    (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)),
    Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
x : M
hk : (↑(k + 1) : ℕ∞) ≤ n
hx :
  Eq (α := M)
    (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
        ((f - HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) x : M) :
      M)
    (0 : M)
⊢ LE.le (α := ℕ∞) (↑k : ℕ∞) (↑(k + 1) : ℕ∞)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
n : ℕ∞
k : ℕ
ih :
  ∀ ⦃x : M⦄ (hk : (↑k : ℕ∞) ≤ n)
    (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M) (0 : M)),
    Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) ((f : (a : M) → M) x : M) : M) (0 : M)
x : M
hk : (↑(k + 1) : ℕ∞) ≤ n
hx :
  Eq (α := M)
    (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
        ((f - HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) x : M) :
      M)
    (0 : M)
⊢ Eq (α := M)
    (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M)
        ((f - HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) ((f : (a : M) → M) x : M) : M) :
      M)
    (0 : M)

Tactic:
simpa using ih (le_trans (by simp) hk) hx

Premises used: le_trans
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
⊢ f.eigenspace μ ∈ f.invtSubmodule

Tactic:
genEigenspace_mem_invtSubmodule f μ 1

Premises used: Module.End.genEigenspace_mem_invtSubmodule, Set.Mem, setOf, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
h :
  ∀ (x : ↥(f.eigenspace μ)),
    Eq.{w + 1} (α := M) (↑((LinearMap.restrict f ⋯ : (a : ↥(f.eigenspace μ)) → ↥(f.eigenspace μ)) x) : M)
      (↑((HSMul.hSMul (β := ↥(f.eigenspace μ) →ₗ[R] ↥(f.eigenspace μ)) μ LinearMap.id :
              (a : ↥(f.eigenspace μ)) → ↥(f.eigenspace μ))
            x) :
        M)
⊢ LinearMap.restrict f ⋯ = HSMul.hSMul (β := ↥(f.eigenspace μ) →ₗ[R] ↥(f.eigenspace μ)) μ LinearMap.id

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : ↥(f.eigenspace μ)
⊢ Eq.{w + 1} (α := M) (↑((LinearMap.restrict f ⋯ : (a : ↥(f.eigenspace μ)) → ↥(f.eigenspace μ)) x) : M)
    (↑((HSMul.hSMul (β := ↥(f.eigenspace μ) →ₗ[R] ↥(f.eigenspace μ)) μ LinearMap.id :
            (a : ↥(f.eigenspace μ)) → ↥(f.eigenspace μ))
          x) :
      M)

Tactic:
mem_eigenspace_iff.mp x.2

Premises used: Module.End.mem_eigenspace_iff, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : ↥(f.eigenspace μ)
⊢ Eq.{w + 1} (α := M) (↑((LinearMap.restrict f ⋯ : (a : ↥(f.eigenspace μ)) → ↥(f.eigenspace μ)) x) : M)
    (↑((HSMul.hSMul (β := ↥(f.eigenspace μ) →ₗ[R] ↥(f.eigenspace μ)) μ LinearMap.id :
            (a : ↥(f.eigenspace μ)) → ↥(f.eigenspace μ))
          x) :
      M)

Tactic:
exact mem_eigenspace_iff.mp x.2

Premises used: Module.End.mem_eigenspace_iff, Iff.mp, Subtype.property
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
hfn : IsNilpotent f
μ : R
hf : f.HasEigenvalue μ
⊢ IsNilpotent μ

Tactic:
hf.isNilpotent_of_isNilpotent hfn

Premises used: Module.End.HasUnifEigenvalue.isNilpotent_of_isNilpotent
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
hμ : f.HasEigenvalue μ
⊢ μ ∈ spectrum R f

Tactic:
hμ.mem_spectrum

Premises used: Module.End.HasUnifEigenvalue.mem_spectrum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
⊢ f.HasEigenvalue μ ↔ μ ∈ spectrum K f

Tactic:
hasUnifEigenvalue_iff_mem_spectrum

Premises used: Module.End.hasUnifEigenvalue_iff_mem_spectrum
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ f.eigenspace (a / b) =
    LinearMap.ker (HSub.hSub (β := End K V) (b • f) ((algebraMap K (End K V) : (a : K) → End K V) a : End K V))

Tactic:
genEigenspace_div f a b hb

Premises used: Module.End.genEigenspace_div
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ f.HasGenEigenvector μ k x ↔
    Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x ∧
      x ≠ 0

Tactic:
Iff.rfl

Premises used: Iff.rfl, Module.End.HasUnifEigenvector
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
⊢ f.HasGenEigenvalue μ k ↔
    Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M)
      (⊥ : Submodule R M)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Module.End.HasUnifEigenvalue
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
h : f.HasGenEigenvalue μ k
⊢ k ≠ 0

Tactic:
HasUnifEigenvalue.exp_ne_zero h

Premises used: Module.End.HasUnifEigenvalue.exp_ne_zero
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
⊢ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ≤ f.maxGenEigenspace μ

Tactic:
(f.genEigenspace μ).monotone le_top

Premises used: OrderHom.monotone, Set.Mem, le_top, Module.End.genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
m : M
⊢ m ∈ f.maxGenEigenspace μ ↔
    ∃ (k : ℕ), Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) m : M) (0 : M)

Tactic:
mem_genEigenspace_top

Premises used: Set.Mem, setOf, Module.End.mem_genEigenspace_top, Set.preimage, Set.singleton
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
μ : R
⊢ f.maxGenEigenspace μ = (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxGenEigenspaceIndex μ) : ℕ∞)

Tactic:
genEigenspace_top_eq_maxUnifEigenspaceIndex _ _

Premises used: Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
h : ∀ (x : M), x ∈ f.maxGenEigenspace μ ↔ x ∈ (f - HSMul.hSMul (β := End R M) μ 1).maxGenEigenspace 0
⊢ f.maxGenEigenspace μ = (f - HSMul.hSMul (β := End R M) μ 1).maxGenEigenspace 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
x : M
⊢ x ∈ f.maxGenEigenspace μ ↔ x ∈ (f - HSMul.hSMul (β := End R M) μ 1).maxGenEigenspace 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k m : ℕ
hm : k ≤ m
hk : f.HasGenEigenvalue μ k
⊢ LE.le (α := ℕ∞) (↑k : ℕ∞) (↑m : ℕ∞)

Tactic:
simpa using hm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
⊢ LE.le (α := ℕ∞) 1 (↑k : ℕ∞)

Tactic:
simpa using Nat.succ_le_of_lt hk

Premises used: Nat.succ_le_of_lt
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
⊢ f.eigenspace μ ≤ f.maxGenEigenspace μ

Tactic:
(f.genEigenspace _).monotone <| OrderTop.le_top _

Premises used: OrderHom.monotone, Set.Mem, OrderTop.le_top, Module.End.genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
hμ : f.HasEigenvalue μ
⊢ LT.lt (α := ℕ∞) 0 (↑k : ℕ∞)

Tactic:
simpa using hk
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
hμ : f.HasGenEigenvalue μ k
⊢ f.HasEigenvalue μ

Tactic:
hμ.lt zero_lt_one

Premises used: zero_lt_one, Module.End.HasUnifEigenvalue.lt
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
hk : 0 < k
⊢ f.HasGenEigenvalue μ k ↔ f.HasEigenvalue μ

Tactic:
simp [hk]
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
apply :
  LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤ : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
⊢ f.maxGenEigenspace μ = (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)

Tactic:
apply le_antisymm _ <| (f.genEigenspace μ).monotone le_top

Premises used: OrderHom.monotone, le_antisymm, le_top, Module.End.genEigenspace
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
rw :
  LE.le (α := Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
⊢ LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤ : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)

Tactic:
rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]

Premises used: Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
⊢ LE.le (α := Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)

Tactic:
apply genEigenspace_le_genEigenspace_finrank f μ

Premises used: Module.End.genEigenspace_le_genEigenspace_finrank
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f g : End R M
h : Commute f g
μ : R
⊢ MapsTo (⇑g : (a : M) → M) (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)

Tactic:
mapsTo_genEigenspace_of_comm h μ ⊤

Premises used: Module.End.mapsTo_genEigenspace_of_comm, Top.top
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
μ : R
k : ℕ
h :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
    (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) : Set M)
⊢ IsNilpotent
    (LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) h)

Tactic:
isNilpotent_restrict_genEigenspace_nat _ _ _

Premises used: Module.End.isNilpotent_restrict_genEigenspace_nat, Module.End.mapsTo_genEigenspace_of_comm, Algebra.mul_sub_algebraMap_commutes, Nat.cast
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
μ : R
h :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
apply : f.maxGenEigenspace μ ≤ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞)
⊢ IsNilpotent
    (LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) h)

Tactic:
apply isNilpotent_restrict_of_le (q := f.genEigenspace μ (maxUnifEigenspaceIndex f μ))
    _ (isNilpotent_restrict_genEigenspace_nat f μ (maxUnifEigenspaceIndex f μ))

Premises used: Module.End.isNilpotent_restrict_genEigenspace_nat, Module.End.mapsTo_genEigenspace_of_comm, Module.End.maxUnifEigenspaceIndex, Algebra.mul_sub_algebraMap_commutes, Nat.cast, Module.End.isNilpotent_restrict_of_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
μ : R
h :
  MapsTo (⇑(HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M)) : (a : M) → M)
    (↑(f.maxGenEigenspace μ) : Set M) (↑(f.maxGenEigenspace μ) : Set M)
rw rw₁ :
  LE.le (α := Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxGenEigenspaceIndex μ) : ℕ∞) : Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxGenEigenspaceIndex μ) : ℕ∞) : Submodule R M)
⊢ f.maxGenEigenspace μ ≤ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞)

Tactic:
rw [maxGenEigenspace_eq]

Premises used: Module.End.maxGenEigenspace_eq
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
rw :
  Disjoint.{w} (α := Submodule R M)
    (⨆ (l : { l : ℕ // (↑l : ℕ∞) ≤ k }), (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑(↑l : ℕ) : ℕ∞))
    (⨆ (l_1 : { l_1 : ℕ // (↑l_1 : ℕ∞) ≤ l }), (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑(↑l_1 : ℕ) : ℕ∞))
⊢ Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) l : Submodule R M)

Tactic:
rw [genEigenspace_eq_iSup_genEigenspace_nat, genEigenspace_eq_iSup_genEigenspace_nat]

Premises used: Module.End.genEigenspace_eq_iSup_genEigenspace_nat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k l : ℕ∞
simp_rw :
  ∀ (i : { l : ℕ // (↑l : ℕ∞) ≤ k }) (i_1 : { l_1 : ℕ // (↑l_1 : ℕ∞) ≤ l }),
    Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑(↑i : ℕ) : ℕ∞) : Submodule R M)
      ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑(↑i_1 : ℕ) : ℕ∞) : Submodule R M)
⊢ Disjoint.{w} (α := Submodule R M)
    (⨆ (l : { l : ℕ // (↑l : ℕ∞) ≤ k }), (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑(↑l : ℕ) : ℕ∞))
    (⨆ (l_1 : { l_1 : ℕ // (↑l_1 : ℕ∞) ≤ l }), (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑(↑l_1 : ℕ) : ℕ∞))

Tactic:
simp_rw [genEigenspace_directed.disjoint_iSup_left, genEigenspace_directed.disjoint_iSup_right]

Premises used: Directed.disjoint_iSup_right, Module.End.genEigenspace_directed, Directed.disjoint_iSup_left
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
⊢ Nontrivial M

Tactic:
nontriviality M
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
Goal:
R : Type v
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
rw :
  Eq (α := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M)
          (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ k_1) k property) : ℕ) : ℕ∞) ⊓
        (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M)
          (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ l_1) l property_1) : ℕ) : ℕ∞) :
      Submodule R M)
    (⊥ : Submodule R M)
⊢ Disjoint (α := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M)
        (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ k_1) k property) : ℕ) : ℕ∞) :
      Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M)
        (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ (↑l : ℕ∞) ≤ l_1) l property_1) : ℕ) : ℕ∞) :
      Submodule R M)

Tactic:
rw [disjoint_iff]

Premises used: disjoint_iff