awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
obtain :
  ∀ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R)
    (inj :
      Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
        (⇑g : (a : MvPolynomial (Fin s) k) → R))
    (int : g.IsIntegral),
    ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R),
      Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
          (⇑g : (a : MvPolynomial (Fin s) k) → R) ∧
        g.Finite
⊢ ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R),
    Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
        (⇑g : (a : MvPolynomial (Fin s) k) → R) ∧
      g.Finite

Tactic:
obtain ⟨s, g, ⟨inj, int⟩⟩ := exists_integral_inj_algHom_of_fg k R

Premises used: exists_integral_inj_algHom_of_fg
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R) (⇑g : (a : MvPolynomial (Fin s) k) → R)
int : g.IsIntegral
⊢ let algInst := g.toAlgebra;
  Algebra.IsIntegral.{u_2, u_3} (MvPolynomial (Fin s) k) R

Tactic:
algebraize [g.toRingHom]

Premises used: AlgHom.toRingHom
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R) (⇑g : (a : MvPolynomial (Fin s) k) → R)
int : g.IsIntegral
algInst : Algebra.{u_2, u_3} (MvPolynomial (Fin s) k) R := g.toAlgebra
algebraizeInst : Algebra.IsIntegral.{u_2, u_3} (MvPolynomial (Fin s) k) R
rw :
  Eq (α := k →+* R)
    (@RingHom.comp _ (MvPolynomial (Fin s) k) _ _ Semiring.toNonAssocSemiring _ (algebraMap (MvPolynomial (Fin s) k) R)
      (algebraMap k (MvPolynomial (Fin s) k)))
    (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
rw₁ rw₂ :
  Eq (α := k →+* R) (g.comp (algebraMap k (MvPolynomial (Fin s) k))) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
⊢ Eq (α := k →+* R) (algebraMap k R) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))

Tactic:
rw [IsScalarTower.algebraMap_eq k (MvPolynomial (Fin s) k), algebraMap_toAlgebra']

Premises used: RingHom.algebraMap_toAlgebra', IsScalarTower.algebraMap_eq, MvPolynomial, Fin
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R) (⇑g : (a : MvPolynomial (Fin s) k) → R)
int : g.IsIntegral
⊢ Eq (α := k →+* R) (algebraMap k R) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))

Tactic:
have h : algebraMap k R = g.toRingHom.comp (algebraMap k (MvPolynomial (Fin s) k)) := by
    algebraize [g.toRingHom]
    rw [IsScalarTower.algebraMap_eq k (MvPolynomial (Fin s) k), algebraMap_toAlgebra']
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R) (⇑g : (a : MvPolynomial (Fin s) k) → R)
int : g.IsIntegral
h : Eq (α := k →+* R) (algebraMap k R) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
⊢ ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R),
    Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
        (⇑g : (a : MvPolynomial (Fin s) k) → R) ∧
      g.Finite

Tactic:
⟨s, g, inj, int.to_finite
    (h ▸ RingHom.finiteType_algebraMap.mpr fin).of_comp_finiteType⟩

Premises used: And.intro, Exists.intro, RingHom.IsIntegral.to_finite
-- Module: Mathlib.RingTheory.NoetherNormalization
Goal:
k : Type u_2
R : Type u_3
inst : Field k
inst_1 : CommRing R
inst_2 : Nontrivial R
a : Algebra k R
fin : Algebra.FiniteType k R
s : ℕ
g : MvPolynomial (Fin s) k →ₐ[k] R
inj :
  Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R) (⇑g : (a : MvPolynomial (Fin s) k) → R)
int : g.IsIntegral
h : Eq (α := k →+* R) (algebraMap k R) (g.comp (algebraMap k (MvPolynomial (Fin s) k)))
⊢ ∃ (s : ℕ) (g : MvPolynomial (Fin s) k →ₐ[k] R),
    Function.Injective.{u_2 + 1, u_3 + 1} (α := MvPolynomial (Fin s) k) (β := R)
        (⇑g : (a : MvPolynomial (Fin s) k) → R) ∧
      g.Finite

Tactic:
exact ⟨s, g, inj, int.to_finite
    (h ▸ RingHom.finiteType_algebraMap.mpr fin).of_comp_finiteType⟩
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : f.range = ⊤
inst_7 : IsNoetherian R M
⊢ IsNoetherian S P

Tactic:
⟨fun s ↦
    have : (s.comap f).map f = s := Submodule.map_comap_eq_self <| hf.symm ▸ le_top
    this ▸ (IsNoetherian.noetherian _).map _⟩

