awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type (max 0 u_2) := { N : Submodule R M // N.FG }
H : WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ :
  ∀ (x : { N : Submodule R M // N.FG }),
    Membership.mem (γ := Set { N : Submodule R M // N.FG }) {N' : α | (↑N' : Submodule R M) ≤ N} x →
      ¬Subtype.mk (p := fun (N : Submodule R M) ↦ N.FG) N₀ h₁ < x
h : ∀ (h₃ : ¬N ≤ N₀), False
⊢ N ≤ N₀

Tactic:
by_contra h₃
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type (max 0 u_2) := { N : Submodule R M // N.FG }
H : WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ :
  ∀ (x : { N : Submodule R M // N.FG }),
    Membership.mem (γ := Set { N : Submodule R M // N.FG }) {N' : α | (↑N' : Submodule R M) ≤ N} x →
      ¬Subtype.mk (p := fun (N : Submodule R M) ↦ N.FG) N₀ h₁ < x
h₃ : ¬N ≤ N₀
h : ∀ (x : M) (hx₁ : x ∈ N) (hx₂ : x ∉ N₀), False
⊢ False

Tactic:
obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := Set.not_subset.mp h₃

Premises used: Set.not_subset, Iff.mp
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type (max 0 u_2) := { N : Submodule R M // N.FG }
H : WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ :
  ∀ (x : { N : Submodule R M // N.FG }),
    Membership.mem (γ := Set { N : Submodule R M // N.FG }) {N' : α | (↑N' : Submodule R M) ≤ N} x →
      ¬Subtype.mk (p := fun (N : Submodule R M) ↦ N.FG) N₀ h₁ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
h : x ∈ N₀
⊢ False

Tactic:
apply hx₂
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type (max 0 u_2) := { N : Submodule R M // N.FG }
H : WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ :
  ∀ (x : { N : Submodule R M // N.FG }),
    Membership.mem (γ := Set { N : Submodule R M // N.FG }) {N' : α | (↑N' : Submodule R M) ≤ N} x →
      ¬Subtype.mk (p := fun (N : Submodule R M) ↦ N.FG) N₀ h₁ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
rw rw₁ : Eq (α := Submodule R M) (R ∙ x) (R ∙ x)
⊢ Eq (α := Submodule R M) (span R (↑{x} : Set M)) (R ∙ x)

Tactic:
rw [Finset.coe_singleton]

Premises used: Finset.coe_singleton
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type (max 0 u_2) := { N : Submodule R M // N.FG }
H : WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ :
  ∀ (x : { N : Submodule R M // N.FG }),
    Membership.mem (γ := Set { N : Submodule R M // N.FG }) {N' : α | (↑N' : Submodule R M) ≤ N} x →
      ¬Subtype.mk (p := fun (N : Submodule R M) ↦ N.FG) N₀ h₁ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
h : x ∈ R ∙ x ⊔ N₀
⊢ x ∈ N₀

Tactic:
rw [eq_of_le_of_not_lt (le_sup_right : N₀ ≤ _) (h₂
      ⟨_, Submodule.FG.sup ⟨{x}, by rw [Finset.coe_singleton]⟩ h₁⟩ <|
      sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e)]

Premises used: Iff.mpr, le_sup_right, Subtype.mk, Exists.intro, sup_le, Submodule.span_singleton_le_iff_mem, Submodule.FG.sup, Singleton.singleton, eq_of_le_of_not_lt
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type (max 0 u_2) := { N : Submodule R M // N.FG }
H : WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ :
  ∀ (x : { N : Submodule R M // N.FG }),
    Membership.mem (γ := Set { N : Submodule R M // N.FG }) {N' : α | (↑N' : Submodule R M) ≤ N} x →
      ¬Subtype.mk (p := fun (N : Submodule R M) ↦ N.FG) N₀ h₁ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ R ∙ x ⊔ N₀

Tactic:
(le_sup_left : R ∙ x ≤ _) (Submodule.mem_span_singleton_self _)

Premises used: le_sup_left, Submodule.mem_span_singleton_self
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type (max 0 u_2) := { N : Submodule R M // N.FG }
H : WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
N N₀ : Submodule R M
h₁ : N₀.FG
e : N₀ ≤ N
h₂ :
  ∀ (x : { N : Submodule R M // N.FG }),
    Membership.mem (γ := Set { N : Submodule R M // N.FG }) {N' : α | (↑N' : Submodule R M) ≤ N} x →
      ¬Subtype.mk (p := fun (N : Submodule R M) ↦ N.FG) N₀ h₁ < x
h₃ : ¬N ≤ N₀
x : M
hx₁ : x ∈ N
hx₂ : x ∉ N₀
⊢ x ∈ R ∙ x ⊔ N₀

Tactic:
exact (le_sup_left : R ∙ x ≤ _) (Submodule.mem_span_singleton_self _)

Premises used: le_sup_left, Submodule.mem_span_singleton_self
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔
    WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2
rw₁ rw₂ :
  (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔
    ∀ (s : Set (Submodule R M)), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬x > m
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M

Tactic:
rw [isNoetherian_iff, WellFounded.wellFounded_iff_has_min]

Premises used: WellFounded.wellFounded_iff_has_min, isNoetherian_iff
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw :
  (∀ (f : ℕ →o Submodule R M),
      ∃ (n : ℕ),
        ∀ (m : ℕ),
          n ≤ m →
            Eq (α := Submodule R M) ((f : (a : ℕ) → Submodule R M) n : Submodule R M)
              ((f : (a : ℕ) → Submodule R M) m : Submodule R M)) ↔
    WellFoundedGT.{u_2} (Submodule R M)
rw₁ rw₂ :
  (∀ (f : ℕ →o Submodule R M),
      ∃ (n : ℕ),
        ∀ (m : ℕ),
          n ≤ m →
            Eq (α := Submodule R M) ((f : (a : ℕ) → Submodule R M) n : Submodule R M)
              ((f : (a : ℕ) → Submodule R M) m : Submodule R M)) ↔
    ∀ (a : ℕ →o Submodule R M),
      ∃ (n : ℕ),
        ∀ (m : ℕ),
          n ≤ m →
            Eq (α := Submodule R M) ((a : (a : ℕ) → Submodule R M) n : Submodule R M)
              ((a : (a : ℕ) → Submodule R M) m : Submodule R M)
⊢ (∀ (f : ℕ →o Submodule R M),
      ∃ (n : ℕ),
        ∀ (m : ℕ),
          n ≤ m →
            Eq (α := Submodule R M) ((f : (a : ℕ) → Submodule R M) n : Submodule R M)
              ((f : (a : ℕ) → Submodule R M) m : Submodule R M)) ↔
    IsNoetherian R M

Tactic:
rw [isNoetherian_iff', wellFoundedGT_iff_monotone_chain_condition]

Premises used: isNoetherian_iff', wellFoundedGT_iff_monotone_chain_condition
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
obtain :
  ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)),
    ∀ᶠ (n : ℕ) in atTop, Disjoint (f ^ n).ker (f ^ n).range
⊢ ∀ᶠ (n : ℕ) in atTop, Disjoint (f ^ n).ker (f ^ n).range

Tactic:
obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)⟩ :=
    monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer

Premises used: Iff.mpr, inferInstance, monotone_stabilizes_iff_noetherian, LinearMap.iterateKer
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
⊢ ∀ᶠ (n : ℕ) in atTop, Disjoint (f ^ n).ker (f ^ n).range

Tactic:
eventually_atTop.mpr ⟨n, fun m hm ↦ disjoint_iff.mpr ?_⟩

Premises used: Iff.mpr, disjoint_iff, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
refine : ∀ (m : ℕ) (hm : m ≥ n), (f ^ m).ker ⊓ (f ^ m).range = ⊥
⊢ ∀ᶠ (n : ℕ) in atTop, Disjoint (f ^ n).ker (f ^ n).range

Tactic:
refine eventually_atTop.mpr ⟨n, fun m hm ↦ disjoint_iff.mpr ?_⟩

Premises used: Iff.mpr, disjoint_iff, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : m ≥ n
rw : ∀ x ∈ LinearMap.ker (f ^ n) ⊓ (f ^ m).range, x = 0
⊢ (f ^ m).ker ⊓ (f ^ m).range = ⊥

Tactic:
rw [← hn _ hm, Submodule.eq_bot_iff]

Premises used: Submodule.eq_bot_iff
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : m ≥ n
x : M
hx : Membership.mem (α := M) (↑(LinearMap.ker (f ^ n)) : Set M) ((f ^ m : (a : M) → M) x : M)
apply : Eq (α := M) ((f ^ n : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((f ^ m : (a : M) → M) x : M) (0 : M)

Tactic:
apply pow_map_zero_of_le hm

Premises used: Module.End.pow_map_zero_of_le
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : m ≥ n
x : M
hx : Membership.mem (α := M) (↑(LinearMap.ker (f ^ n)) : Set M) ((f ^ m : (a : M) → M) x : M)
⊢ x ∈ LinearMap.ker (f ^ (n + m))

Tactic:
simpa [f.pow_apply n, f.pow_apply m, ← f.pow_apply (n + m), ← iterate_add_apply] using hx

Premises used: Function.iterate_add_apply, Module.End.pow_apply, HAdd.hAdd
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : m ≥ n
x : M
hx : Membership.mem (α := M) (↑(LinearMap.ker (f ^ n)) : Set M) ((f ^ m : (a : M) → M) x : M)
⊢ x ∈ LinearMap.ker (f ^ (n + m))

Tactic:
replace hx : x ∈ LinearMap.ker (f ^ (n + m)) := by
    simpa [f.pow_apply n, f.pow_apply m, ← f.pow_apply (n + m), ← iterate_add_apply] using hx
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : End R M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)
m : ℕ
hm : m ≥ n
x : M
hx : x ∈ LinearMap.ker (f ^ (n + m))
rwa rwa₁ rwa₂ rwa₃ : ∀ (hx : x ∈ LinearMap.ker (f ^ n)), Eq (α := M) ((f ^ n : (a : M) → M) x : M) (0 : M)
⊢ Eq (α := M) ((f ^ n : (a : M) → M) x : M) (0 : M)

Tactic:
rwa [← hn _ (n.le_add_right m)] at hx

Premises used: Nat.le_add_right
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
obtain :
  ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker),
    ∀ᶠ (n : ℕ) in atTop, ⨆ (m : ℕ), (f ^ m).ker = (f ^ n).ker
⊢ ∀ᶠ (n : ℕ) in atTop, ⨆ (m : ℕ), (f ^ m).ker = (f ^ n).ker

Tactic:
obtain ⟨n, hn : ∀ m, n ≤ m → ker (f ^ n) = ker (f ^ m)⟩ :=
    monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer

Premises used: Iff.mpr, inferInstance, monotone_stabilizes_iff_noetherian, LinearMap.iterateKer
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
⊢ ∀ᶠ (n : ℕ) in atTop, ⨆ (m : ℕ), (f ^ m).ker = (f ^ n).ker

Tactic:
eventually_atTop.mpr ⟨n, fun m hm ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
refine : ∀ (m : ℕ) (hm : m ≥ n), ⨆ (m : ℕ), (f ^ m).ker = (f ^ m).ker
⊢ ∀ᶠ (n : ℕ) in atTop, ⨆ (m : ℕ), (f ^ m).ker = (f ^ n).ker

Tactic:
refine eventually_atTop.mpr ⟨n, fun m hm ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : m ≥ n
⊢ ⨆ (m : ℕ), (f ^ m).ker = (f ^ m).ker

Tactic:
le_antisymm (iSup_le fun l ↦ ?_) (le_iSup (fun i ↦ LinearMap.ker (f ^ i)) m)

Premises used: LinearMap.ker, le_iSup, le_antisymm, HPow.hPow, iSup_le
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : m ≥ n
refine : ∀ (l : ℕ), (f ^ l).ker ≤ (f ^ m).ker
⊢ ⨆ (m : ℕ), (f ^ m).ker = (f ^ m).ker

Tactic:
refine le_antisymm (iSup_le fun l ↦ ?_) (le_iSup (fun i ↦ LinearMap.ker (f ^ i)) m)

Premises used: LinearMap.ker, le_iSup, le_antisymm, HPow.hPow, iSup_le
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : m ≥ n
l : ℕ
inl : ∀ (h : m ≤ l), (f ^ l).ker ≤ (f ^ m).ker
inr : ∀ (h : l < m), (f ^ l).ker ≤ (f ^ m).ker
⊢ (f ^ l).ker ≤ (f ^ m).ker

Tactic:
rcases le_or_gt m l with h | h

Premises used: le_or_gt
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : m ≥ n
l : ℕ
h : m ≤ l
inl : (f ^ n).ker ≤ (f ^ m).ker
inl₁ inl₂ : (f ^ m).ker ≤ (f ^ m).ker
⊢ (f ^ l).ker ≤ (f ^ m).ker

Tactic:
rw [← hn _ (hm.trans h), hn _ hm]

Premises used: LE.le.trans
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : m ≥ n
l : ℕ
h : l < m
⊢ (f ^ l).ker ≤ (f ^ m).ker

Tactic:
f.iterateKer.monotone h.le

Premises used: OrderHom.monotone, Set.Mem, LT.lt.le, LinearMap.iterateKer
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : M →ₗ[R] M
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).ker
m : ℕ
hm : m ≥ n
l : ℕ
h : l < m
⊢ (f ^ l).ker ≤ (f ^ m).ker

Tactic:
exact f.iterateKer.monotone h.le

Premises used: OrderHom.monotone, LT.lt.le, LinearMap.iterateKer
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
inst : Semiring R
⊢ IsNoetherianRing R ↔ IsNoetherian R R

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
inst : Semiring R
⊢ IsNoetherianRing R ↔ ∀ (I : Ideal R), I.FG

Tactic:
isNoetherianRing_iff.trans isNoetherian_def

Premises used: isNoetherianRing_iff, isNoetherian_def, Iff.trans
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
inst : Semiring R
inst_1 : IsNoetherianRing R
I : Ideal R
⊢ I.FG

Tactic:
IsNoetherian.noetherian _

Premises used: IsNoetherian.noetherian, Submodule.FG, Ideal.FG
-- Module: Mathlib.RingTheory.Noetherian.Filter
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : ℕ →o Submodule R M
simp_rw :
  ∃ (i : ℕ),
    ∀ (j : ℕ),
      i ≤ j →
        Eq (α := Submodule R M) ((f : (a : ℕ) → Submodule R M) i : Submodule R M)
          ((f : (a : ℕ) → Submodule R M) j : Submodule R M)
⊢ EventuallyConst (α := ℕ) (β := Submodule R M) (⇑f : (a : ℕ) → Submodule R M) atTop

Tactic:
simp_rw [eventuallyConst_atTop, eq_comm]

Premises used: Filter.eventuallyConst_atTop, eq_comm
-- Module: Mathlib.RingTheory.Noetherian.Filter
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ ∃ (i : ℕ),
    ∀ (j : ℕ),
      i ≤ j →
        Eq (α := Submodule R M) ((f : (a : ℕ) → Submodule R M) i : Submodule R M)
          ((f : (a : ℕ) → Submodule R M) j : Submodule R M)

Tactic:
(monotone_stabilizes_iff_noetherian.mpr inferInstance) f

Premises used: Iff.mpr, inferInstance, monotone_stabilizes_iff_noetherian
-- Module: Mathlib.RingTheory.Noetherian.Filter
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : IsNoetherian R M
f : ℕ →o Submodule R M
⊢ ∃ (i : ℕ),
    ∀ (j : ℕ),
      i ≤ j →
        Eq (α := Submodule R M) ((f : (a : ℕ) → Submodule R M) i : Submodule R M)
          ((f : (a : ℕ) → Submodule R M) j : Submodule R M)

Tactic:
exact (monotone_stabilizes_iff_noetherian.mpr inferInstance) f

Premises used: Iff.mpr, inferInstance, monotone_stabilizes_iff_noetherian
-- Module: Mathlib.RingTheory.Noetherian.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsNoetherianRing R
obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := Ideal R) (Ideal.radical ⊥) n ≤ ⊥), IsNilpotent (R := Ideal R) (nilradical R)
⊢ IsNilpotent (R := Ideal R) (nilradical R)

Tactic:
obtain ⟨n, hn⟩ := Ideal.exists_radical_pow_le_of_fg (⊥ : Ideal R) (IsNoetherian.noetherian _)

Premises used: Ideal.exists_radical_pow_le_of_fg, IsNoetherian.noetherian, Bot.bot
-- Module: Mathlib.RingTheory.Noetherian.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsNoetherianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.radical ⊥) n ≤ ⊥
⊢ IsNilpotent (R := Ideal R) (nilradical R)

Tactic:
⟨n, eq_bot_iff.mpr hn⟩

Premises used: Iff.mpr, Exists.intro, eq_bot_iff, IsNilpotent
-- Module: Mathlib.RingTheory.Noetherian.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsNoetherianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.radical ⊥) n ≤ ⊥
⊢ IsNilpotent (R := Ideal R) (nilradical R)

Tactic:
exact ⟨n, eq_bot_iff.mpr hn⟩
-- Module: Mathlib.RingTheory.Noetherian.Nilpotent
Goal:
R : Type u_1
inst : CommSemiring R
I : Ideal R
hI : I.FG
⊢ IsNilpotent I ↔ I ≤ nilradical R

Tactic:
⟨fun ⟨n, hn⟩ _ hx ↦ ⟨n, hn ▸ Ideal.pow_mem_pow hx n⟩,
    fun h ↦ let ⟨n, hn⟩ := exists_pow_le_of_le_radical_of_fg h hI; ⟨n, le_bot_iff.mp hn⟩⟩

Premises used: le_bot_iff, Ideal.exists_pow_le_of_le_radical_of_fg, Membership.mem, _private.0.Ideal.FG.isNilpotent_iff_le_nilradical.match_1, Eq.rec, Iff.intro, Exists.intro, Iff.mp, Ideal.pow_mem_pow, IsNilpotent, _private.0.Ideal.FG.isNilpotent_iff_le_nilradical.match_2, nilradical
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := Ideal R) (span (↑{1} : Set R)) ⊤

Tactic:
simp
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
obtain : ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}), I.FG
⊢ I.FG

Tactic:
obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup

Premises used: Submodule.fg_iff_exists_fin_generating_family, Iff.mp
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : Submodule.span R (Set.range f) = I ⊔ span {a}
obtain : ∀ (w : ℕ) (i : Fin w → R) (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
⊢ I.FG

Tactic:
obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon

Premises used: Submodule.fg_iff_exists_fin_generating_family, Iff.mp
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : Submodule.span R (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
rw :
  ∀ (hf : span (Set.range f) = I ⊔ span {a}) (w : ℕ) (i : Fin w → R)
    (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
⊢ I.FG

Tactic:
rw [submodule_span_eq] at hf

Premises used: Ideal.submodule_span_eq
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
k : Fin w
apply : f k ∈ span {a} ⊔ I
⊢ ∃ (r : R), ∃ p ∈ I, r * a + p = f k

Tactic:
apply mem_span_singleton_sup.1

Premises used: Ideal.mem_span_singleton_sup, Iff.mp
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
k : Fin w
rw : Membership.mem (γ := Ideal R) (span (Set.range f)) (f k)
⊢ f k ∈ span {a} ⊔ I

Tactic:
rw [sup_comm, ← hf]

Premises used: sup_comm
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
k : Fin w
⊢ Membership.mem (γ := Ideal R) (span (Set.range f)) (f k)

Tactic:
mem_span_range_self

Premises used: Ideal.mem_span_range_self
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
k : Fin w
⊢ Membership.mem (γ := Ideal R) (span (Set.range f)) (f k)

Tactic:
exact mem_span_range_self

Premises used: Ideal.mem_span_range_self
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
⊢ ∀ (k : Fin w), ∃ (r : R), ∃ p ∈ I, r * a + p = f k

Tactic:
have H k : ∃ r : R, ∃ p ∈ I, r * a + p = f k := by
      apply mem_span_singleton_sup.1
      rw [sup_comm, ← hf]
      exact mem_span_range_self
-- Module: Mathlib.RingTheory.Noetherian.OfPrime
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
a : R
hsup : (I ⊔ span {a}).FG
hcolon : (Submodule.colon I (↑(span {a}) : Set R)).FG
w : ℕ
f : Fin w → R
hf : span (Set.range f) = I ⊔ span {a}
w_1 : ℕ
i : Fin w_1 → R
hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)
H : ∀ (k : Fin w), ∃ (r : R), ∃ p ∈ I, r * a + p = f k
choose! : ∀ (r p : (k : Fin w) → R) (p_mem_I : ∀ (k : Fin w), p k ∈ I) (Hf : ∀ (k : Fin w), r k * a + p k = f k), I.FG
⊢ I.FG

Tactic:
choose! r p p_mem_I Hf using H