-- Mathlib/RingTheory/HopkinsLevitzki.lean
theorem isNoetherian_of_finite_isArtinian {R} [CommRing R] [Module R M]
    [Module.Finite R M] [IsArtinian R M] : IsNoetherian R M

Proof state:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : s.Finite
span : Submodule.span R s = ⊤
⊢ IsNoetherian R M

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

Result:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : s.Finite
span : ⨆ i, Submodule.span R {↑i} = ⊤
⊢ IsNoetherian R M

Proof state:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : s.Finite
span : ⨆ i, Submodule.span R {↑i} = ⊤
⊢ IsNoetherian R M

Tactic:
rw [← Set.finite_coe_iff] at fin

Result:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
⊢ IsNoetherian R M

Proof state:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I => { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinianRing (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))

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

Result:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I => { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinian R ↥(LinearMap.range (LinearMap.toSpanSingleton R M i))

Proof state:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
⊢ IsNoetherian R M

Tactic:
rw [← isNoetherian_top_iff, ← span]

Result:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
⊢ IsNoetherian R ↥(⨆ i, Submodule.span R {↑i})

Proof state:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
⊢ IsNoetherian R ↥(⨆ i, Submodule.span 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

Result:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
x✝ : ∀ (i : M), IsNoetherian R ↥(Submodule.span R {i})
⊢ IsNoetherian R ↥(⨆ i, Submodule.span R {↑i})

Proof state:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I => { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsNoetherian R (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))

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

Result:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I => { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsNoetherian (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))
    (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))

Proof state:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
x✝ : ∀ (i : M), IsNoetherian R ↥(Submodule.span R {i})
⊢ IsNoetherian R ↥(⨆ i, Submodule.span R {↑i})

Tactic:
infer_instance

Result:
no goals

Proof state:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I => { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsNoetherian (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))
    (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))

Tactic:
refine @instIsNoetherianRingOfIsArtinianRing _ _ ?_

Result:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I => { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinianRing (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))

Proof state:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
e : (I : Ideal R) → R ⧸ I →ₛₗ[Ideal.Quotient.mk I] R ⧸ I := fun I => { toAddHom := AddHom.id (R ⧸ I), map_smul' := ⋯ }
⊢ IsArtinian R ↥(LinearMap.range (LinearMap.toSpanSingleton R M i))

Tactic:
infer_instance

Result:
no goals

Proof state:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
⊢ IsNoetherian R M

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

Result:
case intro.intro
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : s.Finite
span : Submodule.span R s = ⊤
⊢ IsNoetherian R M

Proof state:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
⊢ IsNoetherian R ↥(Submodule.span R {i})

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

Result:
M : Type u
inst✝⁴ : AddCommGroup M
R : Type u_3
inst✝³ : CommRing R
inst✝² : Module R M
inst✝¹ : Module.Finite R M
inst✝ : IsArtinian R M
s : Set M
fin : Finite ↑s
span : ⨆ i, Submodule.span R {↑i} = ⊤
i : M
⊢ IsNoetherian R (R ⧸ LinearMap.ker (LinearMap.toSpanSingleton R M i))