awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker = (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1).ker
have rw : (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker = (f - HSMul.hSMul (β := End K V) (b⁻¹ * a) 1).ker
Tactic: rw [smul_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1).ker = (b • (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1)).ker
have rw : (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1).ker = LinearMap.ker (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1)
Tactic: rw [LinearMap.ker_smul _ b hb]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
a b : K
hb : b ≠ 0
⊢ (b • (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1)).ker = (b • f - HSMul.hSMul (β := End K V) a 1).ker
have rw : LinearMap.ker (b • f - b • b⁻¹ • HSMul.hSMul (β := End K V) a 1) = (b • f - HSMul.hSMul (β := End K V) a 1).ker
Tactic: rw [smul_sub, smul_inv_smul₀ hb]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
f : End K V
a b : K
hb : b ≠ 0
rw : LinearMap.ker (b • f - b • b⁻¹ • HSMul.hSMul (β := End K V) a 1) = (b • f - HSMul.hSMul (β := End K V) a 1).ker
⊢ (b • (f - b⁻¹ • HSMul.hSMul (β := End K V) a 1)).ker = (b • f - HSMul.hSMul (β := End K V) a 1).ker
have rw₁ : LinearMap.ker (b • f - HSMul.hSMul (β := End K V) a 1) = (b • f - HSMul.hSMul (β := End K V) a 1).ker
Tactic: rw [smul_sub, smul_inv_smul₀ hb]
-- 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
μ : R
k : ℕ
⊢ f.genEigenrange μ (↑k : ℕ∞) = ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).range
have h : ∀ (x : M), x ∈ f.genEigenrange μ (↑k : ℕ∞) ↔ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).range
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
μ : R
k : ℕ
x : M
⊢ x ∈ f.genEigenrange μ (↑k : ℕ∞) ↔ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).range
have h : (∀ (i : ℕ) (i_1 : i ≤ k), ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ i : (a : M) → M) y = x) ↔
  ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) y = x
Tactic: simp only [genEigenrange, Nat.cast_le, Submodule.mem_iInf, LinearMap.mem_range]
-- 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
μ : R
k : ℕ
x : M
⊢ (∀ (i : ℕ) (i_1 : i ≤ k), ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ i : (a : M) → M) y = x) ↔
    ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) y = x
have h : (∀ (i : ℕ) (i_1 : i ≤ k), ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ i : (a : M) → M) y = x) →
  ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) y = x
Tactic: constructor
-- 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
μ : R
k : ℕ
x : M
h :
  (∀ (i : ℕ) (i_1 : i ≤ k), ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ i : (a : M) → M) y = x) →
    ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) y = x
⊢ (∀ (i : ℕ) (i_1 : i ≤ k), ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ i : (a : M) → M) y = x) ↔
    ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) y = x
have h₁ : (∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) y = x) →
  ∀ (i : ℕ) (i_1 : i ≤ k), ∃ (y : M), ((f - HSMul.hSMul (β := End R M) μ 1) ^ i : (a : M) → M) y = x
Tactic: constructor
-- 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
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
⊢ ∃ (y : M),
    Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ i : (a : M) → M) y : M)
      (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M)
have this : k = i + (k - i)
Tactic: have : k = i + (k - i) := by lia
-- 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
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
this : k = i + (k - i)
⊢ ∃ (y : M),
    Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ i : (a : M) → M) y : M)
      (((f - HSMul.hSMul (β := End R M) μ 1) ^ k : (a : M) → M) x : M)
have h : ∃ (y : M),
  Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ i : (a : M) → M) y : M)
    (((f - HSMul.hSMul (β := End R M) μ 1) ^ i * (f - HSMul.hSMul (β := End R M) μ 1) ^ (k - i) : (a : M) → M) x : M)
Tactic: rw [this, pow_add]
-- 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 : IsNoetherian R M
f : End R M
μ : R
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M)
have this : iSup (ι := ℕ) (⇑((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom)) : (a : ℕ) → Submodule R M) =
  monotonicSequenceLimit ((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom))
Tactic: have := WellFoundedGT.iSup_eq_monotonicSequenceLimit <|
    (f.genEigenspace μ).comp <| WithTop.coeOrderHom.toOrderHom
-- 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 : IsNoetherian R M
f : End R M
μ : R
this :
  iSup (ι := ℕ)
      (⇑((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom)) : (a : ℕ) → Submodule R M) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom))
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M)
have h : Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
  (iSup (ι := ℕ)
      (⇑((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom)) : (a : ℕ) → Submodule R M) :
    Submodule R M)
Tactic: convert! this using 1
-- 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 : IsNoetherian R M
f : End R M
μ : R
this :
  iSup (ι := ℕ)
      (⇑((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom)) : (a : ℕ) → Submodule R M) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom))
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
    (iSup (ι := ℕ)
        (⇑((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom)) : (a : ℕ) → Submodule R M) :
      Submodule R M)
