awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : SMul R S
inst_4 : Module S M
inst_5 : Module R M
inst_6 : IsScalarTower R S M
h : IsNoetherian R M
⊢ IsNoetherian S M

Tactic:
isNoetherian_mk ⟨(Submodule.restrictScalarsEmbedding R S M).dual.wellFounded h.wf⟩

Premises used: isNoetherian_mk, IsWellFounded.mk, IsNoetherian.wf, Submodule.restrictScalarsEmbedding, OrderEmbedding.wellFounded, OrderEmbedding.dual
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
inst_4 : Module.Finite R M
⊢ IsNoetherian R M

Tactic:
have ⟨_, _, h⟩ := Module.Finite.exists_fin' R M
  isNoetherian_of_surjective _ (LinearMap.range_eq_top.mpr h)

Premises used: Iff.mpr, isNoetherian_of_surjective, LinearMap.range_eq_top, IsNoetherian, Module.Finite.exists_fin', _private.0.isNoetherian_of_isNoetherianRing_of_finite.match_1
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
I : IsNoetherianRing R
hN : N.FG
⊢ IsNoetherian.{u_1, u_2} R ↥N

Tactic:
haveI : Module.Finite R N := .of_fg hN; inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
A : Set M
hA : A.Finite
⊢ IsNoetherian.{u_1, u_2} R ↥(span R A)

Tactic:
isNoetherian_of_fg_of_noetherian _ (Submodule.fg_def.mpr ⟨A, hA, rfl⟩)

Premises used: Iff.mpr, Submodule.fg_def, isNoetherian_of_fg_of_noetherian, And.intro, Exists.intro, rfl
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : Ring S
inst_2 : Module R S
inst_3 : IsScalarTower R S S
inst_4 : IsNoetherianRing R
inst_5 : Module.Finite R S
⊢ IsNoetherianRing S

Tactic:
isNoetherian_of_tower R inferInstance

Premises used: inferInstance, isNoetherian_of_tower
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
hf : Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
H : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
isNoetherian_mk ⟨OrderEmbedding.wellFounded (Ideal.orderEmbeddingOfSurjective f hf).dual H.wf⟩

Premises used: isNoetherian_mk, Ideal.orderEmbeddingOfSurjective, IsWellFounded.mk, IsNoetherian.wf, OrderEmbedding.wellFounded, OrderEmbedding.dual
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R →+* S
inst_2 : IsNoetherianRing R
⊢ IsNoetherianRing.{u_2} ↥f.rangeS

Tactic:
isNoetherianRing_of_surjective R f.rangeS f.rangeSRestrict f.rangeSRestrict_surjective

Premises used: RingHom.rangeSRestrict_surjective, isNoetherianRing_of_surjective, Membership.mem, Subtype, RingHom.rangeSRestrict, RingHom.rangeS
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
inst : Ring R
S : Type u_2
inst_1 : Ring S
f : R →+* S
inst_2 : IsNoetherianRing R
⊢ IsNoetherianRing.{u_2} ↥(RingHom.range.{u_1, u_2} (R := R) f)

Tactic:
isNoetherianRing_rangeS f

Premises used: Set.Mem, Subring.copy, isNoetherianRing_rangeS, RingHom.range, Subsemiring.copy, RingHom.rangeS
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
f : R ≃+* S
inst_2 : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
isNoetherianRing_of_surjective R S f.toRingHom f.toEquiv.surjective

Premises used: RingEquiv.toEquiv, isNoetherianRing_of_surjective, RingEquiv.toRingHom, Equiv.surjective
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsNoetherianRing R
inst_3 : IsNoetherianRing S
rw :
  WellFoundedGT.{u_1} (Submodule R R) → WellFoundedGT.{u_2} (Submodule S S) → WellFoundedGT (Submodule (R × S) (R × S))
⊢ IsNoetherianRing (R × S)

