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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
refine_2 :
  Membership.mem (α := M) (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
    ((g ^ l : (a : M) → M) z : M)
⊢ Membership.mem (α := M) (↑(s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) : Set M)
    ((g ^ l : (a : M) → M) (y + z) : M)

Tactic:
rw [SetLike.mem_coe, map_add, hl, zero_add]

Premises used: map_add, zero_add, SetLike.mem_coe
-- 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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
this :
  Submodule.map (g ^ l) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ≤
    s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k
⊢ Membership.mem (α := M) (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
    ((g ^ l : (a : M) → M) z : M)

Tactic:
this (Submodule.mem_map_of_mem hz)

Premises used: Submodule.mem_map_of_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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
this :
  Submodule.map (g ^ l) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ≤
    s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k
⊢ Membership.mem (α := M) (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
    ((g ^ l : (a : M) → M) z : M)

Tactic:
exact this (Submodule.mem_map_of_mem hz)

Premises used: Submodule.mem_map_of_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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
refine_2 :
  Submodule.map (g ^ l) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ≤
    s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k
⊢ Membership.mem (α := M) (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
    ((g ^ l : (a : M) → M) z : M)

Tactic:
suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
          s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)
-- 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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
refine_2 :
  LE.le.{w} (α := Submodule R M) (⨆ i ∈ s, Submodule.map (g ^ l) ((f.genEigenspace i : (a : ℕ∞) → Submodule R M) k))
    (⨆ a ∈ s, (f.genEigenspace a : (a : ℕ∞) → Submodule R M) k)
⊢ Submodule.map (g ^ l) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ≤
    s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k

Tactic:
simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]

Premises used: Submodule.map_iSup, Finset.sup_eq_iSup
-- 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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
⊢ LE.le.{w} (α := Submodule R M) (⨆ i ∈ s, Submodule.map (g ^ l) ((f.genEigenspace i : (a : ℕ∞) → Submodule R M) k))
    (⨆ a ∈ s, (f.genEigenspace a : (a : ℕ∞) → Submodule R M) k)

Tactic:
iSup₂_mono fun μ _ ↦ ?_

Premises used: iSup₂_mono, Set.Mem, setOf
-- 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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
refine_2 :
  ∀ μ ∈ s,
    Submodule.map (g ^ l) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ≤
      (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k
⊢ LE.le.{w} (α := Submodule R M) (⨆ i ∈ s, Submodule.map (g ^ l) ((f.genEigenspace i : (a : ℕ∞) → Submodule R M) k))
    (⨆ a ∈ s, (f.genEigenspace a : (a : ℕ∞) → Submodule R M) k)

Tactic:
refine iSup₂_mono fun μ _ ↦ ?_

Premises used: iSup₂_mono
-- 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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
μ : R
h_1 : μ ∈ s
u : M
hu : u ∈ (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
⊢ Membership.mem (α := M) (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    ((g ^ l : (a : M) → M) u : M)

Tactic:
f.mapsTo_genEigenspace_of_comm ?_ μ k hu

Premises used: Module.End.mapsTo_genEigenspace_of_comm, 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
μ : R
h_1 : μ ∈ s
u : M
hu : u ∈ (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
refine_2 : Commute f (g ^ l)
⊢ Membership.mem (α := M) (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    ((g ^ l : (a : M) → M) u : M)

Tactic:
refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu

Premises used: Module.End.mapsTo_genEigenspace_of_comm
-- 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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
μ : R
h_1 : μ ∈ s
u : M
hu : u ∈ (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
⊢ Commute f (g ^ l)

Tactic:
Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l

Premises used: SemiconjBy, Commute, Algebra.mul_sub_algebraMap_pow_commutes
-- 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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
μ : R
h_1 : μ ∈ s
u : M
hu : u ∈ (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
⊢ Commute f (g ^ l)

Tactic:
exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l

Premises used: Algebra.mul_sub_algebraMap_pow_commutes
-- 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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
⊢ Membership.mem (α := M) (γ := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k ⊓
        s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    ((g ^ l : (a : M) → M) (y + z) : M)

Tactic:
have hyz : (g ^ l) (y + z) ∈
      (f.genEigenspace μ₁ k) ⊓ s.sup fun μ ↦ f.genEigenspace μ k := by
    refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩
    · exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
    · rw [SetLike.mem_coe, map_add, hl, zero_add]
      suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
          s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)
      simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
      refine iSup₂_mono fun μ _ ↦ ?_
      rintro - ⟨u, hu, rfl⟩
      refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
      exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
-- 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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
h : μ₂ ∉ s
hμ₁₂_1 : μ₁ ∉ Insert.insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
ih :
  Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
y z : M
hz : Membership.mem (γ := Submodule R M) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) z
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
g : End R M := f - HSMul.hSMul (β := End R M) μ₂ 1
hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
l : ℕ
hlk : (↑l : ℕ∞) ≤ k
hl : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)
hyz :
  Membership.mem (α := M) (γ := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k ⊓
        s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    ((g ^ l : (a : M) → M) (y + z) : M)
insert :
  ∀ (hyz : Membership.mem (α := M) (γ := Submodule R M) ⊥ ((g ^ l : (a : M) → M) (y + z) : M)),
    y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
insert₁ insert₂ insert₃ insert₄ :
  ∀ (hyz : Eq (α := M) ((g ^ l : (a : M) → M) (y + z) : M) (0 : M)),
    y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
⊢ y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker

Tactic:
rwa [ih.eq_bot, Submodule.mem_bot] at hyz

Premises used: Submodule.mem_bot, Disjoint.eq_bot
-- 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
k : ℕ∞
μ₁ : R
s : Finset R
empty :
  μ₁ ∉ ∅ →
    Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
      (Finset.sup ∅ fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
insert :
  ∀ (μ₂ : R) (s : Finset R),
    μ₂ ∉ s →
      ∀
        (ih :
          μ₁ ∉ s →
            Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
              (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)),
        μ₁ ∉ Insert.insert μ₂ s →
          Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
            ((Insert.insert μ₂ s).sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
⊢ μ₁ ∉ s →
    Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
      (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert μ₂ s _ ih =>
  intro hμ₁₂
  obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
  specialize ih hμ₁
  rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
  rintro x ⟨hx, hx'⟩
  simp only [SetLike.mem_coe] at hx hx'
  suffices x ∈ genEigenspace f μ₂ k by
    rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
    exact ⟨hx, this⟩
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
  let g := f - μ₂ • 1
  simp_rw [mem_genEigenspace, ← exists_prop] at hy ⊢
  peel hy with l hlk hl
  simp only [LinearMap.mem_ker] at hl
  have hyz : (g ^ l) (y + z) ∈
      (f.genEigenspace μ₁ k) ⊓ s.sup fun μ ↦ f.genEigenspace μ k := by
    refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩
    · exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
    · rw [SetLike.mem_coe, map_add, hl, zero_add]
      suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
          s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)
      simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
      refine iSup₂_mono fun μ _ ↦ ?_
      rintro - ⟨u, hu, rfl⟩
      refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
      exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
  rwa [ih.eq_bot, Submodule.mem_bot] at hyz

Premises used: Finset.sup_insert, Submodule.mem_bot, disjoint_iff, Insert.insert, exists_prop, LinearMap.mem_ker, SetLike.mem_coe, Submodule.eq_bot_iff, Module.End.mem_genEigenspace, 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
suffices suffices₁ suffices₂ suffices₃ :
  ∀ (μ₁ : R) (s : Finset R),
    μ₁ ∉ s →
      Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
        (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
⊢ iSupIndep.{v + 1, w} (α := Submodule R M) fun (x : R) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule R M) k

Tactic:
classical
  suffices ∀ μ₁ (s : Finset R), μ₁ ∉ s → Disjoint (f.genEigenspace μ₁ k)
    (s.sup fun μ ↦ f.genEigenspace μ k) by
    simp_rw [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase]
    exact fun s μ _ ↦ this _ _ (s.notMem_erase μ)
  intro μ₁ s
  induction s using Finset.induction_on with
  | empty => simp
  | insert μ₂ s _ ih =>
  intro hμ₁₂
  obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
  specialize ih hμ₁
  rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
  rintro x ⟨hx, hx'⟩
  simp only [SetLike.mem_coe] at hx hx'
  suffices x ∈ genEigenspace f μ₂ k by
    rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
    exact ⟨hx, this⟩
  obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx'
  let g := f - μ₂ • 1
  simp_rw [mem_genEigenspace, ← exists_prop] at hy ⊢
  peel hy with l hlk hl
  simp only [LinearMap.mem_ker] at hl
  have hyz : (g ^ l) (y + z) ∈
      (f.genEigenspace μ₁ k) ⊓ s.sup fun μ ↦ f.genEigenspace μ k := by
    refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩
    · exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
    · rw [SetLike.mem_coe, map_add, hl, zero_add]
      suffices (s.sup fun μ ↦ f.genEigenspace μ k).map (g ^ l) ≤
          s.sup fun μ ↦ f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz)
      simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
      refine iSup₂_mono fun μ _ ↦ ?_
      rintro - ⟨u, hu, rfl⟩
      refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
      exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l
  rwa [ih.eq_bot, Submodule.mem_bot] at hyz

Premises used: Finset.sup_insert, Submodule.mem_bot, disjoint_iff, Insert.insert, exists_prop, LinearMap.mem_ker, SetLike.mem_coe, Submodule.eq_bot_iff, Module.End.mem_genEigenspace, 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
⊢ iSupIndep f.maxGenEigenspace

Tactic:
apply independent_genEigenspace

Premises used: Module.End.independent_genEigenspace