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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
⊢ iSupIndep f.eigenspace

Tactic:
f.independent_genEigenspace 1

Premises used: Module.End.independent_genEigenspace, 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
ι : Type u_1
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
μ : ι → R
hμ : Function.Injective μ
v : ι → M
h_eigenvec : ∀ (i : ι), f.HasEigenvector (μ i) (v i)
⊢ LinearIndependent R v

Tactic:
f.eigenspaces_iSupIndep.comp hμ |>.linearIndependent _
    (fun i ↦ h_eigenvec i |>.left) (fun i ↦ h_eigenvec i |>.right)

Premises used: Module.End.eigenspaces_iSupIndep, iSupIndep.comp, And.right, And.left, iSupIndep.linearIndependent
-- 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
μs : Set R
xs : (↑μs : Type v) → M
h_eigenvec : ∀ (μ : (↑μs : Type v)), f.HasEigenvector (↑μ : R) (xs μ)
⊢ LinearIndependent R xs

Tactic:
f.eigenvectors_linearIndependent' (fun μ : μs ↦ μ) Subtype.coe_injective _ h_eigenvec

Premises used: Module.End.eigenvectors_linearIndependent', Subtype.coe_injective, Subtype.val
-- 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
h :
  ∀ (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)
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) k =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)

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
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)
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)
⊢ 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)

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

Premises used: Submodule.mem_comap, Module.End.mem_genEigenspace_nat, 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
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
x : ↥p
h :
  ∀ (l : ℕ),
    (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
      Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))
⊢ 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)

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]
-- 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
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
h₈ h₉ :
  (((f - HSMul.hSMul (β := End R M) μ 1) ^ l) ∘ₗ p.subtype).ker =
    (((f - HSMul.hSMul (β := End R M) μ 1) ^ l) ∘ₗ p.subtype).ker
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) (↑l : ℕ∞) =
    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]

Premises used: Module.End.pow_apply_mem_of_forall_mem, LinearMap.subtype_comp_restrict, Submodule.ker_subtype, Module.End.pow_restrict, LinearMap.restrict_sub, LinearMap.ker_comp, LinearMap.domRestrict, LinearMap.restrict_smul_one, Module.End.genEigenspace_nat, LinearMap.ker_comp_of_ker_eq_bot, Submodule.sub_mem, Submodule.smul_mem
-- 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
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
rw₂ rw₃ : p ⊓ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k = p ⊓ (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)

Tactic:
rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_subtype]

Premises used: Submodule.map_comap_eq, Submodule.range_subtype, Module.End.genEigenspace_restrict
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
simp_rw :
  ∀ (hx : (↑x : M) ∈ g.maxGenEigenspace μ₁),
    Membership.mem (α := M) (g.maxGenEigenspace μ₂) ((f : (a : M) → M) (↑x : M) : M)
⊢ Membership.mem (α := ↥p) (↑(maxGenEigenspace (LinearMap.restrict g hg) μ₂) : Set ↥p)
    ((LinearMap.restrict f hf : (a : ↥p) → ↥p) x : ↥p)

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 ⊢

Premises used: Module.End.pow_apply_mem_of_forall_mem, Module.End.pow_restrict, LinearMap.restrict_sub, SetLike.mem_coe, LinearMap.restrict_smul_one, Module.End.mem_maxGenEigenspace, Submodule.mk_eq_zero, Submodule.sub_mem, Submodule.smul_mem, LinearMap.restrict_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
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 : M) ∈ g.maxGenEigenspace μ₁
⊢ Membership.mem (α := M) (g.maxGenEigenspace μ₂) ((f : (a : M) → M) (↑x : M) : M)

Tactic:
h hx

Premises used: Set.Mem
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : M) ∈ g.maxGenEigenspace μ₁
⊢ Membership.mem (α := M) (g.maxGenEigenspace μ₂) ((f : (a : M) → M) (↑x : M) : M)