Tactic:
rw [IsNoetherianRing, isNoetherian_iff'] at *

Premises used: isNoetherian_iff', IsNoetherianRing
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
inst_2 : WellFoundedGT.{u_1} (Submodule R R)
inst_3 : WellFoundedGT.{u_2} (Submodule S S)
⊢ WellFoundedGT (Submodule (R × S) (R × S))

Tactic:
Ideal.idealProdEquiv.toOrderEmbedding.wellFoundedGT

Premises used: OrderIso.toOrderEmbedding, Ideal.idealProdEquiv, OrderEmbedding.wellFoundedGT
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
inst_2 : WellFoundedGT.{u_1} (Submodule R R)
inst_3 : WellFoundedGT.{u_2} (Submodule S S)
⊢ WellFoundedGT (Submodule (R × S) (R × S))

Tactic:
exact Ideal.idealProdEquiv.toOrderEmbedding.wellFoundedGT

Premises used: OrderIso.toOrderEmbedding, Ideal.idealProdEquiv, OrderEmbedding.wellFoundedGT
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
ι : Type u_2
inst : Finite ι
apply :
  ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing.{u_1} (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsNoetherianRing.{u_1} (R i)],
        IsNoetherianRing ((i : β) → R i)
apply₁ :
  ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsNoetherianRing.{u_1} (R i)], IsNoetherianRing ((i : PEmpty.{u_2 + 1}) → R i)
apply₂ :
  ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing.{u_1} (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)]
        [∀ (i : Option α), IsNoetherianRing.{u_1} (R i)], IsNoetherianRing ((i : Option α) → R i)
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsNoetherianRing.{u_1} (R i)],
    IsNoetherianRing ((i : ι) → R i)

Tactic:
apply Finite.induction_empty_option _ _ _ ι

Premises used: Finite.induction_empty_option
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
ι : Type u_2
inst : Finite ι
α β : Type u_2
⊢ ∀ (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing.{u_1} (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsNoetherianRing.{u_1} (R i)],
        IsNoetherianRing ((i : β) → R i)

Tactic:
fun e h ↦ isNoetherianRing_of_ringEquiv _ (.piCongrLeft _ e)

Premises used: RingEquiv.piCongrLeft, isNoetherianRing_of_ringEquiv
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
ι : Type u_2
inst : Finite ι
⊢ ∀ {α β : Type u_2} (a : α ≃ β),
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing.{u_1} (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : β → Type u_1} [inst : (i : β) → Semiring (R i)] [∀ (i : β), IsNoetherianRing.{u_1} (R i)],
        IsNoetherianRing ((i : β) → R i)

Tactic:
exact fun e h ↦ isNoetherianRing_of_ringEquiv _ (.piCongrLeft _ e)

Premises used: isNoetherianRing_of_ringEquiv
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
ι : Type u_2
inst : Finite ι
⊢ ∀ {R : PEmpty.{u_2 + 1} → Type u_1} [inst : (i : PEmpty.{u_2 + 1}) → Semiring (R i)]
    [∀ (i : PEmpty.{u_2 + 1}), IsNoetherianRing.{u_1} (R i)], IsNoetherianRing ((i : PEmpty.{u_2 + 1}) → R i)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
ι : Type u_2
inst : Finite ι
α : Type u_2
inst_1 : Fintype α
⊢ (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing.{u_1} (R i)],
      IsNoetherianRing ((i : α) → R i)) →
    ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)]
      [∀ (i : Option α), IsNoetherianRing.{u_1} (R i)], IsNoetherianRing ((i : Option α) → R i)

Tactic:
fun ih ↦ isNoetherianRing_of_ringEquiv _ (.symm .piOptionEquivProd)

Premises used: RingEquiv.piOptionEquivProd, Option.none, Prod, isNoetherianRing_of_ringEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
ι : Type u_2
inst : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing.{u_1} (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)]
        [∀ (i : Option α), IsNoetherianRing.{u_1} (R i)], IsNoetherianRing ((i : Option α) → R i)

Tactic:
exact fun ih ↦ isNoetherianRing_of_ringEquiv _ (.symm .piOptionEquivProd)

Premises used: isNoetherianRing_of_ringEquiv, RingEquiv.symm
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
inst_3 : IsNoetherian.{u_1, u_2} R ↥T
hST : S ≤ T
⊢ S.FG

Tactic:
isNoetherian_submodule.mp inferInstance _ hST

