awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R₀ : Type u_1
R : Type u_2
M_1 : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M_1
inst_4 : Module R₀ M_1
inst_5 : Module R M_1
inst_6 : IsScalarTower R₀ R M_1
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
M : Type u
x : AddCommGroup M
x_1 : Module R₀ M
x_2 : Module R M
h_1 : IsScalarTower R₀ R M
hs :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
hq :
  (fun (M : Type u) [AddCommGroup M] [Module R₀ M] [Module R M] ↦
      IsNoetherian R M ∨ IsArtinian R M → Module.Finite R₀ M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h : IsNoetherian R M ∨ IsArtinian R M
N : Submodule R₀ M := Submodule.restrictScalars R₀ (HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
this_1 : Module.Finite.{u_1, u} R₀ ↥N
this : Module.Finite.{u_1, u} R₀ (M ⧸ N)
⊢ Module.Finite R₀ M

Tactic:
exact .of_submodule_quotient N
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
inst_10 : IsNoetherian R M
⊢ Module.Finite R₀ M

Tactic:
finite_of_isNoetherian_or_isArtinian R₀ R M (.inl ‹_›)

Premises used: _private.0.IsSemiprimaryRing.finite_of_isNoetherian_or_isArtinian, Or.inl
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsSemiprimaryRing R
inst_8 : IsScalarTower R₀ R R
inst_9 : Module.Finite.{u_1, u_2} R₀ (HasQuotient.Quotient R (B := Ideal R) (Ring.jacobson R))
inst_10 : IsArtinian R M
⊢ Module.Finite R₀ M

Tactic:
finite_of_isNoetherian_or_isArtinian R₀ R M (.inr ‹_›)

Premises used: _private.0.IsSemiprimaryRing.finite_of_isNoetherian_or_isArtinian, Or.inr
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M_1 : Type u
inst : Ring R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
inst_3 : IsSemiprimaryRing R
M : Type u
x : AddCommGroup M
x_1 x_2 : Module R M
h_1 : IsScalarTower R R M
h :
  (fun (M : Type u) [AddCommGroup M] [Module R M] [Module R M] ↦ IsNoetherian R M ↔ IsArtinian R M)
    ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
h' :
  (fun (M : Type u) [AddCommGroup M] [Module R M] [Module R M] ↦ IsNoetherian R M ↔ IsArtinian R M)
    (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
N : Submodule R M := HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤
simp_rw simp_rw₁ : IsNoetherian R M ↔ IsArtinian R M
simp_rw₂ : IsNoetherian.{u_2, u} R ↥N ∧ IsNoetherian.{u_2, u} R (M ⧸ N) ↔ IsArtinian R M
simp_rw₃ :
  IsNoetherian.{u_2, u} R ↥N ∧ IsNoetherian.{u_2, u} R (M ⧸ N) ↔
    IsArtinian.{u_2, u} R ↥N ∧ IsArtinian.{u_2, u} R (M ⧸ N)
simp_rw₄ :
  IsNoetherian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ∧
      IsNoetherian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ↔
    IsArtinian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ∧
      IsArtinian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
simp_rw₅ :
  IsArtinian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ∧
      IsNoetherian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ↔
    IsArtinian.{u_2, u} R ↥(HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤) ∧
      IsArtinian.{u_2, u} R (M ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R M) (Ring.jacobson R) ⊤)
⊢ IsNoetherian R M ↔ IsArtinian R M

Tactic:
simp_rw [isNoetherian_iff_submodule_quotient N, isArtinian_iff_submodule_quotient N, N, h, h']

Premises used: isArtinian_iff_submodule_quotient, isNoetherian_iff_submodule_quotient
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsSemiprimaryRing R
fg : Ideal.FG (Ring.jacobson R)
⊢ IsNoetherian R M ↔ Module.Finite R M

Tactic:
⟨fun _ ↦ inferInstance, IsSemiprimaryRing.induction R R M
    (P := fun M ↦ Module.Finite R M → IsNoetherian R M)
    (fun M _ _ _ _ _ _ ↦ (IsSemisimpleModule.finite_tfae.out 0 1).mp)
    fun M _ _ _ _ hs hq fin ↦ (isNoetherian_iff_submodule_quotient (Ring.jacobson R • ⊤)).mpr
      ⟨hs (.of_fg (.smul fg fin.1)), hq inferInstance⟩⟩

Premises used: Iff.mpr, Module.Finite.fg_top, isNoetherian_iff_submodule_quotient, inferInstance, IsSemisimpleModule.finite_tfae, IsSemiprimaryRing.induction, List.TFAE.out, And.intro, Iff.intro, Iff.mp, Module.Finite.of_fg, HSMul.hSMul, Ring.jacobson, Top.top, OfNat.ofNat, Submodule.FG.smul
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
inst : Ring R
inst_1 : IsSemiprimaryRing R
⊢ IsNoetherianRing R ↔ Ideal.FG (Ring.jacobson R)

Tactic:
⟨fun _ ↦ IsNoetherian.noetherian .., fun fg ↦
    (IsSemiprimaryRing.isNoetherian_iff_finite_of_jacobson_fg fg).mpr inferInstance⟩

Premises used: Iff.mpr, inferInstance, IsNoetherian.noetherian, IsSemiprimaryRing.isNoetherian_iff_finite_of_jacobson_fg, Iff.intro, Ring.jacobson
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
⊢ IsNoetherian R M

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
⊢ IsArtinian R M

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
⊢ IsNoetherian R M ↔ IsArtinian R M

Tactic:
2 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
⊢ IsNoetherian R M ↔ IsArtinian R M

Tactic:
tfae_have 2 ↔ 3 := IsSemiprimaryRing.isNoetherian_iff_isArtinian

Premises used: IsSemiprimaryRing.isNoetherian_iff_isArtinian
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
⊢ IsNoetherian R M

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
⊢ Module.Finite R M

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
⊢ ∀ (a : IsNoetherian R M), Module.Finite R M

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
⊢ ∀ (a : IsNoetherian R M), Module.Finite R M

Tactic:
tfae_have 2 → 1 := fun _ ↦ inferInstance
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
⊢ Module.Finite R M

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
⊢ IsArtinian R M

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
⊢ ∀ (a : Module.Finite R M), IsArtinian R M

Tactic:
1 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
⊢ ∀ (a : Module.Finite R M), IsArtinian R M

Tactic:
tfae_have 1 → 3 := fun _ ↦ inferInstance
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
rw : [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M].TFAE
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE

Tactic:
rw [isFiniteLength_iff_isNoetherian_isArtinian]

Premises used: isFiniteLength_iff_isNoetherian_isArtinian
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
⊢ IsNoetherian R M

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
⊢ ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M

Tactic:
4 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
⊢ ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M

Tactic:
tfae_have 4 → 2 := And.left

Premises used: And.left
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
⊢ IsNoetherian R M

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
⊢ IsNoetherian R M ∧ IsArtinian R M

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
⊢ ∀ (a : IsNoetherian R M), IsNoetherian R M ∧ IsArtinian R M

Tactic:
2 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
⊢ ∀ (a : IsNoetherian R M), IsNoetherian R M ∧ IsArtinian R M

Tactic:
tfae_have 2 → 4 := fun h ↦ ⟨h, tfae_2_iff_3.mp h⟩
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
M : Type u
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsArtinianRing R
tfae_2_iff_3 : IsNoetherian R M ↔ IsArtinian R M
tfae_2_to_1 : ∀ (a : IsNoetherian R M), Module.Finite R M
tfae_1_to_3 : ∀ (a : Module.Finite R M), IsArtinian R M
tfae_4_to_2 : ∀ (a : IsNoetherian R M ∧ IsArtinian R M), IsNoetherian R M
tfae_2_to_4 : ∀ (a : IsNoetherian R M), IsNoetherian R M ∧ IsArtinian R M
⊢ [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsNoetherian R M ∧ IsArtinian R M].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R : Type u_2
inst : Ring R
⊢ IsArtinianRing R ↔ IsFiniteLength R R

Tactic:
⟨fun h ↦ ((IsArtinianRing.tfae R R).out 2 3).mp h,
    fun h ↦ (isFiniteLength_iff_isNoetherian_isArtinian.mp h).2⟩

Premises used: List.TFAE.out, And.right, IsArtinianRing.tfae, Iff.intro, Iff.mp, OfNat.ofNat, isFiniteLength_iff_isNoetherian_isArtinian
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
R₀ : Type u_1
R : Type u_2
M : Type u
inst : Ring R₀
inst_1 : Ring R
inst_2 : Module R₀ R
inst_3 : AddCommGroup M
inst_4 : Module R₀ M
inst_5 : Module R M
inst_6 : IsScalarTower R₀ R M
inst_7 : IsArtinianRing R
⊢ IsNoetherianRing R

Tactic:
((IsArtinianRing.tfae R R).out 2 1).mp ‹_›

Premises used: List.TFAE.out, IsArtinianRing.tfae, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
obtain : ∀ (s : Set M) (fin : s.Finite) (span : Eq (α := Submodule R M) (Submodule.span R s) ⊤), IsNoetherian R M
⊢ IsNoetherian R M

Tactic:
obtain ⟨s, fin, span⟩ := Submodule.fg_def.mp (Module.finite_def.mp ‹_›)

Premises used: Submodule.fg_def, Module.finite_def, Iff.mp
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : s.Finite
span : Eq (α := Submodule R M) (Submodule.span R s) ⊤
⊢ Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤

Tactic:
rw [← s.iUnion_of_singleton_coe, Submodule.span_iUnion] at span

Premises used: Submodule.span_iUnion, Set.iUnion_of_singleton_coe
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : s.Finite
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
⊢ Finite.{u + 1} (↑s : Type u)

Tactic:
rw [← Set.finite_coe_iff] at fin

Premises used: Set.finite_coe_iff
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : s.Finite
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
fin₁ : Finite.{u + 1} (↑s : Type u)
⊢ Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤

Tactic:
rw [← Set.finite_coe_iff] at fin

Premises used: Set.finite_coe_iff
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
rw : IsNoetherian.{u_3, u} R ↥(⨆ (i : (↑s : Type u)), R ∙ (↑i : M))
⊢ IsNoetherian R M

Tactic:
rw [← isNoetherian_top_iff, ← span]

Premises used: isNoetherian_top_iff
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
rw : IsNoetherian R (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
⊢ IsNoetherian.{u_3, u} R ↥(R ∙ i)

Tactic:
rw [LinearMap.span_singleton_eq_range, ← (LinearMap.quotKerEquivRange _).isNoetherian_iff]

Premises used: LinearEquiv.isNoetherian_iff, LinearMap.quotKerEquivRange, LinearMap.span_singleton_eq_range
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I :=
  fun (I : Ideal R) ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
rw :
  IsNoetherian.{u_3, u_3} (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
    (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
⊢ IsNoetherian R (HasQuotient.Quotient R (B := Submodule R R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))

Tactic:
rw [(e _).isNoetherian_iff_of_bijective Function.bijective_id]

Premises used: Function.bijective_id, LinearMap.isNoetherian_iff_of_bijective
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I :=
  fun (I : Ideal R) ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsNoetherian.{u_3, u_3} (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
    (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))

Tactic:
@instIsNoetherianRingOfIsArtinianRing _ _ ?_

Premises used: instIsNoetherianRingOfIsArtinianRing
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I :=
  fun (I : Ideal R) ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
refine : IsArtinianRing.{u_3} (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
⊢ IsNoetherian.{u_3, u_3} (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))
    (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))

Tactic:
refine @instIsNoetherianRingOfIsArtinianRing _ _ ?_

Premises used: instIsNoetherianRingOfIsArtinianRing
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I :=
  fun (I : Ideal R) ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
rw : IsArtinian.{u_3, u} R ↥(LinearMap.range (LinearMap.toSpanSingleton R M i))
⊢ IsArtinianRing.{u_3} (HasQuotient.Quotient R (B := Ideal R) (LinearMap.ker (LinearMap.toSpanSingleton R M i)))

Tactic:
rw [IsArtinianRing, ← (e _).isArtinian_iff_of_bijective Function.bijective_id,
      (LinearMap.quotKerEquivRange _).isArtinian_iff]

Premises used: Function.bijective_id, IsArtinianRing, LinearMap.isArtinian_iff_of_bijective, LinearMap.quotKerEquivRange, LinearEquiv.isArtinian_iff
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I :=
  fun (I : Ideal R) ↦ { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinian.{u_3, u} R ↥(LinearMap.range (LinearMap.toSpanSingleton R M i))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
⊢ ∀ (i : M), IsNoetherian.{u_3, u} R ↥(R ∙ i)

Tactic:
have _ (i : M) : IsNoetherian R (Submodule.span R {i}) := by
    rw [LinearMap.span_singleton_eq_range, ← (LinearMap.quotKerEquivRange _).isNoetherian_iff]
    let e (I : Ideal R) : R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := ⟨.id _, fun _ _ ↦ rfl⟩
    rw [(e _).isNoetherian_iff_of_bijective Function.bijective_id]
    refine @instIsNoetherianRingOfIsArtinianRing _ _ ?_
    rw [IsArtinianRing, ← (e _).isArtinian_iff_of_bijective Function.bijective_id,
      (LinearMap.quotKerEquivRange _).isArtinian_iff]
    infer_instance
-- Module: Mathlib.RingTheory.HopkinsLevitzki
Goal:
M : Type u
inst : AddCommGroup M
R : Type u_3
inst_1 : CommRing R
inst_2 : Module R M
inst_3 : Module.Finite R M
inst_4 : IsArtinian R M
s : Set M
fin : Finite.{u + 1} (↑s : Type u)
span : Eq.{u + 1} (α := Submodule R M) (⨆ (i : (↑s : Type u)), R ∙ (↑i : M)) ⊤
h : ∀ (i : M), IsNoetherian.{u_3, u} R ↥(R ∙ i)
⊢ IsNoetherian.{u_3, u} R ↥(⨆ (i : (↑s : Type u)), R ∙ (↑i : M))

Tactic:
infer_instance