-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem genEigenspace_restrict (f : End R M) (p : Submodule R M) (k : ℕ∞) (μ : R)
    (hfp : ∀ x : M, x ∈ p → f x ∈ p) :
    genEigenspace (LinearMap.restrict f hfp) μ k =
      Submodule.comap p.subtype (f.genEigenspace μ k)

Proof state:
case h.succ
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
l : ℕ
ih : LinearMap.ker ((LinearMap.restrict f hfp - μ • 1) ^ l) = LinearMap.ker (((f - μ • 1) ^ l) ∘ₗ p.subtype)
⊢ LinearMap.ker ((LinearMap.restrict f hfp - μ • 1) ^ (l + 1)) = LinearMap.ker (((f - μ • 1) ^ (l + 1)) ∘ₗ p.subtype)

Tactic:
erw [pow_succ, pow_succ, LinearMap.ker_comp, LinearMap.ker_comp, ih, ← LinearMap.ker_comp,
  LinearMap.comp_assoc]

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
this : ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)
⊢ x ∈ (genEigenspace (LinearMap.restrict f hfp) μ) k ↔ x ∈ Submodule.comap p.subtype ((f.genEigenspace μ) k)

Tactic:
simp_rw [mem_genEigenspace, ← mem_genEigenspace_nat, this,
  Submodule.mem_comap, mem_genEigenspace (k := k), mem_genEigenspace_nat]

Result:
no goals

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
l : ℕ
⊢ (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)

Tactic:
simp only [genEigenspace_nat, OrderHom.coe_mk, ← LinearMap.ker_comp]

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
l : ℕ
⊢ LinearMap.ker ((LinearMap.restrict f hfp - μ • 1) ^ l) = LinearMap.ker (((f - μ • 1) ^ l) ∘ₗ p.subtype)

Proof state:
case h.zero
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
⊢ LinearMap.ker ((LinearMap.restrict f hfp - μ • 1) ^ 0) = LinearMap.ker (((f - μ • 1) ^ 0) ∘ₗ p.subtype)

Tactic:
rw [pow_zero, pow_zero, LinearMap.one_eq_id]

Result:
case h.zero
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
⊢ LinearMap.ker LinearMap.id = LinearMap.ker (1 ∘ₗ p.subtype)

Proof state:
case h.zero
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
⊢ LinearMap.ker LinearMap.id = LinearMap.ker (1 ∘ₗ p.subtype)

Tactic:
apply (Submodule.ker_subtype _).symm

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
⊢ (genEigenspace (LinearMap.restrict f hfp) μ) k = Submodule.comap p.subtype ((f.genEigenspace μ) k)

Tactic:
ext x

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
⊢ x ∈ (genEigenspace (LinearMap.restrict f hfp) μ) k ↔ x ∈ Submodule.comap p.subtype ((f.genEigenspace μ) k)

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
l : ℕ
⊢ LinearMap.ker ((LinearMap.restrict f hfp - μ • 1) ^ l) = LinearMap.ker (((f - μ • 1) ^ l) ∘ₗ p.subtype)

Tactic:
induction l with
| zero =>
  rw [pow_zero, pow_zero, LinearMap.one_eq_id]
  apply (Submodule.ker_subtype _).symm
| succ l ih =>
  erw [pow_succ, pow_succ, LinearMap.ker_comp, LinearMap.ker_comp, ih, ← LinearMap.ker_comp,
    LinearMap.comp_assoc]

Result:
no goals

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
⊢ x ∈ (genEigenspace (LinearMap.restrict f hfp) μ) k ↔ x ∈ Submodule.comap p.subtype ((f.genEigenspace μ) k)

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]

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
⊢ ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)

Proof state:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
⊢ ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)

Tactic:
intro l

Result:
case h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
l : ℕ
⊢ (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)