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 : ℕ∞
this :
  ∀ (μ₁ : 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)
⊢ ∀ (s : Finset R),
    ∀ i ∈ s,
      Disjoint (α := Submodule R M) ((f.genEigenspace i : (a : ℕ∞) → Submodule R M) k : Submodule R M)
        ((s.erase i).sup fun (x : R) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)

Tactic:
exact fun s μ _ ↦ this _ _ (s.notMem_erase μ)
-- 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 :
  ∀ (μ₁ : 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:
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 μ)
-- 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
⊢ μ₁ ∉ ∅ →
    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)

Tactic:
simp
-- 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
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)
hμ₁₂ : μ₁ ∉ insert μ₂ s
rwa : ∀ (hμ₁₂ : ¬(μ₁ = μ₂ ∨ μ₁ ∈ s)), ¬μ₁ = μ₂ ∧ μ₁ ∉ s
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hμ₁₂ : ¬μ₁ = μ₂ ∧ μ₁ ∉ s), ¬μ₁ = μ₂ ∧ μ₁ ∉ s
⊢ ¬μ₁ = μ₂ ∧ μ₁ ∉ s

Tactic:
rwa [Finset.mem_insert, not_or] at hμ₁₂

Premises used: Finset.mem_insert, not_or
-- 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
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)
hμ₁₂ : μ₁ ∉ insert μ₂ s
⊢ μ₁ ≠ μ₂

Tactic:
obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
-- 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
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)
hμ₁₂ : μ₁ ∉ insert μ₂ s
hμ₁₃ : μ₁ ≠ μ₂
⊢ μ₁ ∉ s

Tactic:
obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
-- 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
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)
hμ₁₂_1 : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ 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:
specialize ih hμ₁
-- 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)
insert :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M)
        ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k ⊓
            ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
              s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) :
          Submodule R M)
        x →
      x = 0
⊢ 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)

Tactic:
rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]

Premises used: Finset.sup_insert, disjoint_iff, Submodule.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
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)
x : M
hx : x ∈ (↑((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
hx' :
  x ∈
    (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
            s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
          Submodule R M) :
      Set M)
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x

Tactic:
simp only [SetLike.mem_coe] at hx hx'

Premises used: 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)
x : M
hx : x ∈ (↑((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
hx' :
  x ∈
    (↑((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
            s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
          Submodule R M) :
      Set M)
hx₁ : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
⊢ Membership.mem (γ := Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
        s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    x

Tactic:
simp only [SetLike.mem_coe] at hx hx'

Premises used: 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)
x : M
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
        s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    x
this : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
rw :
  Membership.mem (γ := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    x
⊢ x = 0

Tactic:
rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]

Premises used: Submodule.mem_bot, Module.End.disjoint_genEigenspace, 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
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)
x : M
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
        s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    x
this : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
⊢ Membership.mem (γ := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    x

Tactic:
⟨hx, this⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- 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)
x : M
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
        s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    x
this : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
⊢ Membership.mem (γ := Submodule R M)
    ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    x

Tactic:
exact ⟨hx, this⟩
-- 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)
x : M
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
        s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    x
insert : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
⊢ x = 0

Tactic:
suffices x ∈ genEigenspace f μ₂ k by
    rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
    exact ⟨hx, this⟩
-- 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)
x : M
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
hx' :
  Membership.mem (γ := Submodule R M)
    ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
        s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
      Submodule R M)
    x
insert :
  ∀ (y : M)
    (hy : Membership.mem (γ := Submodule R M) ((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))
    (hx' :
      Membership.mem (γ := Submodule R M)
        ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k ⊔
            s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k :
          Submodule R M)
        (y + z)),
    Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'

Premises used: Iff.mp, Submodule.mem_sup, 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 : ℕ∞
μ₁ μ₂ : 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 : M
hy : Membership.mem (γ := Submodule R M) ((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
insert :
  ∀ (hy : ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker),
    ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)

Tactic:
simp_rw [mem_genEigenspace, ← exists_prop] at hy ⊢

Premises used: exists_prop, 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
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
insert :
  ∀ (l : ℕ) (hlk : (↑l : ℕ∞) ≤ k) (hl : y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker),
    y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
⊢ ∃ (l : ℕ) (_ : (↑l : ℕ∞) ≤ k), y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker

Tactic:
peel hy with l hlk hl
-- 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 : y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
⊢ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l : (a : M) → M) y : M) (0 : M)

Tactic:
simp only [LinearMap.mem_ker] at hl

Premises used: LinearMap.mem_ker
-- 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:
⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩

Premises used: Module.End.mapsTo_genEigenspace_of_comm, Set.Mem, setOf, Set.inter, And.intro
-- 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_1 : Commute f (g ^ l)
refine_2 :
  Membership.mem (α := M) (↑(s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) : Set M)
    ((g ^ l : (a : M) → M) (y + z) : 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:
refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k 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
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)
⊢ 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)
⊢ Commute f (g ^ l)

Tactic:
exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l

Premises used: Algebra.mul_sub_algebraMap_pow_commutes