Premises used: Submodule.map_comap_eq_self, Submodule.FG.map, Eq.rec, IsNoetherian.noetherian, Submodule.comap, le_top, IsNoetherian.mk, Eq.symm
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
s : Submodule R M
f : M →ₛₗ[σ] P
inst_7 : IsNoetherian.{u_1, u_3} R ↥s
⊢ Eq (α := Submodule S ↥(Submodule.map f s)) (LinearMap.range (f.submoduleMap s)) ⊤

Tactic:
simp [LinearMap.submoduleMap]

Premises used: LinearMap.submoduleMap
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
inst_7 : IsNoetherian R M
⊢ IsNoetherian.{u_2, u_4} S ↥f.range

Tactic:
isNoetherian_of_surjective _ f.range_rangeRestrict

Premises used: LinearMap.range_rangeRestrict, isNoetherian_of_surjective
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M_1 : Type u_3
P : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M_1
inst_3 : AddCommMonoid P
inst_4 : Module R M_1
inst_5 : Module S P
A : Type u_5
M : Type u_6
inst_6 : Ring A
inst_7 : AddCommGroup M
inst_8 : SMul R A
inst_9 : Module R M
inst_10 : Module A M
inst_11 : IsScalarTower R A M
N : Submodule A M
inst_12 : IsNoetherian R M
⊢ IsNoetherian.{u_1, u_6} R (M ⧸ N)

Tactic:
isNoetherian_of_surjective ((Submodule.mkQ N).restrictScalars R) <|
    LinearMap.range_eq_top.mpr N.mkQ_surjective

Premises used: Iff.mpr, LinearMap.restrictScalars, isNoetherian_of_surjective, LinearMap.range_eq_top, Submodule.mkQ, Submodule.mkQ_surjective
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module S P
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
f : M ≃ₛₗ[σ] P
inst_8 : IsNoetherian R M
⊢ IsNoetherian S P

Tactic:
isNoetherian_of_surjective f.toLinearMap f.range

Premises used: isNoetherian_of_surjective, LinearEquiv.toLinearMap, LinearEquiv.range
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module S P
σ : R →+* S
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
f : M ≃ₛₗ[σ] P
⊢ IsNoetherian R M ↔ IsNoetherian S P

Tactic:
⟨fun _ ↦ isNoetherian_of_linearEquiv f, fun _ ↦ isNoetherian_of_linearEquiv f.symm⟩

Premises used: LinearEquiv.symm, Iff.intro, isNoetherian_of_linearEquiv
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
M : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ IsNoetherian.{u_1, u_3} R ↥⊤ ↔ IsNoetherian R M

Tactic:
Submodule.topEquiv.isNoetherian_iff

Premises used: Submodule.topEquiv, LinearEquiv.isNoetherian_iff
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module S P
inst_6 : IsNoetherian S P
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
inst_8 : RingHomInvPair σ' σ
f : M →ₛₗ[σ] P
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
⊢ IsNoetherian R M

Tactic:
isNoetherian_of_linearEquiv (LinearEquiv.ofInjective f hf).symm

Premises used: LinearEquiv.symm, LinearEquiv.ofInjective, isNoetherian_of_linearEquiv
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_4
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module S P
inst_6 : IsNoetherian S P
N : Submodule R M
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
inst_8 : RingHomInvPair σ' σ
f : M →ₛₗ[σ] P
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
⊢ N.FG

Tactic:
haveI := isNoetherian_of_injective f hf
  IsNoetherian.noetherian N

Premises used: IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Noetherian.Basic
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
rw₁ rw₂ : s = s
⊢ Submodule.span R (↑(⋯.toFinset (s := (↑s : Set M))) : Set M) = s

Tactic:
rw [Set.Finite.coe_toFinset, Submodule.span_eq]

Premises used: Set.Finite.coe_toFinset, Submodule.span_eq
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : IsNoetherian R M
⊢ Module.Finite R M

Tactic:
⟨IsNoetherian.noetherian ⊤⟩

Premises used: IsNoetherian.noetherian, Module.Finite.of_fg_top, Top.top
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S_1 : Type u_2
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : Semiring S_1
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Module R M
inst_5 : Module S_1 N
R₁ : Type u_5
S : Type u_6
inst_6 : CommSemiring R₁
inst_7 : Semiring S
inst_8 : Algebra R₁ S
inst_9 : IsNoetherian R₁ S
I : Ideal S
⊢ Module.Finite.{u_5, u_6} R₁ ↥I

Tactic:
IsNoetherian.finite R₁ ((I : Submodule S S).restrictScalars R₁)

