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
k : ℕ
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x ↔
      x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
⊢ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) = ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker

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
k : ℕ
x : M
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x ↔
    x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).ker

Tactic:
simp [mem_genEigenspace_nat]

Premises used: Module.End.mem_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
f : End R M
μ : R
k : ℕ∞
simp_rw :
  Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (⨆ (l : { l : ℕ // (↑l : ℕ∞) ≤ k }), ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑l : ℕ)).ker : Submodule R M)
simp_rw₁ :
  Eq (α := Submodule R M)
    (({ toFun := fun (k : ℕ∞) ↦ ⨆ (l : ℕ), ⨆ (_ : (↑l : ℕ∞) ≤ k), ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker,
            monotone' := ⋯ : ℕ∞ →o Submodule R M } :
          (a : ℕ∞) → Submodule R M)
        k :
      Submodule R M)
    (⨆ (l : { l : ℕ // (↑l : ℕ∞) ≤ k }), ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑l : ℕ)).ker : Submodule R M)
simp_rw₂ :
  Eq.{w + 1} (α := Submodule R M) (⨆ (l : ℕ), ⨆ (_ : (↑l : ℕ∞) ≤ k), ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker)
    (⨆ (l : { l : ℕ // (↑l : ℕ∞) ≤ k }), ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑l : ℕ)).ker)
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (⨆ (l : { l : ℕ // (↑l : ℕ∞) ≤ k }), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(↑l : ℕ) : ℕ∞) :
      Submodule R M)

Tactic:
simp_rw [genEigenspace_nat, genEigenspace, OrderHom.coe_mk, iSup_subtype]

Premises used: iSup_subtype, OrderHom.coe_mk, Module.End.genEigenspace_nat, 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
rw :
  Eq.{w + 1} (α := Submodule R M)
    (⨆ (i : ℕ),
      ⨆ (h : LE.le (α := ℕ∞) (↑i : ℕ∞) ⊤),
        (f.genEigenspace μ : (a : ℕ∞) → Submodule R M)
          (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ LE.le (α := ℕ∞) (↑l : ℕ∞) ⊤) i h) : ℕ) : ℕ∞))
    (⨆ (k : ℕ), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞))
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
    (⨆ (k : ℕ), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M)

Tactic:
rw [genEigenspace_eq_iSup_genEigenspace_nat, iSup_subtype]

Premises used: iSup_subtype, 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
f : End R M
μ : R
⊢ Eq.{w + 1} (α := Submodule R M)
    (⨆ (i : ℕ),
      ⨆ (h : LE.le (α := ℕ∞) (↑i : ℕ∞) ⊤),
        (f.genEigenspace μ : (a : ℕ∞) → Submodule R M)
          (↑(↑(Subtype.mk (p := fun (l : ℕ) ↦ LE.le (α := ℕ∞) (↑l : ℕ∞) ⊤) i h) : ℕ) : ℕ∞))
    (⨆ (k : ℕ), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞))

Tactic:
simp only [le_top, iSup_pos]

Premises used: iSup_pos, le_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
rw : (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑1 : ℕ∞) = (f - HSMul.hSMul (β := End R M) μ 1).ker
rw₁ : (HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 1).ker = (f - HSMul.hSMul (β := End R M) μ 1).ker
rw₂ rw₃ : LinearMap.ker (f - HSMul.hSMul (β := End R M) μ 1) = (f - HSMul.hSMul (β := End R M) μ 1).ker
⊢ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 = (f - HSMul.hSMul (β := End R M) μ 1).ker

Tactic:
rw [← Nat.cast_one, genEigenspace_nat, pow_one]

Premises used: pow_one, Module.End.genEigenspace_nat, Nat.cast_one
-- 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
rw : x ∈ (f - HSMul.hSMul (β := End R M) μ 1).ker ↔ (f : (a : M) → M) x = μ • x
rw₁ : Eq (α := M) ((f - HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) x : M) (0 : M) ↔ (f : (a : M) → M) x = μ • x
rw₂ :
  HSub.hSub (α := M) (β := M) ((f : (a : M) → M) x : M) ((HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) x : M) = 0 ↔
    (f : (a : M) → M) x = μ • x
rw₃ :
  Eq (α := M) ((f : (a : M) → M) x : M) ((HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) x : M) ↔
    (f : (a : M) → M) x = μ • x
rw₄ : (f : (a : M) → M) x = HSMul.hSMul (β := M) μ ((1 : (a : M) → M) x : M) ↔ (f : (a : M) → M) x = μ • x
rw₅ rw₆ : (f : (a : M) → M) x = μ • x ↔ (f : (a : M) → M) x = μ • x
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) x ↔
    (f : (a : M) → M) x = μ • x

Tactic:
rw [genEigenspace_one, LinearMap.mem_ker, LinearMap.sub_apply,
    sub_eq_zero, LinearMap.smul_apply, Module.End.one_apply]

Premises used: LinearMap.smul_apply, sub_eq_zero, Module.End.genEigenspace_one, LinearMap.mem_ker, Module.End.one_apply, LinearMap.sub_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
x : M
rw :
  Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑0 : ℕ∞) : Submodule R M) x ↔
    x = 0
rw₁ : x ∈ (HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0).ker ↔ x = 0
rw₂ : Membership.mem (γ := Submodule R M) (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) 1) x ↔ x = 0
rw₃ : Eq (α := M) ((1 : (a : M) → M) x : M) (0 : M) ↔ x = 0
rw₄ rw₅ : x = 0 ↔ x = 0
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 0 : Submodule R M) x ↔ x = 0

Tactic:
rw [← Nat.cast_zero, mem_genEigenspace_nat, pow_zero, LinearMap.mem_ker, Module.End.one_apply]

Premises used: pow_zero, LinearMap.mem_ker, Module.End.one_apply, Module.End.mem_genEigenspace_nat, Nat.cast_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
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 0 : Submodule R M) x ↔
      Membership.mem (γ := Submodule R M) ⊥ x
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 0 : Submodule R M) (⊥ : Submodule R M)

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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 0 : Submodule R M) x ↔
    Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
