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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
this :
  ∀ (l : ℕ),
    (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
      Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
simp_rw :
  (∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ x ∈ ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker) ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
simp_rw₁ :
  (∃ (l : ℕ),
      (↑l : ℕ∞) ≤ k ∧
        Membership.mem (γ := Submodule R ↥p)
          ((genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) : Submodule R ↥p) x) ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
simp_rw₂ :
  (∃ (l : ℕ),
      (↑l : ℕ∞) ≤ k ∧ x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))) ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
⊢ Membership.mem (γ := Submodule R ↥p)
      ((genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) k : Submodule R ↥p) x ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
have simp_rw₃ : (∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k ∧
      Membership.mem (α := M) (γ := Submodule R M)
        ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) ((p.subtype : (a : ↥p) → M) x : M)) ↔
  Membership.mem (α := M) (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    ((p.subtype : (a : ↥p) → M) x : M)
Tactic: simp_rw [mem_genEigenspace, ← mem_genEigenspace_nat, this,
      Submodule.mem_comap, mem_genEigenspace (k := k), mem_genEigenspace_nat]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
this :
  ∀ (l : ℕ),
    (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
      Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
simp_rw :
  (∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ x ∈ ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker) ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
simp_rw₁ :
  (∃ (l : ℕ),
      (↑l : ℕ∞) ≤ k ∧
        Membership.mem (γ := Submodule R ↥p)
          ((genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) : Submodule R ↥p) x) ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
simp_rw₂ :
  (∃ (l : ℕ),
      (↑l : ℕ∞) ≤ k ∧ x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))) ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
simp_rw₃ :
  (∃ (l : ℕ),
      (↑l : ℕ∞) ≤ k ∧
        Membership.mem (α := M) (γ := Submodule R M)
          ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M)
          ((p.subtype : (a : ↥p) → M) x : M)) ↔
    Membership.mem (α := M) (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
      ((p.subtype : (a : ↥p) → M) x : M)
⊢ Membership.mem (γ := Submodule R ↥p)
      ((genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) k : Submodule R ↥p) x ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
have simp_rw₄ : (∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k ∧
      Membership.mem (α := M) (γ := Submodule R M)
        ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞) : Submodule R M) ((p.subtype : (a : ↥p) → M) x : M)) ↔
  ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k ∧
      Membership.mem (α := M) ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker ((p.subtype : (a : ↥p) → M) x : M)
Tactic: simp_rw [mem_genEigenspace, ← mem_genEigenspace_nat, this,
      Submodule.mem_comap, mem_genEigenspace (k := k), mem_genEigenspace_nat]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
⊢ Membership.mem (γ := Submodule R ↥p)
      ((genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) k : Submodule R ↥p) x ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