have h : Eq.{w + 1} (α := Submodule R M) (⨆ (l : ℕ), ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker)
  (⨆ (x : ℕ),
    ⨆ (l : ℕ),
      ⨆ (_ : LE.le (α := ℕ∞) ((↑l : ℕ∞) : ℕ∞) ((OrderEmbedding.toOrderHom WithTop.coeOrderHom : (a : ℕ) → ℕ∞) x : ℕ∞)),
        ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker)
Tactic: simp only [genEigenspace, OrderHom.coe_mk, le_top, iSup_pos, OrderHom.comp_coe,
    Function.comp_def]
-- 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 : IsNoetherian R M
f : End R M
μ : R
this :
  iSup (ι := ℕ)
      (⇑((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom)) : (a : ℕ) → Submodule R M) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom))
⊢ Eq.{w + 1} (α := Submodule R M) (⨆ (l : ℕ), ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker)
    (⨆ (x : ℕ),
      ⨆ (l : ℕ),
        ⨆ (_ :
          LE.le (α := ℕ∞) ((↑l : ℕ∞) : ℕ∞) ((OrderEmbedding.toOrderHom WithTop.coeOrderHom : (a : ℕ) → ℕ∞) x : ℕ∞)),
          ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker)
have h : Eq.{w + 1} (α := Submodule R M) (sSup (range fun (l : ℕ) ↦ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker))
  (sSup
    (range
      fun
        (x :
          { x : ℕ × ℕ //
            LE.le (α := ℕ∞) ((↑x.2 : ℕ∞) : ℕ∞)
              ((OrderEmbedding.toOrderHom WithTop.coeOrderHom : (a : ℕ) → ℕ∞) x.1 : ℕ∞) }) ↦
      ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑x : ℕ × ℕ).2).ker))
Tactic: rw [iSup_prod', iSup_subtype', ← sSup_range, ← sSup_range]
-- 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 : IsNoetherian R M
f : End R M
μ : R
this :
  iSup (ι := ℕ)
      (⇑((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom)) : (a : ℕ) → Submodule R M) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom))
⊢ Eq.{w + 1} (α := Submodule R M) (sSup (range fun (l : ℕ) ↦ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker))
    (sSup
      (range
        fun
          (x :
            { x : ℕ × ℕ //
              LE.le (α := ℕ∞) ((↑x.2 : ℕ∞) : ℕ∞)
                ((OrderEmbedding.toOrderHom WithTop.coeOrderHom : (a : ℕ) → ℕ∞) x.1 : ℕ∞) }) ↦
        ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑x : ℕ × ℕ).2).ker))
have h : Eq.{w + 1} (α := Set (Submodule R M)) (range fun (l : ℕ) ↦ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker)
  (range
    fun
      (x :
        { x : ℕ × ℕ //
          LE.le (α := ℕ∞) ((↑x.2 : ℕ∞) : ℕ∞)
            ((OrderEmbedding.toOrderHom WithTop.coeOrderHom : (a : ℕ) → ℕ∞) x.1 : ℕ∞) }) ↦
    ((f - HSMul.hSMul (β := End R M) μ 1) ^ (↑x : ℕ × ℕ).2).ker)
Tactic: congr 1
-- 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 : IsNoetherian R M
f : End R M
μ : R
k : ℕ∞
⊢ LE.le (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M)
have rw : LE.le (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
  ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
Tactic: rw [← genEigenspace_top_eq_maxUnifEigenspaceIndex]
-- 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
μ : R
k m : ℕ∞
hm : k ≤ m
hk : Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
⊢ Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) m : Submodule R M) (⊥ : Submodule R M)
have contrapose : ∀ (hk : Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) m : Submodule R M) (⊥ : Submodule R M)),
  Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
Tactic: contrapose hk
Cleared hypotheses: hk
-- 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
μ : R
k m : ℕ∞
hm : k ≤ m
hk : Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) m : Submodule R M) (⊥ : Submodule R M)
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
have rw : LE.le (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M)
  ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) m : Submodule R M)