Tactic:
exact h 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
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)
simp :
  ∀ (hx : Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f : (a : M) → M) (↑x : M)) ⋯ = μ • x),
    (f : (a : M) → M) ((p.subtype : (a : ↥p) → M) x : M) = HSMul.hSMul (β := M) μ ((p.subtype : (a : ↥p) → M) x : M)
⊢ Membership.mem (α := M) (f.eigenspace μ) ((p.subtype : (a : ↥p) → M) x : M)

Tactic:
simp only [SetLike.mem_coe, mem_eigenspace_iff, LinearMap.restrict_apply] at hx ⊢

Premises used: Module.End.mem_eigenspace_iff, SetLike.mem_coe, LinearMap.restrict_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
p : Submodule R M
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
μ : R
x : ↥p
hx : Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f : (a : M) → M) (↑x : M)) ⋯ = μ • x
⊢ (f : (a : M) → M) ((p.subtype : (a : ↥p) → M) x : M) = HSMul.hSMul (β := M) μ ((p.subtype : (a : ↥p) → M) x : M)

Tactic:
congr_arg Subtype.val hx

Premises used: congr_arg, Subtype.val
-- 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
p : Submodule R M
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
μ : R
x : ↥p
hx : Subtype.mk (p := fun (x : M) ↦ x ∈ p) ((f : (a : M) → M) (↑x : M)) ⋯ = μ • x
⊢ (f : (a : M) → M) ((p.subtype : (a : ↥p) → M) x : M) = HSMul.hSMul (β := M) μ ((p.subtype : (a : ↥p) → M) x : M)

Tactic:
exact congr_arg Subtype.val hx

Premises used: congr_arg, Subtype.val
-- 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) ^ finrank K V) ∘ₗ (f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V).ker =
    (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V *
        HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V).ker
⊢ Submodule.comap ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
      ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)) =
    (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V *
        HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V).ker

Tactic:
rw [genEigenspace_nat, ← LinearMap.ker_comp]

Premises used: LinearMap.ker_comp, Module.End.genEigenspace_nat
-- 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) ^ finrank K V) ∘ₗ (f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V).ker =
    (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V *
        HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V).ker

Tactic:
rfl
-- 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
simp_rw :
  LinearMap.ker
      (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^
        (finrank K V + finrank K V)) =
    ((f - HSMul.hSMul (β := End K V) μ 1) ^ (finrank K V + finrank K V)).ker
⊢ (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V *
        HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ finrank K V).ker =
    (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V + finrank K V) : ℕ∞)

Tactic:
simp_rw [← pow_add, genEigenspace_nat]

Premises used: pow_add, Module.End.genEigenspace_nat
-- 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
⊢ LinearMap.ker
      (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^
        (finrank K V + finrank K V)) =
    ((f - HSMul.hSMul (β := End K V) μ 1) ^ (finrank K V + finrank K V)).ker

Tactic:
rfl
-- 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
hk : finrank K V ≤ finrank K V + finrank K V
⊢ Eq (α := Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V + finrank K V) : ℕ∞) : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)

Tactic:
rw [genEigenspace_eq_genEigenspace_finrank_of_le]

Premises used: Module.End.genEigenspace_eq_genEigenspace_finrank_of_le
-- 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
⊢ finrank K V ≤ finrank K V + finrank K V

Tactic:
lia
-- 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
⊢ Submodule.comap ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
      ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)) =
    (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)

Tactic:
have h :=
    calc
      Submodule.comap ((f - μ • 1) ^ finrank K V)
        (f.genEigenspace μ (finrank K V)) =
          LinearMap.ker ((f - algebraMap _ _ μ) ^ finrank K V *
            (f - algebraMap K (End K V) μ) ^ finrank K V) := by
              rw [genEigenspace_nat, ← LinearMap.ker_comp]; rfl
      _ = f.genEigenspace μ (finrank K V + finrank K V : ℕ) := by
              simp_rw [← pow_add, genEigenspace_nat]; rfl
      _ = f.genEigenspace μ (finrank K V) := by
              rw [genEigenspace_eq_genEigenspace_finrank_of_le]; lia
-- 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
h :
  Submodule.comap ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
      ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)) =
    (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
rw :
  Submodule.map ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
      ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V).ker ≤
    ⊥
