refactor: golf #6309 (#6676)

Also changes a lemma to instance and adds a new instance.



Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/RingTheory/Artinian.lean

@@ -322,8 +322,8 @@ theorem isArtinian_of_submodule_of_artinian (R M) [Ring R] [AddCommGroup M] [Mod
     (N : Submodule R M) (_ : IsArtinian R M) : IsArtinian R N := inferInstance
 #align is_artinian_of_submodule_of_artinian isArtinian_of_submodule_of_artinian
 
-theorem isArtinian_of_quotient_of_artinian (R) [Ring R] (M) [AddCommGroup M] [Module R M]
-    (N : Submodule R M) (_ : IsArtinian R M) : IsArtinian R (M ⧸ N) :=
+instance isArtinian_of_quotient_of_artinian (R) [Ring R] (M) [AddCommGroup M] [Module R M]
+    (N : Submodule R M) [IsArtinian R M] : IsArtinian R (M ⧸ N) :=
   isArtinian_of_surjective M (Submodule.mkQ N) (Submodule.Quotient.mk_surjective N)
 #align is_artinian_of_quotient_of_artinian isArtinian_of_quotient_of_artinian
 
@@ -334,6 +334,9 @@ theorem isArtinian_of_tower (R) {S M} [CommRing R] [Ring S] [AddCommGroup M] [Al
   refine' (Submodule.restrictScalarsEmbedding R S M).wellFounded h
 #align is_artinian_of_tower isArtinian_of_tower
 
+instance (R) [CommRing R] [IsArtinianRing R] (I : Ideal R) : IsArtinianRing (R ⧸ I) :=
+  isArtinian_of_tower R inferInstance
+
 theorem isArtinian_of_fg_of_artinian {R M} [Ring R] [AddCommGroup M] [Module R M]
     (N : Submodule R M) [IsArtinianRing R] (hN : N.FG) : IsArtinian R N := by
   let ⟨s, hs⟩ := hN
@@ -418,28 +421,6 @@ theorem isNilpotent_jacobson_bot : IsNilpotent (Ideal.jacobson (⊥ : Ideal R))
   rwa [← hn (n + 1) (Nat.le_succ _)]
 #align is_artinian_ring.is_nilpotent_jacobson_bot IsArtinianRing.isNilpotent_jacobson_bot
 
-instance isMaximal_of_isPrime (p : Ideal R) [p.IsPrime] : p.IsMaximal :=
-  Ideal.Quotient.maximal_of_isField _
-  { exists_pair_ne := ⟨0, 1, zero_ne_one⟩
-    mul_comm := mul_comm
-    mul_inv_cancel := fun {x} hx => by
-      have : IsArtinianRing (R ⧸ p) := (@Ideal.Quotient.mk_surjective R _ p).isArtinianRing
-      obtain ⟨n, hn⟩ : ∃ (n : ℕ), Ideal.span {x^n} = Ideal.span {x^(n+1)}
-      · obtain ⟨n, h⟩ := IsArtinian.monotone_stabilizes (R := R ⧸ p) (M := R ⧸ p)
-          ⟨fun m => OrderDual.toDual (Ideal.span {x^m}), fun m n h y hy => by
-            dsimp [OrderDual.toDual] at *
-            rw [Ideal.mem_span_singleton] at hy ⊢
-            obtain ⟨z, rfl⟩ := hy
-            exact dvd_mul_of_dvd_left (pow_dvd_pow _ h) _⟩
-        exact ⟨n, h (n + 1) <| by norm_num⟩
-      have H : x^n ∈ Ideal.span {x^(n+1)}
-      { rw [← hn]; refine Submodule.subset_span (Set.mem_singleton _) }
-      rw [Ideal.mem_span_singleton] at H
-      obtain ⟨y, hy⟩ := H
-      rw [pow_add, mul_assoc, pow_one] at hy
-      conv_lhs at hy => rw [←mul_one (x^n)]
-      exact ⟨y, mul_left_cancel₀ (pow_ne_zero _ hx) hy.symm⟩ }
-
 section Localization
 
 variable (S : Submonoid R) (L : Type*) [CommRing L] [Algebra R L] [IsLocalization S L]
@@ -471,4 +452,10 @@ instance : IsArtinianRing (Localization S) :=
 
 end Localization
 
+instance isMaximal_of_isPrime (p : Ideal R) [p.IsPrime] : p.IsMaximal :=
+  Ideal.Quotient.maximal_of_isField _ <|
+    (MulEquiv.ofBijective _ ⟨IsFractionRing.injective (R ⧸ p) (FractionRing (R ⧸ p)),
+      localization_surjective (nonZeroDivisors (R ⧸ p)) (FractionRing (R ⧸ p))⟩).isField _
+    <| Field.toIsField <| FractionRing (R ⧸ p)
+
 end IsArtinianRing