Premises used: isNoetherian_submodule, inferInstance, Iff.mp
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
S T : Submodule R M
hT : T.FG
hST : S ≤ T
⊢ Module.Finite.{u_1, u_2} R ↥T

Tactic:
rw [← Module.Finite.iff_fg] at hT

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
S T : Submodule R M
hT : T.FG
hST : S ≤ T
hT₁ : Module.Finite.{u_1, u_2} R ↥T
⊢ S ≤ T

Tactic:
rw [← Module.Finite.iff_fg] at hT

Premises used: Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
S T : Submodule R M
hT : Module.Finite.{u_1, u_2} R ↥T
hST : S ≤ T
⊢ S.FG

Tactic:
FG.of_le_of_isNoetherian hST

Premises used: Submodule.FG.of_le_of_isNoetherian
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
S T : Submodule R M
hT : Module.Finite.{u_1, u_2} R ↥T
hST : S ≤ T
⊢ S.FG

Tactic:
exact FG.of_le_of_isNoetherian hST

Premises used: Submodule.FG.of_le_of_isNoetherian
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
rcases :
  ∀ (m : ℕ) (f' : (Fin m → R) →ₗ[R] M)
    (hf' : Surjective.{u + 1, v + 1} (α := Fin m → R) (β := M) (⇑f' : (a : Fin m → R) → M)),
    ∃ (P : Type v) (x : AddCommGroup P) (x_1 : Module R P) (_ : Free R P) (_ : Module.Finite R P) (f : P →ₗ[R] M),
      Surjective (α := P) (β := M) (⇑f : (a : P) → M)
⊢ ∃ (P : Type v) (x : AddCommGroup P) (x_1 : Module R P) (_ : Free R P) (_ : Module.Finite R P) (f : P →ₗ[R] M),
    Surjective (α := P) (β := M) (⇑f : (a : P) → M)

Tactic:
rcases Module.Finite.exists_fin' R M with ⟨m, f', hf'⟩

Premises used: Module.Finite.exists_fin'
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
m : ℕ
f' : (Fin m → R) →ₗ[R] M
hf' : Surjective.{u + 1, v + 1} (α := Fin m → R) (β := M) (⇑f' : (a : Fin m → R) → M)
f : (Fin m →₀ Shrink.{v, u} R) →ₗ[R] M :=
  f' ∘ₗ
    (↑(Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) ≪≫ₗ Finsupp.linearEquivFunOnFinite R R (Fin m)) :
      (Fin m →₀ Shrink.{v, u} R) →ₗ[R] Fin m → R)
h : Surjective (α := Fin m →₀ Shrink.{v, u} R) (β := M) (⇑f : (a : Fin m →₀ Shrink.{v, u} R) → M)
⊢ ∃ (P : Type v) (x : AddCommGroup P) (x_1 : Module R P) (_ : Free R P) (_ : Module.Finite R P) (f : P →ₗ[R] M),
    Surjective (α := P) (β := M) (⇑f : (a : P) → M)

Tactic:
use (Fin m →₀ Shrink.{v, u} R), inferInstance, inferInstance, inferInstance, inferInstance, f
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u
inst : CommRing R
inst_1 : Small.{v, u} R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
m : ℕ
f' : (Fin m → R) →ₗ[R] M
hf' : Surjective.{u + 1, v + 1} (α := Fin m → R) (β := M) (⇑f' : (a : Fin m → R) → M)
f : (Fin m →₀ Shrink.{v, u} R) →ₗ[R] M :=
  f' ∘ₗ
    (↑(Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) ≪≫ₗ Finsupp.linearEquivFunOnFinite R R (Fin m)) :
      (Fin m →₀ Shrink.{v, u} R) →ₗ[R] Fin m → R)
⊢ Surjective (α := Fin m →₀ Shrink.{v, u} R) (β := M) (⇑f : (a : Fin m →₀ Shrink.{v, u} R) → M)

Tactic:
simpa [f] using hf'
-- 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
⊢ IsNoetherian R M ↔ ∀ (s : Submodule R M), s.FG

Tactic:
⟨fun h => h.noetherian, IsNoetherian.mk⟩

