awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S N
inst_6 : Finite M
s : Submodule R M
rw : Submodule.span R (↑s : Set M) = s
⊢ Submodule.span R (↑(⋯.toFinset (s := (↑s : Set M))) : Set M) = s
have rw₁ : s = s
Tactic: rw [Set.Finite.coe_toFinset, Submodule.span_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (hypothesis)
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
M₁ M₂ : Submodule R N
inst_8 : IsNoetherian.{u_1, u_4} R ↥M₁
inst_9 : IsNoetherian.{u_1, u_4} R ↥M₂
⊢ IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
have this : IsNoetherian.{u_1, u_4} R ↥(M₁.subtype.coprod M₂.subtype).range
Tactic: have := isNoetherian_range (M₁.subtype.coprod M₂.subtype)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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
M₁ M₂ : Submodule R N
inst_8 : IsNoetherian.{u_1, u_4} R ↥M₁
inst_9 : IsNoetherian.{u_1, u_4} R ↥M₂
this : IsNoetherian.{u_1, u_4} R ↥(M₁.subtype.coprod M₂.subtype).range
⊢ IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
have rwa : ∀ (this : IsNoetherian.{u_1, u_4} R ↥(M₁.subtype.range ⊔ M₂.subtype.range)), IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
Tactic: rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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
M₁ M₂ : Submodule R N
inst_8 : IsNoetherian.{u_1, u_4} R ↥M₁
inst_9 : IsNoetherian.{u_1, u_4} R ↥M₂
this : IsNoetherian.{u_1, u_4} R ↥(M₁.subtype.coprod M₂.subtype).range
rwa : ∀ (this : IsNoetherian.{u_1, u_4} R ↥(M₁.subtype.range ⊔ M₂.subtype.range)), IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
⊢ IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
have rwa₁ : ∀ (this : IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂.subtype.range)), IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
Tactic: rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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
M₁ M₂ : Submodule R N
inst_8 : IsNoetherian.{u_1, u_4} R ↥M₁
inst_9 : IsNoetherian.{u_1, u_4} R ↥M₂
this : IsNoetherian.{u_1, u_4} R ↥(M₁.subtype.coprod M₂.subtype).range
rwa : ∀ (this : IsNoetherian.{u_1, u_4} R ↥(M₁.subtype.range ⊔ M₂.subtype.range)), IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
rwa₁ : ∀ (this : IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂.subtype.range)), IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
⊢ IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
have rwa₂ : ∀ (this : IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)), IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)
Tactic: rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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 : ι → Type u_7} [inst_9 : (i : ι) → AddCommGroup (M i)] [inst_10 : (i : ι) → Module.{u_1, u_7} R (M i)]
    [∀ (i : ι), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : ι) → M i)
have apply : ∀ {α β : Type u_6} (a : α ≃ β),
  (∀ {M : α → Type u_7} [inst_9 : (i : α) → AddCommGroup (M i)] [inst_10 : (i : α) → Module.{u_1, u_7} R (M i)]
      [∀ (i : α), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : α) → M i)) →
    ∀ {M : β → Type u_7} [inst_9 : (i : β) → AddCommGroup (M i)] [inst_10 : (i : β) → Module.{u_1, u_7} R (M i)]
      [∀ (i : β), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : β) → M i)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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 ι
apply :
  ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {M : α → Type u_7} [inst_9 : (i : α) → AddCommGroup (M i)] [inst_10 : (i : α) → Module.{u_1, u_7} R (M i)]
        [∀ (i : α), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : α) → M i)) →
      ∀ {M : β → Type u_7} [inst_9 : (i : β) → AddCommGroup (M i)] [inst_10 : (i : β) → Module.{u_1, u_7} R (M i)]
        [∀ (i : β), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : β) → M i)
⊢ ∀ {M : ι → Type u_7} [inst_9 : (i : ι) → AddCommGroup (M i)] [inst_10 : (i : ι) → Module.{u_1, u_7} R (M i)]
    [∀ (i : ι), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : ι) → M i)
have apply₁ : ∀ {M : PEmpty.{u_6 + 1} → Type u_7} [inst_9 : (i : PEmpty.{u_6 + 1}) → AddCommGroup (M i)]
  [inst_10 : (i : PEmpty.{u_6 + 1}) → Module.{u_1, u_7} R (M i)]
  [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : PEmpty.{u_6 + 1}) → M i)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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 ι
apply :
  ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {M : α → Type u_7} [inst_9 : (i : α) → AddCommGroup (M i)] [inst_10 : (i : α) → Module.{u_1, u_7} R (M i)]
        [∀ (i : α), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : α) → M i)) →
      ∀ {M : β → Type u_7} [inst_9 : (i : β) → AddCommGroup (M i)] [inst_10 : (i : β) → Module.{u_1, u_7} R (M i)]
        [∀ (i : β), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : β) → M i)
apply₁ :
  ∀ {M : PEmpty.{u_6 + 1} → Type u_7} [inst_9 : (i : PEmpty.{u_6 + 1}) → AddCommGroup (M i)]
    [inst_10 : (i : PEmpty.{u_6 + 1}) → Module.{u_1, u_7} R (M i)]
    [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : PEmpty.{u_6 + 1}) → M i)
⊢ ∀ {M : ι → Type u_7} [inst_9 : (i : ι) → AddCommGroup (M i)] [inst_10 : (i : ι) → Module.{u_1, u_7} R (M i)]
    [∀ (i : ι), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : ι) → M i)
