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
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
⊢ x ∈ f.genEigenrange μ (↑k : ℕ∞) ↔ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ k).range

Tactic:
simp only [genEigenrange, Nat.cast_le, Submodule.mem_iInf, LinearMap.mem_range]

Premises used: Submodule.mem_iInf, Module.End.genEigenrange, LinearMap.mem_range, Nat.cast_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
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
⊢ (∀ (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
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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

Tactic:
h _ le_rfl

Premises used: le_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
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

Tactic:
exact h _ le_rfl

Premises used: le_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
f : End R M
μ : R
k : ℕ
x : M
i : ℕ
hi : i ≤ k
⊢ k = i + (k - i)

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
⊢ k = i + (k - i)

Tactic:
have : k = i + (k - i) := by lia
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
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)
⊢ ∃ (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)

Tactic:
rw [this, pow_add]

Premises used: pow_add
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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) ^ i * (f - HSMul.hSMul (β := End R M) μ 1) ^ (k - i) : (a : M) → M) x : M)

Tactic:
⟨_, rfl⟩

Premises used: Exists.intro, 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
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) ^ i * (f - HSMul.hSMul (β := End R M) μ 1) ^ (k - i) : (a : M) → M) x : M)

Tactic:
exact ⟨_, 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
f : End R M
μ : R
h : f.HasUnifEigenvalue μ (↑0 : ℕ∞)
⊢ False

Tactic:
simp [HasUnifEigenvalue, Nat.cast_zero, genEigenspace_zero] at h

Premises used: Module.End.HasUnifEigenvalue, Nat.cast_zero, Module.End.genEigenspace_zero
-- 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 : IsNoetherian R M
f : End R M
μ : R
⊢ 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
-- 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 : 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))
⊢ iSup (ι := ℕ)
      (⇑((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom)) : (a : ℕ) → Submodule R M) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp (OrderEmbedding.toOrderHom WithTop.coeOrderHom))

Tactic:
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 : 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))
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)
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) ⊤ : Submodule R M)
    ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) : Submodule R M)

Tactic:
convert! this using 1
-- 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 : 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))
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)
⊢ 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:
simp only [genEigenspace, OrderHom.coe_mk, le_top, iSup_pos, OrderHom.comp_coe,
    Function.comp_def]

Premises used: iSup_pos, OrderHom.coe_mk, Function.comp_def, le_top, OrderHom.comp_coe, Module.End.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 : 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))
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))
⊢ 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:
rw [iSup_prod', iSup_subtype', ← sSup_range, ← sSup_range]

Premises used: iSup_subtype', iSup_prod', sSup_range
-- 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 : 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))
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)
⊢ 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:
congr 1
-- 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 : 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} (α := 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:
aesop
-- 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 : IsNoetherian R M
f : End R M
μ : R
k : ℕ∞
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)
⊢ 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)

Tactic:
rw [← genEigenspace_top_eq_maxUnifEigenspaceIndex]

Premises used: Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex
-- 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 : 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) ⊤ : Submodule R M)

Tactic:
(f.genEigenspace μ).monotone le_top

Premises used: OrderHom.monotone, Set.Mem, le_top, Module.End.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 : 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) ⊤ : Submodule R M)

Tactic:
exact (f.genEigenspace μ).monotone le_top

Premises used: OrderHom.monotone, le_top, Module.End.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 : IsNoetherian R M
f : End R M
μ : R
k : ℕ
hk : f.maxUnifEigenspaceIndex μ ≤ k
⊢ LE.le (α := ℕ∞) (↑(f.maxUnifEigenspaceIndex μ) : ℕ∞) (↑k : ℕ∞)

Tactic:
simpa using hk
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
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)
⊢ Ne (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) m : Submodule R M) (⊥ : Submodule R M)

Tactic:
contrapose hk
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
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)
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)

Tactic:
rw [← le_bot_iff, ← hk]

Premises used: le_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
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)
⊢ 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:
(f.genEigenspace _).monotone hm

Premises used: OrderHom.monotone, Set.Mem, Module.End.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
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)
⊢ 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:
exact (f.genEigenspace _).monotone hm

Premises used: OrderHom.monotone, Module.End.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
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
apply : f.HasUnifEigenvalue μ 1
⊢ f.HasUnifEigenvalue μ m

Tactic:
apply HasUnifEigenvalue.le (k := 1) (Order.one_le_iff_pos.mpr hm)

Premises used: Iff.mpr, Module.End.HasUnifEigenvalue.le, Order.one_le_iff_pos
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
apply : Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
⊢ False

Tactic:
apply hk
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
⊢ Function.Injective (α := M) (β := M) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)

Tactic:
rw [genEigenspace_one, LinearMap.ker_eq_bot] at contra

Premises used: LinearMap.ker_eq_bot, Module.End.genEigenspace_one
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
rw : LE.le (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)
⊢ Eq (α := Submodule R M) ((f.genEigenspace μ : (a : ℕ∞) → Submodule R M) k : Submodule R M) (⊥ : Submodule R M)

Tactic:
rw [eq_bot_iff]

Premises used: 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
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
⊢ ∃ (l : ℕ), (↑l : ℕ∞) ≤ k ∧ x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker

Tactic:
rw [mem_genEigenspace] at hx

Premises used: 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
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
rcases : ∀ (l : ℕ) (hx : x ∈ ((f - HSMul.hSMul (β := End R M) μ 1) ^ l).ker), Membership.mem (γ := Submodule R M) ⊥ x
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
rcases hx with ⟨l, -, 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
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
rwa : Function.Injective (α := M) (β := M) (⇑((f - HSMul.hSMul (β := End R M) μ 1) ^ l) : (a : M) → M)
⊢ Membership.mem (γ := Submodule R M) ⊥ x

Tactic:
rwa [LinearMap.ker_eq_bot.mpr] at hx

Premises used: Iff.mpr, LinearMap.ker_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
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
rw : Function.Injective (α := M) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)^[l]
⊢ Function.Injective (α := M) (β := M) (⇑((f - HSMul.hSMul (β := End R M) μ 1) ^ l) : (a : M) → M)

Tactic:
rw [Module.End.coe_pow (f - μ • 1) l]

Premises used: HSub.hSub, Module.End.coe_pow, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)^[l]

Tactic:
Function.Injective.iterate contra l

Premises used: Function.Injective.iterate
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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) (⇑(f - HSMul.hSMul (β := End R M) μ 1) : (a : M) → M)^[l]

Tactic:
exact Function.Injective.iterate contra l

Premises used: Function.Injective.iterate
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 : ℕ∞
hk : 0 < k
⊢ f.HasUnifEigenvalue μ k ↔ f.HasUnifEigenvalue μ 1

Tactic:
⟨HasUnifEigenvalue.lt zero_lt_one, HasUnifEigenvalue.lt hk⟩

Premises used: zero_lt_one, Iff.intro, Module.End.HasUnifEigenvalue.lt
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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
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)
⊢ f.maxUnifEigenspaceIndex μ ≤ finrank K V

Tactic:
apply Nat.sInf_le

Premises used: Nat.sInf_le
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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)
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)
⊢ 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)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.LinearAlgebra.Eigenspace.Basic
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 μ).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:
(f.genEigenspace μ).monotone <| WithTop.coeOrderHom.monotone hn

Premises used: OrderEmbedding.monotone, OrderHom.monotone, WithTop.coeOrderHom, Set.Mem, Module.End.genEigenspace