Premises used: IsNoetherian.noetherian, Iff.intro, IsNoetherian.mk
-- 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
N : Submodule R M
⊢ IsNoetherian.{u_1, u_2} R ↥N ↔ ∀ s ≤ N, s.FG

Tactic:
⟨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 => ?_⟩⟩

Premises used: _private.0.isNoetherian_submodule.match_1, Submodule.map_comap_eq_self, Submodule.FG.map, Eq.rec, Submodule.comap, Iff.intro, Submodule.subtype, IsNoetherian.mk, Eq.symm, Submodule.range_subtype
-- 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
N : Submodule R M
refine : ∀ (h : ∀ s ≤ N, s.FG) (s : Submodule R ↥N), s.FG
⊢ IsNoetherian.{u_1, u_2} R ↥N ↔ ∀ s ≤ 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 => ?_⟩⟩
-- 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
N : Submodule R M
h : ∀ s ≤ N, s.FG
s : Submodule R ↥N
⊢ (Submodule.map N.subtype s).FG

Tactic:
specialize h (s.map N.subtype) (Submodule.map_subtype_le N s)

Premises used: Submodule.subtype, Submodule.map, Submodule.map_subtype_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
N : Submodule R M
s : Submodule R ↥N
h : (Submodule.map N.subtype s).FG
⊢ s.FG

Tactic:
Submodule.fg_of_fg_map_injective N.subtype Subtype.val_injective h

Premises used: Subtype.val_injective, Submodule.subtype, Submodule.fg_of_fg_map_injective
-- 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
N : Submodule R M
s : Submodule R ↥N
h : (Submodule.map N.subtype s).FG
⊢ s.FG

Tactic:
exact Submodule.fg_of_fg_map_injective N.subtype Subtype.val_injective h

Premises used: Subtype.val_injective, Submodule.subtype, Submodule.fg_of_fg_map_injective
-- 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
N : Submodule R M
⊢ IsNoetherian.{u_1, u_2} R ↥N ↔ ∀ (s : Submodule R M), (N ⊓ s).FG

Tactic:
isNoetherian_submodule.trans ⟨fun H _ => H _ inf_le_left, fun H _ hs => inf_of_le_right hs ▸ H _⟩

Premises used: isNoetherian_submodule, Eq.rec, inf_of_le_right, Iff.intro, Iff.trans, inf_le_left, Min.min
-- 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
N : Submodule R M
⊢ IsNoetherian.{u_1, u_2} R ↥N ↔ ∀ (s : Submodule R M), (s ⊓ N).FG

Tactic:
isNoetherian_submodule.trans ⟨fun H _ => H _ inf_le_right, fun H _ hs => inf_of_le_left hs ▸ H _⟩

Premises used: isNoetherian_submodule, inf_of_le_left, inf_le_right, Eq.rec, Iff.intro, Iff.trans, Min.min
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid P
inst_3 : Module R M
inst_4 : Module R P
inst_5 : IsNoetherian R M
N : Submodule R M
⊢ IsNoetherian.{u_1, u_2} R ↥N

Tactic:
isNoetherian_submodule.2 fun _ _ => IsNoetherian.noetherian _

Premises used: Iff.mpr, isNoetherian_submodule, IsNoetherian.noetherian
-- 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
s t : Submodule R M
ht : IsNoetherian.{u_1, u_2} R ↥t
h : s ≤ t
⊢ IsNoetherian.{u_1, u_2} R ↥s

Tactic:
isNoetherian_submodule.mpr fun _ hs' => isNoetherian_submodule.mp ht _ (le_trans hs' h)

Premises used: Iff.mpr, isNoetherian_submodule, Iff.mp, 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
⊢ IsNoetherian R M ↔ WellFoundedGT.{u_2} (Submodule R M)

Tactic:
.trans ?_ ((CompleteLattice.wellFoundedGT_characterisations <| Submodule R M).out 0 3).symm

Premises used: Submodule, List.TFAE.out, Iff.trans, CompleteLattice.wellFoundedGT_characterisations, OfNat.ofNat, Iff.symm
-- 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
refine : IsNoetherian R M ↔ ∀ (k : Submodule R M), IsCompactElement k
⊢ IsNoetherian R M ↔ WellFoundedGT.{u_2} (Submodule R M)

