awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ IsNoetherian.{u_1, u_2} R ↥N ↔ ∀ s ≤ N, s.FG
have refine : ∀ (h : ∀ s ≤ N, s.FG) (s : Submodule R ↥N), s.FG
Tactic: refine ⟨fun ⟨hn⟩ => fun s hs =>
    have : s ≤ LinearMap.range N.subtype := N.range_subtype.symm ▸ hs
    Submodule.map_comap_eq_self this ▸ (hn _).map _,
    fun h => ⟨fun s => ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
⊢ s.FG
have h₁ : (Submodule.map N.subtype s).FG
Tactic: specialize h (s.map N.subtype) (Submodule.map_subtype_le N s)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsNoetherian R M ↔ WellFoundedGT.{u_2} (Submodule R M)
have refine : IsNoetherian R M ↔ ∀ (k : Submodule R M), IsCompactElement k
Tactic: refine .trans ?_ ((CompleteLattice.wellFoundedGT_characterisations <| Submodule R M).out 0 3).symm
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsNoetherian R M ↔ WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2
have rw : WellFoundedGT.{u_2} (Submodule R M) ↔ WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2
Tactic: rw [isNoetherian_iff', ← isWellFounded_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
rw : WellFoundedGT.{u_2} (Submodule R M) ↔ WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2
⊢ IsNoetherian R M ↔ WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2
have rw₁ : WellFoundedGT.{u_2} (Submodule R M) ↔ IsWellFounded.{u_2} (Submodule R M) fun (x1 x2 : Submodule R M) ↦ x1 > x2
Tactic: rw [isNoetherian_iff', ← isWellFounded_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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 }
⊢ IsNoetherian R M ↔ WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
have mp : IsNoetherian R M → WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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 }
mp : IsNoetherian R M → WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
⊢ IsNoetherian R M ↔ WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
have mpr : WellFoundedGT.{u_2} { N : Submodule R M // N.FG } → IsNoetherian R M
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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 }
⊢ IsNoetherian R M
have mpr : ∀ (s : Submodule R M), s.FG
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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 : Submodule R M
⊢ N.FG
have mpr : ∀ (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),
  N.FG
Tactic: obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ :=
      WellFounded.has_min H.wf { N' : α | N'.1 ≤ N } ⟨⟨⊥, Submodule.fg_bot⟩, @bot_le _ _ _ N⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
⊢ N.FG
have h : N = N₀
Tactic: convert! h₁
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
⊢ N = N₀
have h : N ≤ N₀
Tactic: refine (e.antisymm ?_).symm
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
⊢ N ≤ N₀
have h : ∀ (h₃ : ¬N ≤ N₀), False
Tactic: by_contra h₃
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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₀
⊢ False
have h : ∀ (x : M) (hx₁ : x ∈ N) (hx₂ : x ∉ N₀), False
Tactic: obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := Set.not_subset.mp h₃
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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₀
⊢ False
have h : x ∈ N₀
Tactic: apply hx₂
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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₀
⊢ Eq (α := Submodule R M) (span R (↑{x} : Set M)) (R ∙ x)
have rw : Eq (α := Submodule R M) (R ∙ x) (R ∙ x)
Tactic: rw [Finset.coe_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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 ∈ N₀
have h : x ∈ R ∙ 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)]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M
have rw : (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔
  WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2
Tactic: rw [isNoetherian_iff, WellFounded.wellFounded_iff_has_min]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
⊢ (∀ (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M
have 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
Tactic: rw [isNoetherian_iff, WellFounded.wellFounded_iff_has_min]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module 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
have 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)
Tactic: rw [isNoetherian_iff', wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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)
⊢ (∀ (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
have 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)
Tactic: rw [isNoetherian_iff', wellFoundedGT_iff_monotone_chain_condition]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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 : ℕ) in atTop, Disjoint (f ^ n).ker (f ^ n).range
have obtain : ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)),
  ∀ᶠ (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
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
have refine : ∀ (m : ℕ) (hm : m ≥ n), (f ^ m).ker ⊓ (f ^ m).range = ⊥
Tactic: refine eventually_atTop.mpr ⟨n, fun m hm ↦ disjoint_iff.mpr ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
⊢ (f ^ m).ker ⊓ (f ^ m).range = ⊥
have rw : ∀ x ∈ LinearMap.ker (f ^ n) ⊓ (f ^ m).range, x = 0
Tactic: rw [← hn _ hm, Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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)
⊢ Eq (α := M) ((f ^ m : (a : M) → M) x : M) (0 : M)
have apply : Eq (α := M) ((f ^ n : (a : M) → M) x : M) (0 : M)
Tactic: apply pow_map_zero_of_le hm
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (hypothesis)
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)
⊢ Eq (α := M) ((f ^ n : (a : M) → M) x : M) (0 : M)
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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))
⊢ Eq (α := M) ((f ^ n : (a : M) → M) x : M) (0 : M)
have rwa : ∀ (hx : x ∈ LinearMap.ker (f ^ n)), Eq (α := M) ((f ^ n : (a : M) → M) x : M) (0 : M)
Tactic: rwa [← hn _ (n.le_add_right m)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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 : ℕ) in atTop, ⨆ (m : ℕ), (f ^ m).ker = (f ^ n).ker
have obtain : ∀ (n : ℕ) (hn : ∀ (m : ℕ), n ≤ m → (f ^ n).ker = (f ^ m).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
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
have refine : ∀ (m : ℕ) (hm : m ≥ n), ⨆ (m : ℕ), (f ^ m).ker = (f ^ m).ker
Tactic: refine eventually_atTop.mpr ⟨n, fun m hm ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
have refine : ∀ (l : ℕ), (f ^ l).ker ≤ (f ^ m).ker
Tactic: refine le_antisymm (iSup_le fun l ↦ ?_) (le_iSup (fun i ↦ LinearMap.ker (f ^ i)) m)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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 : ℕ
⊢ (f ^ l).ker ≤ (f ^ m).ker
have inl : ∀ (h : m ≤ l), (f ^ l).ker ≤ (f ^ m).ker
Tactic: rcases le_or_gt m l with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
⊢ (f ^ l).ker ≤ (f ^ m).ker
have inr : ∀ (h : l < m), (f ^ l).ker ≤ (f ^ m).ker
Tactic: rcases le_or_gt m l with h | h
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
⊢ (f ^ l).ker ≤ (f ^ m).ker
have inl : (f ^ n).ker ≤ (f ^ m).ker
Tactic: rw [← hn _ (hm.trans h), hn _ hm]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Defs (goal)
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
⊢ (f ^ l).ker ≤ (f ^ m).ker
have inl₁ : (f ^ m).ker ≤ (f ^ m).ker
Tactic: rw [← hn _ (hm.trans h), hn _ hm]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Filter (goal)
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
⊢ EventuallyConst (α := ℕ) (β := Submodule R M) (⇑f : (a : ℕ) → Submodule R M) atTop
have 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)
Tactic: simp_rw [eventuallyConst_atTop, eq_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : IsNoetherianRing R
⊢ IsNilpotent (R := Ideal R) (nilradical R)
have obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := Ideal R) (Ideal.radical ⊥) n ≤ ⊥), IsNilpotent (R := Ideal R) (nilradical R)
Tactic: obtain ⟨n, hn⟩ := Ideal.exists_radical_pow_le_of_fg (⊥ : Ideal R) (IsNoetherian.noetherian _)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
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
⊢ I.FG
have obtain : ∀ (w : ℕ) (f : Fin w → R) (hf : Submodule.span R (Set.range f) = I ⊔ span {a}), I.FG
Tactic: obtain ⟨_, f, hf⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hsup
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
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}
⊢ I.FG
have obtain : ∀ (w : ℕ) (i : Fin w → R) (hi : Submodule.span R (Set.range i) = Submodule.colon I (↑(span {a}) : Set R)), I.FG
Tactic: obtain ⟨_, i, hi⟩ := Submodule.fg_iff_exists_fin_generating_family.1 hcolon
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
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)
⊢ I.FG
have 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
Tactic: rw [submodule_span_eq] at hf
Cleared hypotheses: hf, w_1, i, hi
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
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
have apply : f k ∈ span {a} ⊔ I
Tactic: apply mem_span_singleton_sup.1
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
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
⊢ f k ∈ span {a} ⊔ I
have rw : Membership.mem (γ := Ideal R) (span (Set.range f)) (f k)
Tactic: rw [sup_comm, ← hf]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (hypothesis)
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)
⊢ I.FG
have H : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
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
⊢ I.FG
have 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
Tactic: choose! r p p_mem_I Hf using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
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)
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
have refine_1 : span (↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) : Set R) ≤ I
Tactic: refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.OfPrime (goal)
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)
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
refine_1 : span (↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) : Set R) ≤ I
⊢ I.FG
have refine_2 : ∀ (y : R) (hy : y ∈ I),
  Membership.mem (γ := Submodule R R) (span (↑(Finset.image p Finset.univ ∪ Finset.image (a • i) Finset.univ) : Set R))
    y
Tactic: refine ⟨image p univ ∪ image (a • i) univ, le_antisymm ?_ (fun y hy ↦ ?_)⟩