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
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
α β : Type u_6
e : α ≃ β
h : ∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)
_ : ∀ {M : β → Submodule R N} [∀ (i : β), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : β), M i)
⊢ ∀ {M : β → Submodule R N} [∀ (i : β), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : β), M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
α β : Type u_6
e : α ≃ β
h : ∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)
M_1 : β → Submodule R N
_ : ∀ [∀ (i : β), IsNoetherian.{u_1, u_4} R ↥(M_1 i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : β), M_1 i)
⊢ ∀ [∀ (i : β), IsNoetherian.{u_1, u_4} R ↥(M_1 i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : β), M_1 i)

Tactic:
_
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
α β : Type u_6
e : α ≃ β
h : ∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)
M_1 : β → Submodule R N
inst_9 : ∀ (i : β), IsNoetherian.{u_1, u_4} R ↥(M_1 i)
rw : IsNoetherian.{u_1, u_4} R ↥(⨆ (x : α), M_1 ((e : (a : α) → β) x))
⊢ IsNoetherian.{u_1, u_4} R ↥(⨆ (i : β), M_1 i)

Tactic:
rw [← e.iSup_comp]

Premises used: Equiv.iSup_comp
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
α β : Type u_6
e : α ≃ β
h : ∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)
M_1 : β → Submodule R N
inst_9 : ∀ (i : β), IsNoetherian.{u_1, u_4} R ↥(M_1 i)
⊢ IsNoetherian.{u_1, u_4} R ↥(⨆ (x : α), M_1 ((e : (a : α) → β) x))

Tactic:
apply h
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
M_1 : PEmpty.{u_6 + 1} → Submodule R N
inst_9 : ∀ (i : PEmpty.{u_6 + 1}), IsNoetherian.{u_1, u_4} R ↥(M_1 i)
rw : IsNoetherian.{u_1, u_4} R ↥⊥
⊢ IsNoetherian.{u_1, u_4} R ↥(⨆ (i : PEmpty.{u_6 + 1}), M_1 i)

Tactic:
rw [iSup_of_empty]

Premises used: iSup_of_empty
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
M_1 : PEmpty.{u_6 + 1} → Submodule R N
inst_9 : ∀ (i : PEmpty.{u_6 + 1}), IsNoetherian.{u_1, u_4} R ↥(M_1 i)
⊢ IsNoetherian.{u_1, u_4} R ↥⊥

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
α : Type u_6
_ :
  ∀ [Fintype α],
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)],
        IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)) →
      ∀ {M : Option α → Submodule R N} [∀ (i : Option α), IsNoetherian.{u_1, u_4} R ↥(M i)],
        IsNoetherian.{u_1, u_4} R ↥(⨆ (i : Option α), M i)
⊢ ∀ [Fintype α],
    (∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)],
        IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)) →
      ∀ {M : Option α → Submodule R N} [∀ (i : Option α), IsNoetherian.{u_1, u_4} R ↥(M i)],
        IsNoetherian.{u_1, u_4} R ↥(⨆ (i : Option α), M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
α : Type u_6
inst_9 : Fintype α
ih :
  ∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)
_ :
  ∀ {M : Option α → Submodule R N} [∀ (i : Option α), IsNoetherian.{u_1, u_4} R ↥(M i)],
    IsNoetherian.{u_1, u_4} R ↥(⨆ (i : Option α), M i)
⊢ ∀ {M : Option α → Submodule R N} [∀ (i : Option α), IsNoetherian.{u_1, u_4} R ↥(M i)],
    IsNoetherian.{u_1, u_4} R ↥(⨆ (i : Option α), M i)

Tactic:
_
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
α : Type u_6
inst_9 : Fintype α
ih :
  ∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)
M_1 : Option α → Submodule R N
_ : ∀ [∀ (i : Option α), IsNoetherian.{u_1, u_4} R ↥(M_1 i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : Option α), M_1 i)
⊢ ∀ [∀ (i : Option α), IsNoetherian.{u_1, u_4} R ↥(M_1 i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : Option α), M_1 i)

Tactic:
_
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
α : Type u_6
inst_9 : Fintype α
ih :
  ∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)
M_1 : Option α → Submodule R N
inst_10 : ∀ (i : Option α), IsNoetherian.{u_1, u_4} R ↥(M_1 i)
rw : IsNoetherian.{u_1, u_4} R ↥(M_1 none ⊔ ⨆ (b : α), M_1 (some b))
⊢ IsNoetherian.{u_1, u_4} R ↥(⨆ (i : Option α), M_1 i)

Tactic:
rw [iSup_option]