have h : ∀ (l : ℕ),
  (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
Tactic: suffices ∀ l : ℕ, genEigenspace (LinearMap.restrict f hfp) μ l =
      Submodule.comap p.subtype (f.genEigenspace μ l) by
    simp_rw [mem_genEigenspace, ← mem_genEigenspace_nat, this,
      Submodule.mem_comap, mem_genEigenspace (k := k), mem_genEigenspace_nat]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
l : ℕ
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
have h : ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
  Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
Tactic: rw [genEigenspace_nat, genEigenspace_nat, ← LinearMap.restrict_smul_one μ,
    LinearMap.restrict_sub hfp, Module.End.pow_restrict _,
    ← LinearMap.ker_comp_of_ker_eq_bot _ (Submodule.ker_subtype p),
    LinearMap.subtype_comp_restrict, LinearMap.domRestrict, ← LinearMap.ker_comp]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
l : ℕ
h :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
have h₁ : ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
  Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
Tactic: rw [genEigenspace_nat, genEigenspace_nat, ← LinearMap.restrict_smul_one μ,
    LinearMap.restrict_sub hfp, Module.End.pow_restrict _,
    ← LinearMap.ker_comp_of_ker_eq_bot _ (Submodule.ker_subtype p),
    LinearMap.subtype_comp_restrict, LinearMap.domRestrict, ← LinearMap.ker_comp]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
l : ℕ
h :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
h₁ :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
have h₂ : ((LinearMap.restrict f hfp - LinearMap.restrict (HSMul.hSMul (β := End R M) μ 1) sorry) ^ l).ker =
  Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
Tactic: rw [genEigenspace_nat, genEigenspace_nat, ← LinearMap.restrict_smul_one μ,
    LinearMap.restrict_sub hfp, Module.End.pow_restrict _,
    ← LinearMap.ker_comp_of_ker_eq_bot _ (Submodule.ker_subtype p),
    LinearMap.subtype_comp_restrict, LinearMap.domRestrict, ← LinearMap.ker_comp]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
l : ℕ
h :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
h₁ :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₂ :
  ((LinearMap.restrict f hfp - LinearMap.restrict (HSMul.hSMul (β := End R M) μ 1) ⋯) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
have h₃ : (HPow.hPow (α := End R ↥p) ((f - HSMul.hSMul (β := End R M) μ 1).restrict sorry) l).ker =
  Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
Tactic: rw [genEigenspace_nat, genEigenspace_nat, ← LinearMap.restrict_smul_one μ,
    LinearMap.restrict_sub hfp, Module.End.pow_restrict _,
    ← LinearMap.ker_comp_of_ker_eq_bot _ (Submodule.ker_subtype p),
    LinearMap.subtype_comp_restrict, LinearMap.domRestrict, ← LinearMap.ker_comp]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
l : ℕ
h :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
h₁ :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₂ :
  ((LinearMap.restrict f hfp - LinearMap.restrict (HSMul.hSMul (β := End R M) μ 1) ⋯) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₃ :
  (HPow.hPow (α := End R ↥p) ((f - HSMul.hSMul (β := End R M) μ 1).restrict ⋯) l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
have h₄ : LinearMap.ker (((f - HSMul.hSMul (β := End R M) μ 1) ^ l).restrict sorry) =
  Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
Tactic: rw [genEigenspace_nat, genEigenspace_nat, ← LinearMap.restrict_smul_one μ,
    LinearMap.restrict_sub hfp, Module.End.pow_restrict _,
    ← LinearMap.ker_comp_of_ker_eq_bot _ (Submodule.ker_subtype p),
    LinearMap.subtype_comp_restrict, LinearMap.domRestrict, ← LinearMap.ker_comp]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
l : ℕ
h :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
h₁ :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₂ :
  ((LinearMap.restrict f hfp - LinearMap.restrict (HSMul.hSMul (β := End R M) μ 1) ⋯) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₃ :
  (HPow.hPow (α := End R ↥p) ((f - HSMul.hSMul (β := End R M) μ 1).restrict ⋯) l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₄ :
  LinearMap.ker (((f - HSMul.hSMul (β := End R M) μ 1) ^ l).restrict ⋯) =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
have h₅ : (p.subtype ∘ₗ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).restrict sorry).ker =
  Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
Tactic: rw [genEigenspace_nat, genEigenspace_nat, ← LinearMap.restrict_smul_one μ,
    LinearMap.restrict_sub hfp, Module.End.pow_restrict _,
    ← LinearMap.ker_comp_of_ker_eq_bot _ (Submodule.ker_subtype p),
    LinearMap.subtype_comp_restrict, LinearMap.domRestrict, ← LinearMap.ker_comp]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
l : ℕ
h :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
h₁ :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₂ :
  ((LinearMap.restrict f hfp - LinearMap.restrict (HSMul.hSMul (β := End R M) μ 1) ⋯) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₃ :
  (HPow.hPow (α := End R ↥p) ((f - HSMul.hSMul (β := End R M) μ 1).restrict ⋯) l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₄ :
  LinearMap.ker (((f - HSMul.hSMul (β := End R M) μ 1) ^ l).restrict ⋯) =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₅ :
  (p.subtype ∘ₗ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).restrict ⋯).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
have h₆ : (((f - HSMul.hSMul (β := End R M) μ 1) ^ l).domRestrict p).ker =
  Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
Tactic: rw [genEigenspace_nat, genEigenspace_nat, ← LinearMap.restrict_smul_one μ,
    LinearMap.restrict_sub hfp, Module.End.pow_restrict _,
    ← LinearMap.ker_comp_of_ker_eq_bot _ (Submodule.ker_subtype p),
    LinearMap.subtype_comp_restrict, LinearMap.domRestrict, ← LinearMap.ker_comp]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
l : ℕ
h :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
h₁ :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₂ :
  ((LinearMap.restrict f hfp - LinearMap.restrict (HSMul.hSMul (β := End R M) μ 1) ⋯) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₃ :
  (HPow.hPow (α := End R ↥p) ((f - HSMul.hSMul (β := End R M) μ 1).restrict ⋯) l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₄ :
  LinearMap.ker (((f - HSMul.hSMul (β := End R M) μ 1) ^ l).restrict ⋯) =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₅ :
  (p.subtype ∘ₗ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).restrict ⋯).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₆ :
  (((f - HSMul.hSMul (β := End R M) μ 1) ^ l).domRestrict p).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
have h₇ : (((f - HSMul.hSMul (β := End R M) μ 1) ^ l) ∘ₗ p.subtype).ker =
  Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
Tactic: rw [genEigenspace_nat, genEigenspace_nat, ← LinearMap.restrict_smul_one μ,
    LinearMap.restrict_sub hfp, Module.End.pow_restrict _,
    ← LinearMap.ker_comp_of_ker_eq_bot _ (Submodule.ker_subtype p),
    LinearMap.subtype_comp_restrict, LinearMap.domRestrict, ← LinearMap.ker_comp]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
l : ℕ
h :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
h₁ :
  ((LinearMap.restrict f hfp - HSMul.hSMul (β := End R ↥p) μ 1) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₂ :
  ((LinearMap.restrict f hfp - LinearMap.restrict (HSMul.hSMul (β := End R M) μ 1) ⋯) ^ l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₃ :
  (HPow.hPow (α := End R ↥p) ((f - HSMul.hSMul (β := End R M) μ 1).restrict ⋯) l).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₄ :
  LinearMap.ker (((f - HSMul.hSMul (β := End R M) μ 1) ^ l).restrict ⋯) =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₅ :
  (p.subtype ∘ₗ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).restrict ⋯).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₆ :
  (((f - HSMul.hSMul (β := End R M) μ 1) ^ l).domRestrict p).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
h₇ :
  (((f - HSMul.hSMul (β := End R M) μ 1) ^ l) ∘ₗ p.subtype).ker =
    Submodule.comap p.subtype ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
have h₈ : (((f - HSMul.hSMul (β := End R M) μ 1) ^ l) ∘ₗ p.subtype).ker =
  (((f - HSMul.hSMul (β := End R M) μ 1) ^ l) ∘ₗ p.subtype).ker
Tactic: rw [genEigenspace_nat, genEigenspace_nat, ← LinearMap.restrict_smul_one μ,
    LinearMap.restrict_sub hfp, Module.End.pow_restrict _,
    ← LinearMap.ker_comp_of_ker_eq_bot _ (Submodule.ker_subtype p),
    LinearMap.subtype_comp_restrict, LinearMap.domRestrict, ← LinearMap.ker_comp]
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
⊢ p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k =
    Submodule.map p.subtype ((genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) k)
have rw : p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k =
  Submodule.map p.subtype (Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k))
Tactic: rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
rw :
  p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k =
    Submodule.map p.subtype (Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k))
⊢ p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k =
    Submodule.map p.subtype ((genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) k)
have rw₁ : p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k =
  p.subtype.range ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k
Tactic: rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
rw :
  p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k =
    Submodule.map p.subtype (Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k))
rw₁ :
  p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k =
    p.subtype.range ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k
⊢ p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k =
    Submodule.map p.subtype ((genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) k)
have rw₂ : p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k = p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k
Tactic: rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_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
p : Submodule R M
f g : End R M
hf : MapsTo (⇑f : (a : M) → M) (↑p : Set M) (↑p : Set M)
hg : MapsTo (⇑g : (a : M) → M) (↑p : Set M) (↑p : Set M)
μ₁ μ₂ : R
h : MapsTo (⇑f : (a : M) → M) (↑(g.maxGenEigenspace μ₁) : Set M) (↑(g.maxGenEigenspace μ₂) : Set M)
x : ↥p
hx : x ∈ (↑(maxGenEigenspace (LinearMap.restrict g hg) μ₁) : Set ↥p)
⊢ Membership.mem (α := ↥p) (↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂) : Set ↥p)
    ((LinearMap.restrict f hf : (a : ↥p) → ↥p) x : ↥p)
have simp_rw : ∀ (hx : (↑x : M) ∈ g.maxGenEigenspace μ₁),
  Membership.mem (α := M) (g.maxGenEigenspace μ₂) ((f : (a : M) → M) (↑x : M) : M)
Tactic: simp_rw [SetLike.mem_coe, mem_maxGenEigenspace, ← LinearMap.restrict_smul_one _,
    LinearMap.restrict_sub _, Module.End.pow_restrict _, LinearMap.restrict_apply,
    Submodule.mk_eq_zero, ← mem_maxGenEigenspace] at hx ⊢
Cleared hypotheses: hx
-- 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
p : Submodule R M
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
μ : R
x : ↥p
hx : x ∈ (↑(eigenspace (LinearMap.restrict f hfp) μ) : Set ↥p)
⊢ Membership.mem (α := M) (f.eigenspace μ) ((p.subtype : (a : ↥p) → M) x : M)
have simp : ∀ (hx : Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f : (a : M) → M) (↑x : M)) sorry = μ • x),
  (f : (a : M) → M) ((p.subtype : (a : ↥p) → M) x : M) = HSMul.hSMul (β := M) μ ((p.subtype : (a : ↥p) → M) x : M)
Tactic: simp only [SetLike.mem_coe, mem_eigenspace_iff, LinearMap.restrict_apply] at hx ⊢
Cleared hypotheses: hx