Tactic: rw [← le_bot_iff, ← hk]
-- 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
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ m
have apply : f.HasUnifEigenvalue μ 1
Tactic: apply HasUnifEigenvalue.le (k := 1) (Order.one_le_iff_pos.mpr hm)
-- 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
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) (⊥ : Submodule R M)
⊢ False
have apply : Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
Tactic: apply hk
-- 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
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) 1 : Submodule R M) (⊥ : Submodule R M)
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
have contra₁ : Function.Injective (α := M) (β := M) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
Tactic: rw [genEigenspace_one, LinearMap.ker_eq_bot] at contra
Cleared hypotheses: 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
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective (α := M) (β := M) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
have rw : LE.le (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
Tactic: rw [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
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective (α := M) (β := M) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
x : M
hx : Membership.mem (γ := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) x
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have hx₁ : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
Tactic: rw [mem_genEigenspace] at hx
Cleared hypotheses: 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
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective (α := M) (β := M) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
x : M
hx : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have rcases : ∀ (l : ℕ) (hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker), Membership.mem (γ := Submodule R M) ⊥ x
Tactic: rcases hx with ⟨l, -, hx⟩
Cleared hypotheses: 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
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective (α := M) (β := M) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
x : M
l : ℕ
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ Membership.mem (γ := Submodule R M) ⊥ x
have rwa : Function.Injective (α := M) (β := M) (⇑((f - HSMul.hSMul (β := End R M) μ 1) ^ l) : (a : M) → M)
Tactic: rwa [LinearMap.ker_eq_bot.mpr] at 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
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
contra : Function.Injective (α := M) (β := M) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)
x : M
l : ℕ
hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker
⊢ Function.Injective (α := M) (β := M) (⇑((f - HSMul.hSMul (β := End R M) μ 1) ^ l) : (a : M) → M)
have rw : Function.Injective (α := M) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)^[l]
Tactic: rw [Module.End.coe_pow (f - μ • 1) l]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
⊢ f.maxUnifEigenspaceIndex μ ≤ finrank K V
have hm : Membership.mem (γ := Set ℕ)
  {n : ℕ |
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Submodule K V)
          (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) n :
            Submodule K V)
          (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) m :
            Submodule K V)}
  (finrank K V)
Tactic: apply Nat.sInf_le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ Eq (α := Submodule K V)
    (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V)
        (finrank K V) :
      Submodule K V)
    (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) n :
      Submodule K V)
have hm : LE.le (α := Submodule K V)
  (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) (finrank K V) :
    Submodule K V)
  (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) n :
    Submodule K V)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
hm :
  LE.le (α := Submodule K V)
    (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V)
        (finrank K V) :
      Submodule K V)
    (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) n :
      Submodule K V)
⊢ Eq (α := Submodule K V)
    (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V)
        (finrank K V) :
      Submodule K V)
    (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) n :
      Submodule K V)
have hm₁ : LE.le (α := Submodule K V)
  (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) n :
    Submodule K V)
  (((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom) : (a : ℕ) → Submodule K V) (finrank K V) :
    Submodule K V)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
n : ℕ
hn : finrank K V ≤ n
⊢ LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑n : ℕ∞) : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
have hm : ((f - HSMul.hSMul (β := End K V) μ 1) ^ n).ker ≤ ((f - HSMul.hSMul (β := End K V) μ 1) ^ finrank K V).ker
Tactic: rw [genEigenspace_nat, genEigenspace_nat]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤ : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
have rw : LE.le (α := Submodule K V)
  ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule K V)
  ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
Tactic: rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Eigenspace.Basic (goal)
Goal:
K : Type v
V : Type w
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
f : End K V
μ : K
k : ℕ∞
⊢ LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) k : Submodule K V)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
have calc : LE.le (α := Submodule K V) ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) ⊤ : Submodule K V)
  ((f.genEigenspace μ : (a : ℕ∞) → Submodule K V) (↑(finrank K V) : ℕ∞) : Submodule K V)
Tactic: calc f.genEigenspace μ k
      ≤ f.genEigenspace μ ⊤ := (f.genEigenspace _).monotone le_top
    _ ≤ f.genEigenspace μ (finrank K V) := by
      rw [genEigenspace_top_eq_maxUnifEigenspaceIndex]
      exact (f.genEigenspace _).monotone <| by simpa using maxUnifEigenspaceIndex_le_finrank f μ
-- 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 g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
hx : x ∈ (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
⊢ Membership.mem (α := M) (↑((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) : Set M)
    ((g : (a : M) → M) x : M)
have simp : ∀
  (hx :
    ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)),
  ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
Tactic: simp only [SetLike.mem_coe, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢
Cleared hypotheses: 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
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
hx : ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
have rcases : ∀ (l : ℕ) (hl : (↑l : ℕ∞) ≤ k)
  (hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)),
  ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
Tactic: rcases hx with ⟨l, hl, hx⟩
Cleared hypotheses: 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
f g : End R M
h : Commute f g
μ : R
k : ℕ∞
x : M
l : ℕ
hl : (↑l : ℕ∞) ≤ k
hx : Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) x : M) (0 : M)
⊢ ∃ (l : ℕ),
    (↑l : ℕ∞) ≤ k ∧
      Eq (α := M) (((f - HSMul.hSMul (β := End R M) μ 1) ^ l : (a : M) → M) ((g : (a : M) → M) x : M) : M) (0 : M)
have h₁ : Commute ((f - HSMul.hSMul (β := End R M) μ 1) ^ l) g
Tactic: replace h : Commute ((f - μ • (1 : End R M)) ^ l) g :=
    (h.sub_left <| Algebra.commute_algebraMap_left μ g).pow_left l
Cleared hypotheses: h