Premises used: iSup_option
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module S P
ι : Type u_6
inst_8 : Finite ι
α : Type u_6
inst_9 : Fintype α
ih :
  ∀ {M : α → Submodule R N} [∀ (i : α), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : α), M i)
M_1 : Option α → Submodule R N
inst_10 : ∀ (i : Option α), IsNoetherian.{u_1, u_4} R ↥(M_1 i)
⊢ IsNoetherian.{u_1, u_4} R ↥(M_1 none ⊔ ⨆ (b : α), M_1 (some b))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_7
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : IsNoetherian R M
inst_8 : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range = g.ker
⊢ ∀ (a : Submodule R N), Submodule.map (f.ker.liftQ f ⋯) (Submodule.comap (f.ker.liftQ f ⋯) a) = a ⊓ f.range

Tactic:
simp [Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ]

Premises used: Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
P : Type u_7
inst_5 : AddCommGroup P
inst_6 : Module R P
inst_7 : IsNoetherian R M
inst_8 : IsNoetherian R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : f.range = g.ker
⊢ ∀ (a : Submodule R N),
    Submodule.comap (M₂ := ↥g.range) g.rangeRestrict (Submodule.map g.rangeRestrict a) = a ⊔ f.range

Tactic:
simp [Submodule.comap_map_eq, h]

Premises used: Submodule.comap_map_eq
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
S : Submodule R N
⊢ IsNoetherian R N ↔ IsNoetherian.{u_1, u_4} R ↥S ∧ IsNoetherian.{u_1, u_4} R (N ⧸ S)

Tactic:
⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩

Premises used: inferInstance, And.intro, Iff.intro, IsNoetherian, _private.0.isNoetherian_iff_submodule_quotient.match_1
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
S : Submodule R N
refine :
  IsNoetherian.{u_1, u_4} R ↥S ∧ IsNoetherian.{u_1, u_4} R (N ⧸ S) →
    IsNoetherian.{u_1, u_4} R ↥S → IsNoetherian.{u_1, u_4} R (N ⧸ S) → IsNoetherian R N
⊢ IsNoetherian R N ↔ IsNoetherian.{u_1, u_4} R ↥S ∧ IsNoetherian.{u_1, u_4} R (N ⧸ S)

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
S : Submodule R N
h : IsNoetherian.{u_1, u_4} R ↥S ∧ IsNoetherian.{u_1, u_4} R (N ⧸ S)
left : IsNoetherian.{u_1, u_4} R ↥S
right : IsNoetherian.{u_1, u_4} R (N ⧸ S)
apply : S.subtype.range = S.mkQ.ker
⊢ IsNoetherian R N

Tactic:
apply isNoetherian_of_range_eq_ker S.subtype S.mkQ

Premises used: isNoetherian_of_range_eq_ker, Submodule.subtype, Submodule.mkQ
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
N : Type u_4
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
S : Submodule R N
h : IsNoetherian.{u_1, u_4} R ↥S ∧ IsNoetherian.{u_1, u_4} R (N ⧸ S)
left : IsNoetherian.{u_1, u_4} R ↥S
right : IsNoetherian.{u_1, u_4} R (N ⧸ S)
rw : S.subtype.range = S
rw₁ rw₂ : S = S
⊢ S.subtype.range = S.mkQ.ker

Tactic:
rw [Submodule.ker_mkQ, Submodule.range_subtype]

Premises used: Submodule.ker_mkQ, Submodule.range_subtype
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherian R M
inst_6 : Module.Finite R N
ι : Type u_4
inst_7 : Finite ι
⊢ IsNoetherian R ((ι → R) →ₗ[R] M)

Tactic:
let _i : Fintype ι := Fintype.ofFinite ι; isNoetherian_of_linearEquiv (Module.piEquiv ι R M)

Premises used: Fintype.ofFinite, Module.piEquiv, isNoetherian_of_linearEquiv
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherian R M
inst_6 : Module.Finite R N
obtain :
  ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] N)
    (hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := Fin n → R) (β := N) (⇑f : (a : Fin n → R) → N)),
    IsNoetherian R (N →ₗ[R] M)
⊢ IsNoetherian R (N →ₗ[R] M)

Tactic:
obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R N

Premises used: Module.Finite.exists_fin'
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherian R M
inst_6 : Module.Finite R N
n : ℕ
f : (Fin n → R) →ₗ[R] N
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := Fin n → R) (β := N) (⇑f : (a : Fin n → R) → N)
g : (N →ₗ[R] M) →ₗ[R] (Fin n → R) →ₗ[R] M :=
  (LinearMap.flip (LinearMap.llcomp R (Fin n → R) N M) :
      (a : (Fin n → R) →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] (Fin n → R) →ₗ[R] M)
    f
