awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
this : IsNilpotent (f₂ - f₁)
⊢ False
have hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p) : (a : R) → End R ↥p) (μ₁ - μ₂)
Tactic: have hf₁₂ : f₂ - f₁ = algebraMap R (End R p) (μ₁ - μ₂) := by ext; simp [f₁, f₂]
-- 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
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k_1 l_1 : ℕ∞
k : ℕ
property : (↑k : ℕ∞) ≤ k_1
l : ℕ
property_1 : (↑l : ℕ∞) ≤ l_1
h : Nontrivial M
p : Submodule R M :=
  (f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) (↑k : ℕ∞) ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) (↑l : ℕ∞)
hp : Nontrivial.{w} ↥p
f₁ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₁ : End R M)) ⋯
f₂ : End R ↥p :=
  LinearMap.restrict (HSub.hSub (β := End R M) f ((algebraMap R (End R M) : (a : R) → End R M) μ₂ : End R M)) ⋯
this : IsNilpotent (f₂ - f₁)
hf₁₂ : f₂ - f₁ = (algebraMap R (End R ↥p) : (a : R) → End R ↥p) (μ₁ - μ₂)
⊢ False
have this₁ : μ₁ = μ₂
Tactic: rw [hf₁₂, IsNilpotent.map_iff (FaithfulSMul.algebraMap_injective R (End R p)),
    isNilpotent_iff_eq_zero, sub_eq_zero] at this
Cleared hypotheses: this, hf₁₂
-- 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
h :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₁
μ₂ : R
hμ₂ :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₂
hμ₁₂ :
  Eq.{w + 1} (α := Submodule R M)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₁)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₂)
⊢ μ₁ = μ₂
have by_contra : ∀ (contra : ¬μ₁ = μ₂), False
Tactic: by_contra contra
-- 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
h :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₁
μ₂ : R
hμ₂ :
  Membership.mem (γ := Set R)
    {μ : R |
      Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)}
    μ₂
hμ₁₂ :
  Eq.{w + 1} (α := Submodule R M)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₁)
    ((fun (x : R) ↦ ((f.genEigenspace x : (a : ℕ∞) → Submodule R M) k : Submodule R M)) μ₂)
contra : ¬μ₁ = μ₂
⊢ False
have apply : Eq (α := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
Tactic: apply hμ₂
-- 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 : ℕ∞
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)
⊢ iSupIndep.{v + 1, w} (α := Submodule R M) fun (x : R) ↦ (f.genEigenspace x : (a : ℕ∞) → Submodule R M) k
have simp_rw : ∀ (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: simp_rw [iSupIndep_iff_supIndep,
      Finset.supIndep_iff_disjoint_erase]
-- 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: 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 μ)
-- 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
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
⊢ ¬μ₁ = μ₂ ∧ μ₁ ∉ s
have rwa : ∀ (hμ₁₂ : ¬(μ₁ = μ₂ ∨ μ₁ ∈ s)), ¬μ₁ = μ₂ ∧ μ₁ ∉ s
Tactic: rwa [Finset.mem_insert, not_or] at hμ₁₂
-- 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
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
⊢ ¬μ₁ = μ₂ ∧ μ₁ ∉ s
have rwa₁ : ∀ (hμ₁₂ : ¬μ₁ = μ₂ ∧ μ₁ ∉ s), ¬μ₁ = μ₂ ∧ μ₁ ∉ s
Tactic: rwa [Finset.mem_insert, not_or] at hμ₁₂
-- 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
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
⊢ 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)
have hμ₁₃ : μ₁ ≠ μ₂
Tactic: obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
-- 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
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μ₁₃ : μ₁ ≠ μ₂
⊢ 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)
have hμ₁ : μ₁ ∉ s
Tactic: obtain ⟨hμ₁₂ : μ₁ ≠ μ₂, hμ₁ : μ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hμ₁₂
-- 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
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)
    ((insert μ₂ s).sup fun (μ : R) ↦ (f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
have 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)
Tactic: specialize ih hμ₁
Cleared hypotheses: ih
-- 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)
⊢ 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)
have 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
Tactic: rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff]
-- 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)
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)
⊢ x = 0
have hx₁ : 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'
Cleared hypotheses: hx, hx'
-- 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)
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
⊢ x = 0
have 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
Tactic: simp only [SetLike.mem_coe] at hx hx'
Cleared hypotheses: hx, hx'
-- 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)
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
⊢ x = 0
have rw : Membership.mem (γ := Submodule R M)
  ((f.genEigenspace μ₁ : (a : ℕ∞) → Submodule R M) k ⊓ (f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k :
    Submodule R M)
  x
Tactic: rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
-- 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)
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
⊢ x = 0
have insert : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
Tactic: suffices x ∈ genEigenspace f μ₂ k by
    rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
    exact ⟨hx, this⟩
-- 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)
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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
have 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)
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'
Cleared hypotheses: x, hx, hx'
-- 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 : 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
⊢ Membership.mem (γ := Submodule R M) ((f.genEigenspace μ₂ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (y + z)
have 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
Tactic: simp_rw [mem_genEigenspace, ← exists_prop] at hy ⊢
Cleared hypotheses: hy
-- 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 : ℕ) (_ : (↑l : ℕ∞) ≤ k), y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
have 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
Tactic: peel hy with l hlk hl
-- 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 : y ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
⊢ y + z ∈ ((f - HSMul.hSMul (β := End R M) μ₂ 1) ^ l).ker
have hl₁ : 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
Cleared hypotheses: hl
-- 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)
    ((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)
have refine_1 : Commute f (g ^ l)
Tactic: refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩
-- 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)
refine_1 : Commute f (g ^ l)
⊢ 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)
have 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)
Tactic: refine ⟨f.mapsTo_genEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