awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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 - HSMul.hSMul (β := End R M) μ 1) ^ k).ker
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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 : ℕ∞
⊢ 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)
have 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)
Tactic: simp_rw [genEigenspace_nat, genEigenspace, OrderHom.coe_mk, iSup_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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)
⊢ 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)
have simp_rw₁ : Eq (α := Submodule R M)
  (({ toFun := fun (k : ℕ∞) ↦ ⨆ (l : ℕ), ⨆ (_ : (↑l : ℕ∞) ≤ k), ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker,
          monotone' := sorry : ℕ∞ →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)
Tactic: simp_rw [genEigenspace_nat, genEigenspace, OrderHom.coe_mk, iSup_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: simp_rw [genEigenspace_nat, genEigenspace, OrderHom.coe_mk, iSup_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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 (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
    (⨆ (k : ℕ), (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) : Submodule R M)
have 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 : ℕ∞))
Tactic: rw [genEigenspace_eq_iSup_genEigenspace_nat, iSup_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 = (f - HSMul.hSMul (β := End R M) μ 1).ker
have rw : (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑1 : ℕ∞) = (f - HSMul.hSMul (β := End R M) μ 1).ker
Tactic: rw [← Nat.cast_one, genEigenspace_nat, pow_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 = (f - HSMul.hSMul (β := End R M) μ 1).ker
have rw₁ : (HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 1).ker = (f - HSMul.hSMul (β := End R M) μ 1).ker
Tactic: rw [← Nat.cast_one, genEigenspace_nat, pow_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 = (f - HSMul.hSMul (β := End R M) μ 1).ker
have rw₂ : LinearMap.ker (f - HSMul.hSMul (β := End R M) μ 1) = (f - HSMul.hSMul (β := End R M) μ 1).ker
Tactic: rw [← Nat.cast_one, genEigenspace_nat, pow_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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) 1 : Submodule R M) x ↔
    (f : (a : M) → M) x = μ • x
have rw : x ∈ (f - HSMul.hSMul (β := End R M) μ 1).ker ↔ (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) x ↔
    (f : (a : M) → M) x = μ • x
have rw₁ : Eq (α := M) ((f - HSMul.hSMul (β := End R M) μ 1 : (a : M) → M) x : M) (0 : M) ↔ (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) x ↔
    (f : (a : M) → M) x = μ • x
have 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
Tactic: rw [genEigenspace_one, LinearMap.mem_ker, LinearMap.sub_apply,
    sub_eq_zero, LinearMap.smul_apply, Module.End.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) x ↔
    (f : (a : M) → M) x = μ • x
have 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
Tactic: rw [genEigenspace_one, LinearMap.mem_ker, LinearMap.sub_apply,
    sub_eq_zero, LinearMap.smul_apply, Module.End.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) x ↔
    (f : (a : M) → M) x = μ • x
have rw₄ : (f : (a : M) → M) x = HSMul.hSMul (β := M) μ ((1 : (a : M) → M) x : M) ↔ (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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) x ↔
    (f : (a : M) → M) x = μ • x
have rw₅ : (f : (a : M) → M) x = μ • 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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 ↔ x = 0
have rw : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 0 : Submodule R M) x ↔ x = 0
have rw₁ : x ∈ (HPow.hPow (β := ℕ) (f - HSMul.hSMul (β := End R M) μ 1) 0).ker ↔ x = 0
Tactic: rw [← Nat.cast_zero, mem_genEigenspace_nat, pow_zero, LinearMap.mem_ker, Module.End.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 0 : Submodule R M) x ↔ x = 0
have rw₂ : Membership.mem (γ := Submodule R M) (LinearMap.ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) 1) x ↔ x = 0
Tactic: rw [← Nat.cast_zero, mem_genEigenspace_nat, pow_zero, LinearMap.mem_ker, Module.End.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 0 : Submodule R M) x ↔ x = 0
have rw₃ : Eq (α := M) ((1 : (a : M) → M) x : M) (0 : M) ↔ x = 0
Tactic: rw [← Nat.cast_zero, mem_genEigenspace_nat, pow_zero, LinearMap.mem_ker, Module.End.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 0 : Submodule R M) x ↔ x = 0
have rw₄ : x = 0 ↔ x = 0
Tactic: rw [← Nat.cast_zero, mem_genEigenspace_nat, pow_zero, LinearMap.mem_ker, Module.End.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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 (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 0 : Submodule R M) (⊥ : Submodule R M)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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.genEigenspace 0 : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) = LinearMap.ker (f ^ k)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ f.HasUnifEigenvalue μ k
have rw : ∃ (x : M),
  Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x ∧ x ≠ 0
Tactic: rw [HasUnifEigenvalue, Submodule.ne_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ ∃ (x : M),
    Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x ∧ x ≠ 0
have h₁ : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x ∧ x ≠ 0
Tactic: use x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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 : ℕ
⊢ (f ^ n : (a : M) → M) v = μ ^ n • v
have zero : (HPow.hPow (β := ℕ) f 0 : (a : M) → M) v = HPow.hPow (β := ℕ) μ 0 • v
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ (f ^ n : (a : M) → M) v = μ ^ n • v
have succ : ∀ (n : ℕ), (f ^ n : (a : M) → M) v = μ ^ n • v → (f ^ (n + 1) : (a : M) → M) v = μ ^ (n + 1) • v
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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 : ℕ
⊢ (f ^ n).HasUnifEigenvalue (μ ^ n) 1
have rw : ∃ (x : M),
  Membership.mem (γ := Submodule R M) (((f ^ n).genEigenspace (μ ^ n) : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) x ∧
    x ≠ 0
Tactic: rw [HasUnifEigenvalue, Submodule.ne_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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 : ℕ
⊢ ∃ (x : M),
    Membership.mem (γ := Submodule R M) (((f ^ n).genEigenspace (μ ^ n) : (a : ℕ∞) → Submodule R M) 1 : Submodule R M)
        x ∧
      x ≠ 0
have 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
Tactic: obtain ⟨m : M, hm⟩ := h.exists_hasUnifEigenvector
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ IsNilpotent μ
have obtain : ∀ (m : M) (hm : f.HasUnifEigenvector μ 1 m), IsNilpotent μ
Tactic: obtain ⟨m : M, hm⟩ := hf.exists_hasUnifEigenvector
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ IsNilpotent μ
have obtain : ∀ (n : ℕ) (hn : f ^ n = 0), IsNilpotent μ
Tactic: obtain ⟨n : ℕ, hn : f ^ n = 0⟩ := hfn
Cleared hypotheses: hfn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
have refine : ∀ (h_unit : IsUnit (HSub.hSub (α := End R M) ((algebraMap R (End R M) : (a : R) → End R M) μ : End R M) f)), False
Tactic: refine spectrum.mem_iff.mpr fun h_unit ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ False
have rcases : ∀ (v : M) (hv : f.HasUnifEigenvector μ 1 v), False
Tactic: rcases hμ.exists_hasUnifEigenvector with ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
have refine : HSub.hSub (β := M) (μ • v) ((f : (a : M) → M) v : M) = 0
Tactic: refine hv.2 ((LinearMap.ker_eq_bot'.mp f'.ker) v (?_ : μ • v - f v = 0))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ HSub.hSub (β := M) (μ • v) ((f : (a : M) → M) v : M) = 0
have rw : μ • v - μ • v = 0
Tactic: rw [hv.apply_eq_smul, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ HSub.hSub (β := M) (μ • v) ((f : (a : M) → M) v : M) = 0
have rw₁ : Eq.{w + 1} (α := M) 0 0
Tactic: rw [hv.apply_eq_smul, sub_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f
have 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)) = ⊥
Tactic: rw [spectrum.mem_iff, IsUnit.sub_iff, LinearMap.isUnit_iff_ker_eq_bot,
    HasUnifEigenvalue, genEigenspace_one, ne_eq, not_iff_not]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [div_eq_mul_inv, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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)
⊢ 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)
have 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)
Tactic: rw [div_eq_mul_inv, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
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.genEigenspace (b⁻¹ * a) : (a : ℕ∞) → Submodule K V) 1 = (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker
have rw : (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker = (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker
Tactic: rw [genEigenspace_one]