⊢ IsNoetherian R (N →ₗ[R] M)

Tactic:
isNoetherian_of_injective g hf.injective_linearMapComp_right

Premises used: isNoetherian_of_injective, Function.Surjective.injective_linearMapComp_right
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
inst_5 : IsNoetherian R M
inst_6 : Module.Finite R N
n : ℕ
f : (Fin n → R) →ₗ[R] N
hf : Function.Surjective.{u_1 + 1, u_3 + 1} (α := Fin n → R) (β := N) (⇑f : (a : Fin n → R) → N)
g : (N →ₗ[R] M) →ₗ[R] (Fin n → R) →ₗ[R] M :=
  (LinearMap.flip (LinearMap.llcomp R (Fin n → R) N M) :
      (a : (Fin n → R) →ₗ[R] N) → (N →ₗ[R] M) →ₗ[R] (Fin n → R) →ₗ[R] M)
    f
⊢ IsNoetherian R (N →ₗ[R] M)

Tactic:
exact isNoetherian_of_injective g hf.injective_linearMapComp_right

Premises used: isNoetherian_of_injective, Function.Surjective.injective_linearMapComp_right
-- Module: Mathlib.RingTheory.Noetherian.Basic
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
P : Submodule R M → Prop
hgt : ∀ (I : Submodule R M), (∀ J > I, P J) → P I
I : Submodule R M
⊢ P I

Tactic:
IsWellFounded.induction _ I hgt

Premises used: IsWellFounded.induction
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑l : (a : M) → P)
simp_rw : WellFoundedGT.{u_2} (Submodule R M) ↔ WellFoundedGT.{u_4} (Submodule S P)
⊢ IsNoetherian R M ↔ IsNoetherian S P

Tactic:
simp_rw [isNoetherian_iff']

Premises used: isNoetherian_iff'
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑l : (a : M) → P)
e : OrderIso.{u_2, u_4} (Submodule R M) (Submodule S P) := orderIsoMapComapOfBijective l hl
⊢ WellFoundedGT.{u_2} (Submodule R M) ↔ WellFoundedGT.{u_4} (Submodule S P)

Tactic:
⟨fun _ ↦ e.symm.strictMono.wellFoundedGT, fun _ ↦ e.strictMono.wellFoundedGT⟩

Premises used: OrderIso.strictMono, StrictMono.wellFoundedGT, OrderIso.symm, Iff.intro
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
P : Type u_4
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
l : M →ₛₗ[σ] P
hl : Bijective.{u_2 + 1, u_4 + 1} (α := M) (β := P) (⇑l : (a : M) → P)
e : OrderIso.{u_2, u_4} (Submodule R M) (Submodule S P) := orderIsoMapComapOfBijective l hl
⊢ WellFoundedGT.{u_2} (Submodule R M) ↔ WellFoundedGT.{u_4} (Submodule S P)

Tactic:
exact ⟨fun _ ↦ e.symm.strictMono.wellFoundedGT, fun _ ↦ e.strictMono.wellFoundedGT⟩
-- Module: Mathlib.RingTheory.Noetherian.Basic
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
ι : Type u_5
N : ι → Submodule R M
h : iSupIndep N
⊢ Set.Finite.{u_5} (α := ι) {i : ι | N i ≠ ⊥}

Tactic:
WellFoundedGT.finite_ne_bot_of_iSupIndep h

Premises used: WellFoundedGT.finite_ne_bot_of_iSupIndep, setOf
-- Module: Mathlib.RingTheory.Noetherian.Basic
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
inst_4 : Nontrivial R
ι : Type u_5
v : ι → M
hv : LinearIndependent R v
i : ι
h : Eq (α := Submodule R M) (R ∙ v i) ⊥
⊢ v i = 0

Tactic:
simp_all
-- Module: Mathlib.RingTheory.Noetherian.Basic
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
P : Type u_5
inst_4 : AddCommMonoid P
inst_5 : Module R P
f : P × M →ₗ[R] M
inj_1 : Injective (α := P × M) (β := M) (⇑f : (a : P × M) → M)
p : P
h : ¬p = 0
g : LinearMap.{u_1, u_1, u_5, u_2} (RingHom.id R) (ℕ →₀ P) M
inj : Injective.{u_5 + 1, u_2 + 1} (α := ℕ →₀ P) (β := M) (⇑g : (a : ℕ →₀ P) → M)
i : ℕ
⊢ Ne.{u_2 + 1} (α := M) ((g : (a : ℕ →₀ P) → M) ((Finsupp.lsingle i : (a : P) → ℕ →₀ P) p : ℕ →₀ P) : M) (0 : M)