Premises used: Set.Mem, Submodule.restrictScalars, Membership.mem, Subtype, Module.IsNoetherian.finite
-- Module: Mathlib.RingTheory.Noetherian.Basic
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 : IsNoetherian S N
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
inst_8 : RingHomInvPair σ' σ
f : M →ₛₗ[σ] N
hf : Function.Injective.{u_3 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ Module.Finite R M

Tactic:
⟨fg_of_injective f hf⟩

Premises used: Module.Finite.of_fg_top, fg_of_injective
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module S P
inst_6 : IsNoetherian S P
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
inst_8 : RingHomInvPair σ' σ
f : M →ₛₗ[σ] P
hf : f.ker = ⊥
⊢ IsNoetherian R M

Tactic:
isNoetherian_of_linearEquiv (LinearEquiv.ofInjective f <| LinearMap.ker_eq_bot.mp hf).symm

Premises used: LinearEquiv.symm, LinearMap.ker_eq_bot, LinearEquiv.ofInjective, Iff.mp, isNoetherian_of_linearEquiv
-- Module: Mathlib.RingTheory.Noetherian.Basic
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
P : Type u_5
inst : Ring R
inst_1 : Ring S
inst_2 : AddCommGroup M
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module S P
inst_6 : IsNoetherian S P
N : Submodule R M
σ : R →+* S
σ' : S →+* R
inst_7 : RingHomInvPair σ σ'
inst_8 : RingHomInvPair σ' σ
f : M →ₛₗ[σ] P
hf : f.ker = ⊥
⊢ N.FG

Tactic:
haveI := isNoetherian_of_ker_bot f hf
  IsNoetherian.noetherian N

Premises used: IsNoetherian.noetherian
-- 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
inst_8 : IsNoetherian R M
inst_9 : IsNoetherian R N
⊢ IsNoetherian R (M × N)

Tactic:
⟨fun s =>
    Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.snd R M N) (noetherian _) <|
      have : s ⊓ LinearMap.ker (LinearMap.snd R M N) ≤ LinearMap.range (LinearMap.inl R M N) :=
        fun x ⟨_, hx2⟩ => ⟨x.1, Prod.ext rfl <| Eq.symm <| LinearMap.mem_ker.1 hx2⟩
      Submodule.map_comap_eq_self this ▸ (noetherian _).map _⟩

Premises used: LinearMap.inl, Submodule.map_comap_eq_self, LinearMap.snd, LinearMap.ker, Submodule.FG.map, Membership.mem, Eq.rec, LinearMap.range, IsNoetherian.noetherian, _private.0.isNoetherian_prod.match_1, Prod.fst, LinearMap.mem_ker, Submodule.comap, Prod.ext, Exists.intro, Iff.mp, Submodule.map, IsNoetherian.mk, Eq.symm, Min.min, rfl, Submodule.fg_of_fg_map_of_fg_inf_ker
-- 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
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₁.subtype.coprod M₂.subtype).range

Tactic:
have := isNoetherian_range (M₁.subtype.coprod M₂.subtype)
-- 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
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₂)
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (this : IsNoetherian.{u_1, u_4} R ↥(M₁ ⊔ M₂)), 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

Premises used: LinearMap.range_coprod, Submodule.range_subtype
-- 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 ι
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)
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)
⊢ ∀ {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 _ _ _ ι

Premises used: Finite.induction_empty_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
⊢ ∀ (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:
fun e h ↦ isNoetherian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)

Premises used: LinearEquiv.piCongrLeft, isNoetherian_of_linearEquiv
-- 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} (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:
exact fun e h ↦ isNoetherian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)

Premises used: LinearEquiv.piCongrLeft, isNoetherian_of_linearEquiv
-- 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 : 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:
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
inst_9 : 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:
fun ih ↦ isNoetherian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm

Premises used: LinearEquiv.symm, LinearEquiv.piOptionEquivProd, isNoetherian_of_linearEquiv
-- 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 : α → 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:
exact fun ih ↦ isNoetherian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm

Premises used: LinearEquiv.symm, LinearEquiv.piOptionEquivProd, isNoetherian_of_linearEquiv
-- 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 ι
inst_9 : IsNoetherian R M
⊢ IsNoetherian R (ι → M)

Tactic:
isNoetherian_pi

Premises used: isNoetherian_pi
-- 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 ι
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)
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)
⊢ ∀ {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 _ _ _ ι

Premises used: Finite.induction_empty_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
_ :
  ∀ {β : 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)
⊢ ∀ {β : 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:
_