⊢ Disjoint (f.genEigenrange μ (↑(finrank K V) : ℕ∞))
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞))

Tactic:
rw [disjoint_iff_inf_le, genEigenrange_nat, LinearMap.range_eq_map,
    Submodule.map_inf_eq_map_inf_comap, top_inf_eq, h, genEigenspace_nat]

Premises used: Submodule.map_inf_eq_map_inf_comap, top_inf_eq, Module.End.genEigenrange_nat, Module.End.genEigenspace_nat, LinearMap.range_eq_map, disjoint_iff_inf_le
-- 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
h :
  Submodule.comap ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
      ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)) =
    (f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞)
⊢ Submodule.map ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V)
      ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V).ker ≤
    ⊥

Tactic:
apply Submodule.map_comap_le

Premises used: Submodule.map_comap_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
f : End R M
p : Submodule R M
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
μ : R
hμp : Disjoint (f.eigenspace μ) p
rw : eigenspace (LinearMap.restrict f hfp) μ ≤ ⊥
⊢ eigenspace (LinearMap.restrict f hfp) μ = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_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
p : Submodule R M
hfp : ∀ x ∈ p, Membership.mem (α := M) p ((f : (a : M) → M) x : M)
μ : R
hμp : Disjoint (f.eigenspace μ) p
x : ↥p
hx : x ∈ eigenspace (LinearMap.restrict f hfp) μ
⊢ Membership.mem (γ := Submodule R ↥p) ⊥ x

Tactic:
simpa using hμp.le_bot ⟨eigenspace_restrict_le_eigenspace f hfp μ ⟨x, hx, rfl⟩, x.prop⟩

Premises used: Disjoint.le_bot, Module.End.eigenspace_restrict_le_eigenspace, Subtype.prop, And.intro, Exists.intro, rfl
-- 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 : ℕ
μ : K
hx : f.HasEigenvalue μ
hk : 0 < k
rw rw₁ : Eq (α := ℕ) 0 0
⊢ 0 = finrank.{v, w} K ↥⊥

Tactic:
rw [finrank_bot]

Premises used: finrank_bot
-- 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 : ℕ
μ : K
hx : f.HasEigenvalue μ
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:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
μ : K
n : ℕ
rw :
  Submodule.map f ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).range =
    (f * HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n).range
⊢ Submodule.map f (f.genEigenrange μ (↑n : ℕ∞)) =
    (f * HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n).range

Tactic:
rw [genEigenrange_nat]

Premises used: Module.End.genEigenrange_nat
-- 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
μ : K
n : ℕ
⊢ Submodule.map f ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).range =
    (f * HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n).range

Tactic:
(LinearMap.range_comp _ _).symm

Premises used: LinearMap.range_comp, Eq.symm
-- 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
μ : K
n : ℕ
⊢ Submodule.map f ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).range =
    (f * HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n).range

Tactic:
exact (LinearMap.range_comp _ _).symm

Premises used: LinearMap.range_comp, Eq.symm
-- 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
μ : K
n : ℕ
rw rw₁ :
  LinearMap.range (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n * f) =
    (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n * f).range
⊢ (f * HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n).range =
    (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n * f).range

Tactic:
rw [Algebra.mul_sub_algebraMap_pow_commutes]

Premises used: Algebra.mul_sub_algebraMap_pow_commutes
-- 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
μ : K
n : ℕ
rw :
  Submodule.map (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n)
      (LinearMap.range f) ≤
    ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).range
⊢ Submodule.map (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n)
      (LinearMap.range f) ≤
    f.genEigenrange μ (↑n : ℕ∞)

Tactic:
rw [genEigenrange_nat]

Premises used: Module.End.genEigenrange_nat
-- 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
μ : K
n : ℕ
⊢ Submodule.map (HSub.hSub (β := End K V) f ((algebraMap K (End K V) : (a : K) → End K V) μ : End K V) ^ n)
      (LinearMap.range f) ≤
    ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).range

Tactic:
apply LinearMap.map_le_range

Premises used: LinearMap.map_le_range