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
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) (↑(s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) : Set M)
    ((g ^ l : (a : M) → M) (y + z) : M)
have 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)
Tactic: rw [SetLike.mem_coe, map_add, hl, zero_add]
-- 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
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) (s.sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
    ((g ^ l : (a : M) → M) z : M)
have 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
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)
-- 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
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)
⊢ 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
have 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)
Tactic: simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)]
-- 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
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)
have refine_2 : ∀ μ ∈ s,
  Submodule.map (g ^ l) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k) ≤
    (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k
Tactic: refine iSup₂_mono fun μ _ ↦ ?_
-- 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
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)
have refine_2 : Commute f (g ^ l)
Tactic: refine f.mapsTo_genEigenspace_of_comm ?_ μ k hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (hypothesis)
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)
⊢ y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
have 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)
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
-- 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
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)
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)
⊢ y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
have 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
Tactic: rwa [ih.eq_bot, Submodule.mem_bot] at hyz
Cleared hypotheses: hyz
-- 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
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
⊢ y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
have 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
Tactic: rwa [ih.eq_bot, Submodule.mem_bot] at hyz
Cleared hypotheses: hyz
-- 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
μ₁ : 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)
have 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)
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
Cleared hypotheses: s
-- 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
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)
⊢ μ₁ ∉ 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)
have 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 μ₂ s →
        Disjoint (α := Submodule R M) ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
          ((insert μ₂ 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
Cleared hypotheses: s
-- 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
inst_3 : IsDomain R
inst_4 : IsTorsionFree R M
f : End R M
k : ℕ∞
⊢ iSupIndep.{v + 1, w} (α := Submodule R M) fun (x : R) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule R M) k
have 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)
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
-- 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)
⊢ (genEigenspace (LinearMap.restrict f hfp) μ : (a : ℕ∞) → Submodule R ↥p) k =
    Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k)
have 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)
Tactic: ext x
-- 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 : ℕ∞))
⊢ 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 ∧ 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)
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)
⊢ 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 (γ := 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)
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)
⊢ 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 ∧ x ∈ Submodule.comap p.subtype ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞))) ↔
  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]