have apply₂ : ∀ {α : Type u_6} [Fintype α],
  (∀ {M : α → Type u_7} [inst_10 : (i : α) → AddCommGroup (M i)] [inst_11 : (i : α) → Module.{u_1, u_7} R (M i)]
      [∀ (i : α), IsNoetherian.{u_1, u_7} R (M i)], IsNoetherian R ((i : α) → M i)) →
    ∀ {M : Option α → Type u_7} [inst_10 : (i : Option α) → AddCommGroup (M i)]
      [inst_11 : (i : Option α) → Module.{u_1, u_7} R (M i)] [∀ (i : Option α), IsNoetherian.{u_1, u_7} R (M i)],
      IsNoetherian R ((i : Option α) → M i)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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 : ι → Submodule R N} [∀ (i : ι), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : ι), M i)
have apply : ∀ {α β : Type u_6} (a : α ≃ β),
  (∀ {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: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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 ι
apply :
  ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {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)
have apply₁ : ∀ {M : PEmpty.{u_6 + 1} → Submodule R N} [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian.{u_1, u_4} R ↥(M i)],
  IsNoetherian.{u_1, u_4} R ↥(⨆ (i : PEmpty.{u_6 + 1}), M i)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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 ι
apply :
  ∀ {α β : Type u_6} (a : α ≃ β),
    (∀ {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)
apply₁ :
  ∀ {M : PEmpty.{u_6 + 1} → Submodule R N} [∀ (i : PEmpty.{u_6 + 1}), IsNoetherian.{u_1, u_4} R ↥(M i)],
    IsNoetherian.{u_1, u_4} R ↥(⨆ (i : PEmpty.{u_6 + 1}), M i)
⊢ ∀ {M : ι → Submodule R N} [∀ (i : ι), IsNoetherian.{u_1, u_4} R ↥(M i)], IsNoetherian.{u_1, u_4} R ↥(⨆ (i : ι), M i)
have apply₂ : ∀ {α : 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)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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 ↥(⨆ (i : β), M_1 i)
have rw : IsNoetherian.{u_1, u_4} R ↥(⨆ (x : α), M_1 ((e : (a : α) → β) x))
Tactic: rw [← e.iSup_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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 ↥(⨆ (i : PEmpty.{u_6 + 1}), M_1 i)
have rw : IsNoetherian.{u_1, u_4} R ↥⊥
Tactic: rw [iSup_of_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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 ↥(⨆ (i : Option α), M_1 i)
have rw : IsNoetherian.{u_1, u_4} R ↥(M_1 none ⊔ ⨆ (b : α), M_1 (some b))
Tactic: rw [iSup_option]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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)
have 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
Tactic: refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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)
⊢ IsNoetherian R N
have apply : S.subtype.range = S.mkQ.ker
Tactic: apply isNoetherian_of_range_eq_ker S.subtype S.mkQ
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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)
⊢ S.subtype.range = S.mkQ.ker
have rw : S.subtype.range = S
Tactic: rw [Submodule.ker_mkQ, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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
⊢ S.subtype.range = S.mkQ.ker
have rw₁ : S = S
Tactic: rw [Submodule.ker_mkQ, Submodule.range_subtype]
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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
⊢ IsNoetherian R (N →ₗ[R] M)
have 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)
Tactic: obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R N
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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)
⊢ IsNoetherian R M ↔ IsNoetherian S P
have simp_rw : WellFoundedGT.{u_2} (Submodule R M) ↔ WellFoundedGT.{u_4} (Submodule S P)
Tactic: simp_rw [isNoetherian_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
t : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊥
have obtain : ∀ (n : ℕ) (w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊥
Tactic: obtain ⟨n, w⟩ := t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
n : ℕ
w : ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊥
have h₁ : ∀ (m : ℕ), n + 1 ≤ m → f m = ⊥
Tactic: use n + 1
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (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 : ℕ → 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
⊢ f (m + 1) = ⊥
have h₁ : n ≤ m
Tactic: apply w
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f m = ⊥
have suffices : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
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
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (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 : ℕ → Submodule R M
h : ∀ (n : ℕ), Disjoint ((partialSups f : (a : ℕ) → Submodule R M) n) (f (n + 1))
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f (m + 1) = ⊥
have 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) = ⊥
Tactic: obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance (partialSups f)
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (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 : ℕ → 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) = ⊥
have 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)
Tactic: refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
inst_2 : IsNoetherianRing R
inst_3 : IsNoetherianRing S
⊢ IsNoetherianRing (R × S)
have rw : WellFoundedGT.{u_1} (Submodule R R) → WellFoundedGT.{u_2} (Submodule S S) → WellFoundedGT (Submodule (R × S) (R × S))
Tactic: rw [IsNoetherianRing, isNoetherian_iff'] at *
Cleared hypotheses: inst_2, inst_3
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
Goal:
ι : Type u_2
inst : Finite ι
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsNoetherianRing.{u_1} (R i)],
    IsNoetherianRing ((i : ι) → R i)
have 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)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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)
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsNoetherianRing.{u_1} (R i)],
    IsNoetherianRing ((i : ι) → R i)
have 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)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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)
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsNoetherianRing.{u_1} (R i)],
    IsNoetherianRing ((i : ι) → R i)
have 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)
Tactic: apply Finite.induction_empty_option _ _ _ ι
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (hypothesis)
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
⊢ S.FG
have hT₁ : Module.Finite.{u_1, u_2} R ↥T
Tactic: rw [← Module.Finite.iff_fg] at hT
Cleared hypotheses: hT, hST
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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
⊢ ∃ (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)
have 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)
Tactic: rcases Module.Finite.exists_fin' R M with ⟨m, f', hf'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Noetherian.Basic (goal)
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)
⊢ ∃ (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)
have h : Surjective (α := Fin m →₀ Shrink.{v, u} R) (β := M) (⇑f : (a : Fin m →₀ Shrink.{v, u} R) → M)
Tactic: use (Fin m →₀ Shrink.{v, u} R), inferInstance, inferInstance, inferInstance, inferInstance, f