apply mem_genEigenspace_zero

Premises used: Module.End.mem_genEigenspace_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
k : ℕ
h :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) ((f.genEigenspace 0 : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x ↔
      x ∈ LinearMap.ker (f ^ k)
⊢ (f.genEigenspace 0 : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) = LinearMap.ker (f ^ k)

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
k : ℕ
x : M
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace 0 : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M) x ↔
    x ∈ LinearMap.ker (f ^ k)

Tactic:
simp [mem_genEigenspace_nat]

Premises used: Module.End.mem_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
f : End R M
μ : R
k : ℕ∞
h : f.HasUnifEigenvalue μ k
⊢ (↑f : (k : ℕ∞) → f.UnifEigenvalues k → R) k (Subtype.mk (p := fun (μ : R) ↦ f.HasUnifEigenvalue μ k) μ h) = μ

Tactic:
rfl

Premises used: Module.End.UnifEigenvalues.val, rfl
-- 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
k : ℕ∞
μ : f.UnifEigenvalues k
⊢ Subtype.mk (p := fun (μ : R) ↦ f.HasUnifEigenvalue μ k) ((↑f : (k : ℕ∞) → f.UnifEigenvalues k → R) k μ) ⋯ = μ

Tactic:
rfl

Premises used: Module.End.UnifEigenvalues.val, Module.End.UnifEigenvalues, rfl
-- 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
h : f.HasUnifEigenvector μ k x
rw :
  ∃ (x : M),
    Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x ∧ x ≠ 0
⊢ f.HasUnifEigenvalue μ k

Tactic:
rw [HasUnifEigenvalue, Submodule.ne_bot_iff]

Premises used: Module.End.HasUnifEigenvalue, Submodule.ne_bot_iff
-- 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
h : f.HasUnifEigenvector μ k x
h₁ : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x ∧ x ≠ 0
⊢ ∃ (x : M),
    Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x ∧ x ≠ 0

Tactic:
use 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
k : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x ∧ x ≠ 0

Tactic:
h

Premises used: 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 : ℕ∞
x : M
h : f.HasUnifEigenvector μ k x
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x ∧ x ≠ 0

Tactic:
exact h
-- 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
hx : f.HasUnifEigenvector μ 1 x
⊢ (f : (a : M) → M) x = μ • x

Tactic:
mem_genEigenspace_one.mp hx.1

Premises used: And.left, Module.End.mem_genEigenspace_one, Iff.mp
-- 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
v : M
hv : f.HasUnifEigenvector μ 1 v
n : ℕ
zero : (HPow.hPow (β := ℕ) f 0 : (a : M) → M) v = HPow.hPow (β := ℕ) μ 0 • v
succ : ∀ (n : ℕ), (f ^ n : (a : M) → M) v = μ ^ n • v → (f ^ (n + 1) : (a : M) → M) v = μ ^ (n + 1) • v
⊢ (f ^ n : (a : M) → M) v = μ ^ n • v

Tactic:
induction n
-- 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
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ (HPow.hPow (β := ℕ) f 0 : (a : M) → M) v = HPow.hPow (β := ℕ) μ 0 • v

Tactic:
simp [*, pow_succ f, hv.apply_eq_smul, smul_smul, pow_succ' μ]

Premises used: pow_succ, smul_smul, Module.End.HasUnifEigenvector.apply_eq_smul, pow_succ'
-- 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
v : M
hv : f.HasUnifEigenvector μ 1 v
n : ℕ
h : (f ^ n : (a : M) → M) v = μ ^ n • v
⊢ (f ^ (n + 1) : (a : M) → M) v = μ ^ (n + 1) • v

Tactic:
simp [*, pow_succ f, hv.apply_eq_smul, smul_smul, pow_succ' μ]

Premises used: pow_succ, smul_smul, Module.End.HasUnifEigenvector.apply_eq_smul, pow_succ'
-- 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.HasUnifEigenvalue μ k
⊢ ∃ (v : M), f.HasUnifEigenvector μ k 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.HasUnifEigenvalue μ 1
n : ℕ
rw :
  ∃ (x : M),
    Membership.mem (γ := Submodule R M) (((f ^ n).genEigenspace (μ ^ n) : (a : ℕ∞) → Submodule R M) 1 : Submodule R M)
        x ∧
      x ≠ 0
⊢ (f ^ n).HasUnifEigenvalue (μ ^ n) 1

Tactic:
rw [HasUnifEigenvalue, Submodule.ne_bot_iff]

Premises used: Module.End.HasUnifEigenvalue, Submodule.ne_bot_iff
-- 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.HasUnifEigenvalue μ 1
n : ℕ
obtain :
  ∀ (m : M) (hm : f.HasUnifEigenvector μ 1 m),
    ∃ (x : M),
      Membership.mem (γ := Submodule R M) (((f ^ n).genEigenspace (μ ^ n) : (a : ℕ∞) → Submodule R M) 1 : Submodule R M)
          x ∧
        x ≠ 0
⊢ ∃ (x : M),
    Membership.mem (γ := Submodule R M) (((f ^ n).genEigenspace (μ ^ n) : (a : ℕ∞) → Submodule R M) 1 : Submodule R M)
        x ∧
      x ≠ 0

Tactic:
obtain ⟨m : M, hm⟩ := h.exists_hasUnifEigenvector

Premises used: Module.End.HasUnifEigenvalue.exists_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.HasUnifEigenvalue μ 1
n : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ Membership.mem (γ := Submodule R M) (((f ^ n).genEigenspace (μ ^ n) : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) m

Tactic:
simpa [mem_genEigenspace_one] using hm.pow_apply n

Premises used: Module.End.HasUnifEigenvector.pow_apply, Module.End.mem_genEigenspace_one
-- 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.HasUnifEigenvalue μ 1
n : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ ∃ (x : M),
    Membership.mem (γ := Submodule R M) (((f ^ n).genEigenspace (μ ^ n) : (a : ℕ∞) → Submodule R M) 1 : Submodule R M)
        x ∧
      x ≠ 0

Tactic:
exact ⟨m, by simpa [mem_genEigenspace_one] using hm.pow_apply n, hm.2⟩
-- 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.HasUnifEigenvalue μ 1
obtain : ∀ (m : M) (hm : f.HasUnifEigenvector μ 1 m), IsNilpotent μ
⊢ IsNilpotent μ

Tactic:
obtain ⟨m : M, hm⟩ := hf.exists_hasUnifEigenvector

Premises used: Module.End.HasUnifEigenvalue.exists_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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
hfn : IsNilpotent f
μ : R
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
obtain : ∀ (n : ℕ) (hn : f ^ n = 0), IsNilpotent μ
⊢ IsNilpotent μ

Tactic:
obtain ⟨n : ℕ, hn : f ^ n = 0⟩ := hfn
-- 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
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ μ ^ n = 0

Tactic:
simpa [hn, hm.2, eq_comm (a := (0 : M))] using hm.pow_apply n

Premises used: Module.End.HasUnifEigenvector.pow_apply, eq_comm, And.right
-- 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
hf : f.HasUnifEigenvalue μ 1
m : M
hm : f.HasUnifEigenvector μ 1 m
n : ℕ
hn : f ^ n = 0
⊢ IsNilpotent μ

Tactic:
exact ⟨n, by simpa [hn, hm.2, eq_comm (a := (0 : M))] using hm.pow_apply n⟩
-- 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.HasUnifEigenvalue μ 1
⊢ μ ∈ spectrum R f

Tactic:
spectrum.mem_iff.mpr fun h_unit ↦ ?_

Premises used: Iff.mpr, spectrum.mem_iff
-- 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.HasUnifEigenvalue μ 1
refine :
  ∀ (h_unit : IsUnit (HSub.hSub (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) f)), False
⊢ μ ∈ spectrum R f

Tactic:
refine spectrum.mem_iff.mpr fun h_unit ↦ ?_

Premises used: Iff.mpr, spectrum.mem_iff
-- 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.HasUnifEigenvalue μ 1
h_unit : IsUnit (HSub.hSub (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
rcases : ∀ (v : M) (hv : f.HasUnifEigenvector μ 1 v), False
⊢ False

Tactic:
rcases hμ.exists_hasUnifEigenvector with ⟨v, hv⟩

Premises used: Module.End.HasUnifEigenvalue.exists_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.HasUnifEigenvalue μ 1
h_unit : IsUnit (HSub.hSub (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
⊢ False

Tactic:
hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (?_ : μ • v - f v = 0))

Premises used: LinearMap.ker_eq_bot', And.right, Iff.mp, LinearEquiv.ker
-- 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.HasUnifEigenvalue μ 1
h_unit : IsUnit (HSub.hSub (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
refine : HSub.hSub (β := M) (μ • v) ((f : (a : M) → M) v : M) = 0
⊢ False

Tactic:
refine hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (?_ : μ • v - f v = 0))

Premises used: LinearMap.ker_eq_bot', And.right, Iff.mp, LinearEquiv.ker
-- 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.HasUnifEigenvalue μ 1
h_unit : IsUnit (HSub.hSub (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) f)
f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit
v : M
hv : f.HasUnifEigenvector μ 1 v
rw : μ • v - μ • v = 0
rw₁ rw₂ : Eq.{w + 1} (α := M) 0 0
⊢ HSub.hSub (β := M) (μ • v) ((f : (a : M) → M) v : M) = 0

Tactic:
rw [hv.apply_eq_smul, sub_self]

Premises used: sub_self, Module.End.HasUnifEigenvector.apply_eq_smul
-- 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 :
  (f - HSMul.hSMul (β := End K V) μ 1).ker = ⊥ ↔
    LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V)) = ⊥
⊢ f.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f

Tactic:
rw [spectrum.mem_iff, IsUnit.sub_iff, LinearMap.isUnit_iff_ker_eq_bot,
    HasUnifEigenvalue, genEigenspace_one, ne_eq, not_iff_not]

Premises used: not_iff_not, LinearMap.isUnit_iff_ker_eq_bot, Module.End.HasUnifEigenvalue, IsUnit.sub_iff, ne_eq, Module.End.genEigenspace_one, spectrum.mem_iff
-- 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 - HSMul.hSMul (β := End K V) μ 1).ker = ⊥ ↔
    LinearMap.ker (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V)) = ⊥

Tactic:
simp [Submodule.ext_iff, LinearMap.mem_ker]

Premises used: Submodule.ext_iff, LinearMap.mem_ker
-- 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
rw :
  Eq (α := Submodule K V) ((f.genEigenspace (a * b⁻¹) : (a : ℕ∞) → Submodule K V) 1 : Submodule K V)
    ((f.genEigenspace (b⁻¹ * a) : (a : ℕ∞) → Submodule K V) 1 : Submodule K V)
rw₁ rw₂ :
  Eq (α := Submodule K V) ((f.genEigenspace (b⁻¹ * a) : (a : ℕ∞) → Submodule K V) 1 : Submodule K V)
    ((f.genEigenspace (b⁻¹ * a) : (a : ℕ∞) → Submodule K V) 1 : Submodule K V)
⊢ Eq (α := Submodule K V) ((f.genEigenspace (a / b) : (a : ℕ∞) → Submodule K V) 1 : Submodule K V)
    ((f.genEigenspace (b⁻¹ * a) : (a : ℕ∞) → Submodule K V) 1 : Submodule K V)

Tactic:
rw [div_eq_mul_inv, mul_comm]

Premises used: div_eq_mul_inv, mul_comm
-- 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
rw rw₁ : (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker = (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker
⊢ (f.genEigenspace (b⁻¹ * a) : (a : ℕ∞) → Submodule K V) 1 = (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker

Tactic:
rw [genEigenspace_one]

Premises used: Module.End.genEigenspace_one
-- 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
rw rw₁ : (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker = (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker
⊢ (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker = (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1).ker

Tactic:
rw [smul_smul]

Premises used: smul_smul
-- 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
rw rw₁ : (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1).ker = LinearMap.ker (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1)
⊢ (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1).ker = (b • (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1)).ker

Tactic:
rw [LinearMap.ker_smul _ b hb]

Premises used: LinearMap.ker_smul
-- 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
rw : LinearMap.ker (b • f - b • b⁻¹ • HSMul.hSMul (β := End K V) a 1) = (b • f - HSMul.hSMul (β := End K V) a 1).ker
rw₁ rw₂ : LinearMap.ker (b • f - HSMul.hSMul (β := End K V) a 1) = (b • f - HSMul.hSMul (β := End K V) a 1).ker
⊢ (b • (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1)).ker = (b • f - HSMul.hSMul (β := End K V) a 1).ker

Tactic:
rw [smul_sub, smul_inv_smul₀ hb]

Premises used: smul_inv_smul₀, smul_sub
-- 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 : ∀ (x : M), x ∈ f.genEigenrange μ (↑k : ℕ∞) ↔ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).range
⊢ f.genEigenrange μ (↑k : ℕ∞) = ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).range

Tactic:
ext x