Tactic:
simpa [inj]
-- Module: Mathlib.RingTheory.Noetherian.Basic
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
inst_4 : Nontrivial R
s : Set M
hi : LinearIndependent.{u_2, u_1, u_2} (ι := { x : M // x ∈ s }) R (Subtype.val (p := fun (x : M) ↦ x ∈ s))
⊢ s.Finite

Tactic:
hi.finite_of_isNoetherian

Premises used: Set.Finite, LinearIndependent.finite_of_isNoetherian
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
t : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
obtain : ∀ (n : ℕ) (w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊥
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊥

Tactic:
obtain ⟨n, w⟩ := t
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
h₁ : ∀ (m : ℕ), n + 1 ≤ m → f m = ⊥
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊥

Tactic:
use n + 1
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
p : n + 1 ≤ 0
⊢ f 0 = ⊥

Tactic:
cases p
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
h₁ : n ≤ m
⊢ f (m + 1) = ⊥

Tactic:
apply w
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
⊢ n ≤ m

Tactic:
Nat.succ_le_succ_iff.mp p

Premises used: Nat.succ_le_succ_iff, Iff.mp
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
m : ℕ
p : n + 1 ≤ m + 1
⊢ n ≤ m

Tactic:
exact Nat.succ_le_succ_iff.mp p

Premises used: Nat.succ_le_succ_iff, Iff.mp
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
suffices : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊥

Tactic:
suffices t : ∃ n : ℕ, ∀ m, n ≤ m → f (m + 1) = ⊥ by
    obtain ⟨n, w⟩ := t
    use n + 1
    rintro (_ | m) p
    · cases p
    · apply w
      exact Nat.succ_le_succ_iff.mp p
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
obtain :
  ∀ (n : ℕ)
    (w :
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Submodule R M) ((partialSups f : (a : ℕ) → Submodule R M) n : Submodule R M)
            ((partialSups f : (a : ℕ) → Submodule R M) m : Submodule R M)),
    ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥

Tactic:
obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance (partialSups f)

Premises used: Iff.mpr, inferInstance, partialSups, monotone_stabilizes_iff_noetherian
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M) ((partialSups f : (a : ℕ) → Submodule R M) n : Submodule R M)
        ((partialSups f : (a : ℕ) → Submodule R M) m : Submodule R M)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥

Tactic:
⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩

Premises used: Disjoint.eq_bot_of_ge, sup_eq_left, Exists.intro, Iff.mp
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M) ((partialSups f : (a : ℕ) → Submodule R M) n : Submodule R M)
        ((partialSups f : (a : ℕ) → Submodule R M) m : Submodule R M)
refine :
  ∀ (m : ℕ) (p : n ≤ m),
    Eq (α := Submodule R M) ((partialSups f : (a : ℕ) → Submodule R M) m ⊔ f (m + 1) : Submodule R M)
      ((partialSups f : (a : ℕ) → Submodule R M) m : Submodule R M)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥

Tactic:
refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
n : ℕ
w :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := Submodule R M) ((partialSups f : (a : ℕ) → Submodule R M) n : Submodule R M)
        ((partialSups f : (a : ℕ) → Submodule R M) m : Submodule R M)
m : ℕ
p : n ≤ m
⊢ Eq (α := Submodule R M) ((partialSups f : (a : ℕ) → Submodule R M) m ⊔ f (m + 1) : Submodule R M)
    ((partialSups f : (a : ℕ) → Submodule R M) m : Submodule R M)

Tactic:
simpa only [partialSups_add_one] using (w (m + 1) <| le_add_right p).symm.trans <| w m p

Premises used: partialSups_add_one, HAdd.hAdd, OfNat.ofNat, Eq.symm, Eq.trans, le_add_right
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Subsingleton R
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
⊢ IsNoetherian R M

Tactic:
haveI := Module.subsingleton R M
  isNoetherian_of_finite R M

Premises used: isNoetherian_of_finite
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : IsNoetherian R M
⊢ IsNoetherian.{u_1, u_2} R ↥N

Tactic:
isNoetherian_mk ⟨OrderEmbedding.wellFounded (Submodule.MapSubtype.orderEmbedding N).dual h.wf⟩

Premises used: isNoetherian_mk, IsWellFounded.mk, IsNoetherian.wf, Submodule.MapSubtype.orderEmbedding, OrderEmbedding.wellFounded, OrderEmbedding.dual