Tactic:
refine .trans ?_ ((CompleteLattice.wellFoundedGT_characterisations <| Submodule R M).out 0 3).symm
-- 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
⊢ IsNoetherian R M ↔ ∀ (k : Submodule R M), IsCompactElement k

Tactic:
⟨fun ⟨h⟩ => fun k => (fg_iff_compact k).mp (h k), fun h =>
      ⟨fun k => (fg_iff_compact k).mpr (h k)⟩⟩

Premises used: Iff.mpr, _private.0.isNoetherian_iff'.match_1, Iff.intro, Iff.mp, Submodule.fg_iff_compact, IsNoetherian.mk
-- 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
⊢ IsNoetherian R M ↔ ∀ (k : Submodule R M), IsCompactElement k

Tactic:
exact
    ⟨fun ⟨h⟩ => fun k => (fg_iff_compact k).mp (h k), fun h =>
      ⟨fun k => (fg_iff_compact k).mpr (h k)⟩⟩
-- 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 : WellFoundedGT.{u_2} (Submodule R M) ↔ WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2
rw₁ rw₂ :
  WellFoundedGT.{u_2} (Submodule R M) ↔ IsWellFounded.{u_2} (Submodule R M) fun (x1 x2 : Submodule R M) ↦ x1 > x2
⊢ IsNoetherian R M ↔ WellFounded fun (x1 x2 : Submodule R M) ↦ x1 > x2

Tactic:
rw [isNoetherian_iff', ← isWellFounded_iff]

Premises used: isNoetherian_iff', isWellFounded_iff
-- Module: Mathlib.RingTheory.Noetherian.Defs
Goal:
R : Type u_1
M : Type u_2
P : Type u_3
N : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : AddCommMonoid P
inst_6 : Module R P
h : IsNoetherian R M
⊢ WellFoundedGT.{u_2} (Submodule R M)

Tactic:
h.wellFoundedGT

Premises used: IsNoetherian.wellFoundedGT
-- 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 }
mp : IsNoetherian R M → WellFoundedGT.{u_2} { N : Submodule R M // N.FG }
mpr : WellFoundedGT.{u_2} { N : Submodule R M // N.FG } → IsNoetherian R M
⊢ IsNoetherian R M ↔ WellFoundedGT.{u_2} { N : Submodule R M // N.FG }

Tactic:
constructor
-- 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 : IsNoetherian R M
f : α ↪o Submodule R M := OrderEmbedding.subtype fun (N : Submodule R M) ↦ N.FG
⊢ WellFoundedGT.{u_2} { N : Submodule R M // N.FG }

Tactic:
OrderEmbedding.wellFoundedLT f.dual

Premises used: OrderEmbedding.wellFoundedLT, OrderDual, OrderEmbedding.dual
-- 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 : IsNoetherian R M
f : α ↪o Submodule R M := OrderEmbedding.subtype fun (N : Submodule R M) ↦ N.FG
⊢ WellFoundedGT.{u_2} { N : Submodule R M // N.FG }

Tactic:
exact OrderEmbedding.wellFoundedLT f.dual

Premises used: OrderEmbedding.wellFoundedLT, OrderEmbedding.dual
-- 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 }
mpr : ∀ (s : Submodule R M), s.FG
⊢ IsNoetherian R M

Tactic:
constructor
-- 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 : Submodule R M
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
⊢ 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⟩

Premises used: setOf, Bot.bot, LE.le, IsWellFounded.wf, Subtype.mk, Exists.intro, WellFounded.has_min, Submodule.fg_bot, Subtype.val, bot_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
α : 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

Tactic:
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₀
⊢ N.FG

Tactic:
convert! 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
⊢ N = N₀

Tactic:
(e.antisymm ?_).symm

Premises used: LE.le.antisymm, Eq.symm
-- 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₀
⊢ N = N₀

Tactic:
refine (e.antisymm ?_).symm

Premises used: LE.le.antisymm, Eq.symm