feat: make isNoetherian_of_isNoetherianRing_of_finite an instance (#8999)

riccardobrasca · riccardobrasca · commit c4988d10a696 · 2023-12-13T18:20:22.000Z
Make `isNoetherian_of_isNoetherianRing_of_finite an instance`: this was impossible in Lean 3 because of a loop.
diff --git a/Mathlib/Algebra/DirectSum/LinearMap.lean b/Mathlib/Algebra/DirectSum/LinearMap.lean
@@ -17,9 +17,7 @@ domain and codomain.
 
 open Set BigOperators DirectSum
 
-attribute [local instance]
-  isNoetherian_of_isNoetherianRing_of_finite
-  Module.free_of_finite_type_torsion_free'
+attribute [local instance] Module.free_of_finite_type_torsion_free'
 
 variable {ι R M : Type*} [CommRing R] [AddCommGroup M] [Module R M]
   {N : ι → Submodule R M} [DecidableEq ι] (h : IsInternal N)
diff --git a/Mathlib/Algebra/Lie/Killing.lean b/Mathlib/Algebra/Lie/Killing.lean
@@ -54,7 +54,6 @@ variable (R K L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
   [Module.Free R M] [Module.Finite R M]
   [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [FiniteDimensional K M]
 
-attribute [local instance] isNoetherian_of_isNoetherianRing_of_finite
 attribute [local instance] Module.free_of_finite_type_torsion_free'
 
 local notation "φ" => LieModule.toEndomorphism R L M
diff --git a/Mathlib/Algebra/Lie/Weights/Linear.lean b/Mathlib/Algebra/Lie/Weights/Linear.lean
@@ -40,9 +40,7 @@ or `R` has characteristic zero.
 
 open Set
 
-attribute [local instance]
-  isNoetherian_of_isNoetherianRing_of_finite
-  Module.free_of_finite_type_torsion_free'
+attribute [local instance] Module.free_of_finite_type_torsion_free'
 
 variable (R L M : Type*) [CommRing R] [LieRing L] [LieAlgebra R L]
   [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M]
diff --git a/Mathlib/Algebra/Module/PID.lean b/Mathlib/Algebra/Module/PID.lean
@@ -243,7 +243,6 @@ theorem equiv_directSum_of_isTorsion [h' : Module.Finite R N] (hN : Module.IsTor
     ∀ i,
       ∃ (d : ℕ) (k : Fin d → ℕ),
         Nonempty <| torsionBy R N (p i ^ e i) ≃ₗ[R] ⨁ j, R ⧸ R ∙ p i ^ k j := by
-    have := isNoetherian_of_isNoetherianRing_of_finite R N
     haveI := fun i => isNoetherian_submodule' (torsionBy R N <| p i ^ e i)
     exact fun i =>
       torsion_by_prime_power_decomposition.{u, v} (hp i)
@@ -266,7 +265,6 @@ theorem equiv_directSum_of_isTorsion [h' : Module.Finite R N] (hN : Module.IsTor
 theorem equiv_free_prod_directSum [h' : Module.Finite R N] :
     ∃ (n : ℕ) (ι : Type u) (_ : Fintype ι) (p : ι → R) (_ : ∀ i, Irreducible <| p i) (e : ι → ℕ),
       Nonempty <| N ≃ₗ[R] (Fin n →₀ R) × ⨁ i : ι, R ⧸ R ∙ p i ^ e i := by
-  have := isNoetherian_of_isNoetherianRing_of_finite R N
   haveI := isNoetherian_submodule' (torsion R N)
   haveI := Module.Finite.of_surjective _ (torsion R N).mkQ_surjective
   obtain ⟨I, fI, p, hp, e, ⟨h⟩⟩ :=
diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean
@@ -352,8 +352,7 @@ theorem numberField [h : NumberField K] [Finite S] [IsCyclotomicExtension S K L]
 /-- A finite cyclotomic extension of an integral noetherian domain is integral -/
 theorem integral [IsDomain B] [IsNoetherianRing A] [Finite S] [IsCyclotomicExtension S A B] :
     Algebra.IsIntegral A B :=
-  letI := IsCyclotomicExtension.finite S A B; isIntegral_of_noetherian <|
-    isNoetherian_of_isNoetherianRing_of_finite A B
+  letI := IsCyclotomicExtension.finite S A B; isIntegral_of_noetherian inferInstance
 #align is_cyclotomic_extension.integral IsCyclotomicExtension.integral
 
 /-- If `S` is finite and `IsCyclotomicExtension S K A`, then `finiteDimensional K A`. -/
diff --git a/Mathlib/Probability/Cdf.lean b/Mathlib/Probability/Cdf.lean
@@ -69,8 +69,8 @@ lemma tendsto_cdf_atBot : Tendsto (cdf μ) atBot (𝓝 0) := tendsto_condCdf_atB
 /-- The cdf tends to 1 at +∞. -/
 lemma tendsto_cdf_atTop : Tendsto (cdf μ) atTop (𝓝 1) := tendsto_condCdf_atTop _ _
 
-set_option synthInstance.maxHeartbeats 25000 in
 lemma ofReal_cdf [IsProbabilityMeasure μ] (x : ℝ) : ENNReal.ofReal (cdf μ x) = μ (Iic x) := by
+  have := IsProbabilityMeasure.toIsFiniteMeasure (Measure.prod (Measure.dirac ()) μ)
   have h := lintegral_condCdf ((Measure.dirac Unit.unit).prod μ) x
   simpa only [MeasureTheory.Measure.fst_prod, Measure.prod_prod, measure_univ, one_mul,
     lintegral_dirac] using h
diff --git a/Mathlib/RingTheory/Adjoin/Tower.lean b/Mathlib/RingTheory/Adjoin/Tower.lean
@@ -157,7 +157,6 @@ theorem fg_of_fg_of_fg [IsNoetherianRing A] (hAC : (⊤ : Subalgebra A C).FG)
     Subalgebra.fg_of_submodule_fg <|
       have : IsNoetherianRing B₀ := isNoetherianRing_of_fg hAB₀
       have : Module.Finite B₀ C := ⟨hB₀C⟩
-      have : IsNoetherian B₀ C := isNoetherian_of_isNoetherianRing_of_finite B₀ C
       fg_of_injective (IsScalarTower.toAlgHom B₀ B C).toLinearMap hBCi
 #align fg_of_fg_of_fg fg_of_fg_of_fg
 
diff --git a/Mathlib/RingTheory/DedekindDomain/PID.lean b/Mathlib/RingTheory/DedekindDomain/PID.lean
@@ -239,8 +239,7 @@ theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime [DecidableEq (
     IsScalarTower.algebraMap_eq R (Localization.AtPrime p) Sₚ, ← Ideal.map_map,
     Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_le_iff_le_comap,
     hpu (LocalRing.maximalIdeal _) ⟨this, _⟩, hpu (comap _ _) ⟨_, _⟩]
-  · have hRS : Algebra.IsIntegral R S :=
-      isIntegral_of_noetherian (isNoetherian_of_isNoetherianRing_of_finite R S)
+  · have hRS : Algebra.IsIntegral R S := isIntegral_of_noetherian inferInstance
     exact mt (Ideal.eq_bot_of_comap_eq_bot (isIntegral_localization hRS)) hP0
   · exact Ideal.comap_isPrime (algebraMap (Localization.AtPrime p) Sₚ) P
   · exact (LocalRing.maximalIdeal.isMaximal _).isPrime
diff --git a/Mathlib/RingTheory/Filtration.lean b/Mathlib/RingTheory/Filtration.lean
@@ -404,7 +404,6 @@ variable {F}
 
 theorem Stable.of_le [IsNoetherianRing R] [Module.Finite R M] (hF : F.Stable)
     {F' : I.Filtration M} (hf : F' ≤ F) : F'.Stable := by
-  have := isNoetherian_of_isNoetherianRing_of_finite R M
   rw [← submodule_fg_iff_stable] at hF ⊢
   any_goals intro i; exact IsNoetherian.noetherian _
   have := isNoetherian_of_fg_of_noetherian _ hF
@@ -438,8 +437,7 @@ theorem Ideal.mem_iInf_smul_pow_eq_bot_iff [IsNoetherianRing R] [Module.Finite R
   have hN : ∀ k, (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N :=
     fun k => inf_eq_right.mpr ((iInf_le _ k).trans <| le_of_eq <| by simp)
   constructor
-  · have := isNoetherian_of_isNoetherianRing_of_finite R M
-    obtain ⟨r, hr₁, hr₂⟩ :=
+  · obtain ⟨r, hr₁, hr₂⟩ :=
       Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I N (IsNoetherian.noetherian N) (by
         obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
         have := hk k (le_refl _)
diff --git a/Mathlib/RingTheory/Noetherian.lean b/Mathlib/RingTheory/Noetherian.lean
@@ -594,9 +594,7 @@ theorem isNoetherian_of_fg_of_noetherian {R M} [Ring R] [AddCommGroup M] [Module
     rw [Finsupp.not_mem_support_iff.1 hx, zero_smul]
 #align is_noetherian_of_fg_of_noetherian isNoetherian_of_fg_of_noetherian
 
--- It would be nice to make this an instance but it is empirically problematic, possibly because
--- of the loop that it causes with `Module.IsNoetherian.finite`
-theorem isNoetherian_of_isNoetherianRing_of_finite (R M : Type*)
+instance isNoetherian_of_isNoetherianRing_of_finite (R M : Type*)
     [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] :
     IsNoetherian R M :=
   have : IsNoetherian R (⊤ : Submodule R M) :=
