feat: A dedekind domain that is local is a PID. (#9282)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib/RingTheory/Artinian.lean

@@ -448,8 +448,8 @@ theorem isNilpotent_jacobson_bot : IsNilpotent (Ideal.jacobson (⊥ : Ideal R))
     sup_le_sup_left (smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _
   have : Jac * Ideal.span {x} ≤ J := by -- Need version 4 of Nakayama's lemma on Stacks
     by_contra H
-    refine' H (smul_le_of_le_smul_of_le_jacobson_bot (fg_span_singleton _) le_rfl
-      (this.eq_of_not_lt (hJ' _ _)).ge)
+    refine H (Ideal.mul_le_left.trans (le_of_le_smul_of_le_jacobson_bot (fg_span_singleton _) le_rfl
+      (le_sup_right.trans_eq (this.eq_of_not_lt (hJ' _ ?_)).symm)))
     exact lt_of_le_of_ne le_sup_left fun h => H <| h.symm ▸ le_sup_right
   have : Ideal.span {x} * Jac ^ (n + 1) ≤ ⊥
   calc

Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

@@ -15,7 +15,7 @@ import Mathlib.RingTheory.Nakayama
 # Equivalent conditions for DVR
 
 In `DiscreteValuationRing.TFAE`, we show that the following are equivalent for a
-noetherian local domain `(R, m, k)`:
+noetherian local domain that is not a field `(R, m, k)`:
 - `R` is a discrete valuation ring
 - `R` is a valuation ring
 - `R` is a dedekind domain
@@ -24,20 +24,21 @@ noetherian local domain `(R, m, k)`:
 - `dimₖ m/m² = 1`
 - Every nonzero ideal is a power of `m`.
 
+Also see `tfae_of_isNoetherianRing_of_localRing_of_isDomain` for a version without `¬ IsField R`.
 -/
 
 
 variable (R : Type*) [CommRing R] (K : Type*) [Field K] [Algebra R K] [IsFractionRing R K]
 
-open scoped DiscreteValuation
+open scoped DiscreteValuation BigOperators
 
-open LocalRing
-
-open scoped BigOperators
+open LocalRing FiniteDimensional
 
 theorem exists_maximalIdeal_pow_eq_of_principal [IsNoetherianRing R] [LocalRing R] [IsDomain R]
-    (h : ¬IsField R) (h' : (maximalIdeal R).IsPrincipal) (I : Ideal R) (hI : I ≠ ⊥) :
+    (h' : (maximalIdeal R).IsPrincipal) (I : Ideal R) (hI : I ≠ ⊥) :
     ∃ n : ℕ, I = maximalIdeal R ^ n := by
+  by_cases h : IsField R;
+  · exact ⟨0, by simp [letI := h.toField; (eq_bot_or_eq_top I).resolve_left hI]⟩
   classical
   obtain ⟨x, hx : _ = Ideal.span _⟩ := h'
   by_cases hI' : I = ⊤
@@ -149,87 +150,42 @@ theorem maximalIdeal_isPrincipal_of_isDedekindDomain [LocalRing R] [IsDomain R]
     · rwa [Submodule.span_le, Set.singleton_subset_iff]
 #align maximal_ideal_is_principal_of_is_dedekind_domain maximalIdeal_isPrincipal_of_isDedekindDomain
 
-theorem DiscreteValuationRing.TFAE [IsNoetherianRing R] [LocalRing R] [IsDomain R]
-    (h : ¬IsField R) :
+/--
+Let `(R, m, k)` be a noetherian local domain (possibly a field).
+The following are equivalent:
+0. `R` is a PID
+1. `R` is a valuation ring
+2. `R` is a dedekind domain
+3. `R` is integrally closed with at most one non-zero prime ideal
+4. `m` is principal
+5. `dimₖ m/m² ≤ 1`
+6. Every nonzero ideal is a power of `m`.
+
+Also see `DiscreteValuationRing.TFAE` for a version assuming `¬ IsField R`.
+-/
+theorem tfae_of_isNoetherianRing_of_localRing_of_isDomain
+    [IsNoetherianRing R] [LocalRing R] [IsDomain R] :
     List.TFAE
-      [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R,
-        IsIntegrallyClosed R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime, (maximalIdeal R).IsPrincipal,
-        FiniteDimensional.finrank (ResidueField R) (CotangentSpace R) = 1,
+      [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
+        IsIntegrallyClosed R ∧ ∀ P : Ideal R, P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
+        (maximalIdeal R).IsPrincipal,
+        finrank (ResidueField R) (CotangentSpace R) ≤ 1,
         ∀ (I) (_ : I ≠ ⊥), ∃ n : ℕ, I = maximalIdeal R ^ n] := by
-  have ne_bot := Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
-  classical
-  rw [finrank_eq_one_iff']
   tfae_have 1 → 2
-  · intro; infer_instance
+  · exact fun _ ↦ inferInstance
   tfae_have 2 → 1
-  · intro
-    haveI := IsBezout.toGCDDomain R
-    haveI : UniqueFactorizationMonoid R := ufm_of_gcd_of_wfDvdMonoid
-    apply DiscreteValuationRing.of_ufd_of_unique_irreducible
-    · obtain ⟨x, hx₁, hx₂⟩ := Ring.exists_not_isUnit_of_not_isField h
-      obtain ⟨p, hp₁, -⟩ := WfDvdMonoid.exists_irreducible_factor hx₂ hx₁
-      exact ⟨p, hp₁⟩
-    · exact ValuationRing.unique_irreducible
+  · exact fun _ ↦ ((IsBezout.TFAE (R := R)).out 0 1).mp ‹_›
   tfae_have 1 → 4
   · intro H
-    exact ⟨inferInstance, ((DiscreteValuationRing.iff_pid_with_one_nonzero_prime R).mp H).2⟩
+    exact ⟨inferInstance, fun P hP hP' ↦ eq_maximalIdeal (hP'.isMaximal hP)⟩
   tfae_have 4 → 3
-  · rintro ⟨h₁, h₂⟩;
-    exact { h₁ with
-      maximalOfPrime := fun hI hI' => ExistsUnique.unique h₂ ⟨ne_bot, inferInstance⟩ ⟨hI, hI'⟩ ▸
-        maximalIdeal.isMaximal R, }
+  · exact fun ⟨h₁, h₂⟩ ↦ { h₁ with maximalOfPrime := (h₂ _ · · ▸ maximalIdeal.isMaximal R) }
   tfae_have 3 → 5
-  · intro h; exact maximalIdeal_isPrincipal_of_isDedekindDomain R
-  tfae_have 5 → 6
-  · rintro ⟨x, hx⟩
-    have : x ∈ maximalIdeal R := by rw [hx]; exact Submodule.subset_span (Set.mem_singleton x)
-    let x' : maximalIdeal R := ⟨x, this⟩
-    use Submodule.Quotient.mk x'
-    constructor
-    swap
-    · intro e
-      rw [Submodule.Quotient.mk_eq_zero] at e
-      apply Ring.ne_bot_of_isMaximal_of_not_isField (maximalIdeal.isMaximal R) h
-      apply Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (maximalIdeal R)
-      · exact ⟨{x}, (Finset.coe_singleton x).symm ▸ hx.symm⟩
-      · conv_lhs => rw [hx]
-        rw [Submodule.mem_smul_top_iff] at e
-        rwa [Submodule.span_le, Set.singleton_subset_iff]
-      · rw [LocalRing.jacobson_eq_maximalIdeal (⊥ : Ideal R) bot_ne_top]
-    · refine' fun w => Quotient.inductionOn' w fun y => _
-      obtain ⟨y, hy⟩ := y
-      rw [hx, Submodule.mem_span_singleton] at hy
-      obtain ⟨a, rfl⟩ := hy
-      exact ⟨Ideal.Quotient.mk _ a, rfl⟩
-  tfae_have 6 → 5
-  · rintro ⟨x, hx, hx'⟩
-    induction x using Quotient.inductionOn' with | h x => ?_
-    use x
-    apply le_antisymm
-    swap; · rw [Submodule.span_le, Set.singleton_subset_iff]; exact x.prop
-    have h₁ :
-      (Ideal.span {(x : R)} : Ideal R) ⊔ maximalIdeal R ≤
-        Ideal.span {(x : R)} ⊔ maximalIdeal R • maximalIdeal R := by
-      refine' sup_le le_sup_left _
-      rintro m hm
-      obtain ⟨c, hc⟩ := hx' (Submodule.Quotient.mk ⟨m, hm⟩)
-      induction c using Quotient.inductionOn' with | h c => ?_
-      rw [← sub_sub_cancel (c * x) m]
-      apply sub_mem _ _
-      · refine' Ideal.mem_sup_left (Ideal.mem_span_singleton'.mpr ⟨c, rfl⟩)
-      · have := (Submodule.Quotient.eq _).mp hc
-        rw [Submodule.mem_smul_top_iff] at this
-        exact Ideal.mem_sup_right this
-    have h₂ : maximalIdeal R ≤ (⊥ : Ideal R).jacobson := by
-      rw [LocalRing.jacobson_eq_maximalIdeal]
-      exact bot_ne_top
-    have :=
-      Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson (IsNoetherian.noetherian _) h₂ h₁
-    rw [Submodule.bot_smul, sup_bot_eq] at this
-    rw [← sup_eq_left, eq_comm]
-    exact le_sup_left.antisymm (h₁.trans <| le_of_eq this)
+  · exact fun h ↦ maximalIdeal_isPrincipal_of_isDedekindDomain R
+  tfae_have 6 ↔ 5
+  · exact finrank_cotangentSpace_le_one_iff
   tfae_have 5 → 7
-  · exact exists_maximalIdeal_pow_eq_of_principal R h
+  · exact exists_maximalIdeal_pow_eq_of_principal R
   tfae_have 7 → 2
   · rw [ValuationRing.iff_ideal_total]
     intro H
@@ -249,4 +205,54 @@ theorem DiscreteValuationRing.TFAE [IsNoetherianRing R] [LocalRing R] [IsDomain
     · left; exact Ideal.pow_le_pow_right h'
     · right; exact Ideal.pow_le_pow_right h'
   tfae_finish
+
+/--
+The following are equivalent for a
+noetherian local domain that is not a field `(R, m, k)`:
+0. `R` is a discrete valuation ring
+1. `R` is a valuation ring
+2. `R` is a dedekind domain
+3. `R` is integrally closed with a unique non-zero prime ideal
+4. `m` is principal
+5. `dimₖ m/m² = 1`
+6. Every nonzero ideal is a power of `m`.
+
+Also see `tfae_of_isNoetherianRing_of_localRing_of_isDomain` for a version without `¬ IsField R`.
+-/
+theorem DiscreteValuationRing.TFAE [IsNoetherianRing R] [LocalRing R] [IsDomain R]
+    (h : ¬IsField R) :
+    List.TFAE
+      [DiscreteValuationRing R, ValuationRing R, IsDedekindDomain R,
+        IsIntegrallyClosed R ∧ ∃! P : Ideal R, P ≠ ⊥ ∧ P.IsPrime, (maximalIdeal R).IsPrincipal,
+        finrank (ResidueField R) (CotangentSpace R) = 1,
+        ∀ (I) (_ : I ≠ ⊥), ∃ n : ℕ, I = maximalIdeal R ^ n] := by
+  have : finrank (ResidueField R) (CotangentSpace R) = 1 ↔
+    finrank (ResidueField R) (CotangentSpace R) ≤ 1
+  · simp [Nat.le_one_iff_eq_zero_or_eq_one, finrank_cotangentSpace_eq_zero_iff, h]
+  rw [this]
+  have : maximalIdeal R ≠ ⊥ := isField_iff_maximalIdeal_eq.not.mp h
+  convert tfae_of_isNoetherianRing_of_localRing_of_isDomain R
+  · exact ⟨fun _ ↦ inferInstance, fun h ↦ { h with not_a_field' := this }⟩
+  · exact ⟨fun h P h₁ h₂ ↦ h.unique ⟨h₁, h₂⟩ ⟨this, inferInstance⟩,
+      fun H ↦ ⟨_, ⟨this, inferInstance⟩, fun P hP ↦ H P hP.1 hP.2⟩⟩
 #align discrete_valuation_ring.tfae DiscreteValuationRing.TFAE
+
+variable {R}
+
+lemma LocalRing.finrank_CotangentSpace_eq_one_iff [IsNoetherianRing R] [LocalRing R] [IsDomain R] :
+    finrank (ResidueField R) (CotangentSpace R) = 1 ↔ DiscreteValuationRing R := by
+  by_cases hR : IsField R
+  · letI := hR.toField
+    simp only [finrank_cotangentSpace_eq_zero, zero_ne_one, false_iff]
+    exact fun h ↦ h.3 maximalIdeal_eq_bot
+  · exact (DiscreteValuationRing.TFAE R hR).out 5 0
+
+variable (R)
+
+lemma LocalRing.finrank_CotangentSpace_eq_one [IsDomain R] [DiscreteValuationRing R] :
+    finrank (ResidueField R) (CotangentSpace R) = 1 :=
+  finrank_CotangentSpace_eq_one_iff.mpr ‹_›
+
+instance (priority := 100) IsDedekindDomain.isPrincipalIdealRing
+    [LocalRing R] [IsDedekindDomain R] :
+    IsPrincipalIdealRing R := ((tfae_of_isNoetherianRing_of_localRing_of_isDomain R).out 2 0).mp ‹_›

Mathlib/RingTheory/Filtration.lean

@@ -472,6 +472,19 @@ theorem Ideal.iInf_pow_eq_bot_of_localRing [IsNoetherianRing R] [LocalRing R] (h
   rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one]
 #align ideal.infi_pow_eq_bot_of_local_ring Ideal.iInf_pow_eq_bot_of_localRing
 
+/-- Also see `Ideal.isIdempotentElem_iff_eq_bot_or_top` for integral domains. -/
+theorem Ideal.isIdempotentElem_iff_eq_bot_or_top_of_localRing {R} [CommRing R]
+    [IsNoetherianRing R] [LocalRing R] (I : Ideal R) :
+    IsIdempotentElem I ↔ I = ⊥ ∨ I = ⊤ := by
+  constructor
+  · intro H
+    by_cases I = ⊤; · exact Or.inr ‹_›
+    refine Or.inl (eq_bot_iff.mpr ?_)
+    rw [← Ideal.iInf_pow_eq_bot_of_localRing I ‹_›]
+    apply le_iInf
+    rintro (_|n) <;> simp [H.pow_succ_eq]
+  · rintro (rfl | rfl) <;> simp [IsIdempotentElem]
+
 /-- **Krull's intersection theorem** for noetherian domains. -/
 theorem Ideal.iInf_pow_eq_bot_of_isDomain [IsNoetherianRing R] [IsDomain R] (h : I ≠ ⊤) :
     ⨅ i : ℕ, I ^ i = ⊥ := by

Mathlib/RingTheory/Ideal/Cotangent.lean

@@ -8,6 +8,8 @@ import Mathlib.Algebra.Module.Torsion
 import Mathlib.Algebra.Ring.Idempotents
 import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.RingTheory.Ideal.LocalRing
+import Mathlib.RingTheory.Filtration
+import Mathlib.RingTheory.Nakayama
 
 #align_import ring_theory.ideal.cotangent from "leanprover-community/mathlib"@"4b92a463033b5587bb011657e25e4710bfca7364"
 
@@ -211,4 +213,50 @@ instance : IsScalarTower R (ResidueField R) (CotangentSpace R) :=
 instance [IsNoetherianRing R] : FiniteDimensional (ResidueField R) (CotangentSpace R) :=
   Module.Finite.of_restrictScalars_finite R _ _
 
+variable {R}
+
+lemma subsingleton_cotangentSpace_iff [IsNoetherianRing R] :
+    Subsingleton (CotangentSpace R) ↔ IsField R := by
+  refine (maximalIdeal R).cotangent_subsingleton_iff.trans ?_
+  rw [LocalRing.isField_iff_maximalIdeal_eq, Ideal.isIdempotentElem_iff_eq_bot_or_top_of_localRing]
+  simp [(maximalIdeal.isMaximal R).ne_top]
+
+lemma CotangentSpace.map_eq_top_iff [IsNoetherianRing R] {M : Submodule R (maximalIdeal R)} :
+    M.map (maximalIdeal R).toCotangent = ⊤ ↔ M = ⊤ := by
+  refine ⟨fun H ↦ eq_top_iff.mpr ?_, by rintro rfl; simp [Ideal.toCotangent_range]⟩
+  refine (Submodule.map_le_map_iff_of_injective (Submodule.injective_subtype _) _ _).mp ?_
+  rw [Submodule.map_top, Submodule.range_subtype]
+  apply Submodule.le_of_le_smul_of_le_jacobson_bot (IsNoetherian.noetherian _)
+    (LocalRing.jacobson_eq_maximalIdeal _ bot_ne_top).ge
+  rw [smul_eq_mul, ← pow_two, ← Ideal.map_toCotangent_ker, ← Submodule.map_sup,
+    ← Submodule.comap_map_eq, H, Submodule.comap_top, Submodule.map_top, Submodule.range_subtype]
+
+lemma CotangentSpace.span_image_eq_top_iff [IsNoetherianRing R] {s : Set (maximalIdeal R)} :
+    Submodule.span (ResidueField R) ((maximalIdeal R).toCotangent '' s) = ⊤ ↔
+      Submodule.span R s = ⊤ := by
+  rw [← map_eq_top_iff, ← (Submodule.restrictScalars_injective R ..).eq_iff,
+    Submodule.restrictScalars_span]
+  simp only [Ideal.toCotangent_apply, Submodule.restrictScalars_top, Submodule.map_span]
+  exact Ideal.Quotient.mk_surjective
+
+open FiniteDimensional
+
+lemma finrank_cotangentSpace_eq_zero_iff [IsNoetherianRing R] :
+    finrank (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R := by
+  rw [finrank_zero_iff, subsingleton_cotangentSpace_iff]
+
+lemma finrank_cotangentSpace_eq_zero (R) [Field R] :
+    finrank (ResidueField R) (CotangentSpace R) = 0 :=
+  finrank_cotangentSpace_eq_zero_iff.mpr (Field.toIsField R)
+
+open Submodule in
+theorem finrank_cotangentSpace_le_one_iff [IsNoetherianRing R] :
+    finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ (maximalIdeal R).IsPrincipal := by
+  rw [Module.finrank_le_one_iff_top_isPrincipal, IsPrincipal_iff,
+    (maximalIdeal R).toCotangent_surjective.exists, IsPrincipal_iff]
+  simp_rw [← Set.image_singleton, eq_comm (a := ⊤), CotangentSpace.span_image_eq_top_iff,
+    ← (map_injective_of_injective (injective_subtype _)).eq_iff, map_span, Set.image_singleton,
+    Submodule.map_top, range_subtype, eq_comm (a := maximalIdeal R)]
+  exact ⟨fun ⟨x, h⟩ ↦ ⟨_, h⟩, fun ⟨x, h⟩ ↦ ⟨⟨x, h ▸ subset_span (Set.mem_singleton x)⟩, h⟩⟩
+
 end LocalRing

Mathlib/RingTheory/Nakayama.lean

@@ -71,9 +71,10 @@ theorem eq_bot_of_le_smul_of_le_jacobson_bot (I : Ideal R) (N : Submodule R M) (
 #align submodule.eq_bot_of_le_smul_of_le_jacobson_bot Submodule.eq_bot_of_le_smul_of_le_jacobson_bot
 
 theorem sup_eq_sup_smul_of_le_smul_of_le_jacobson {I J : Ideal R} {N N' : Submodule R M}
-    (hN' : N'.FG) (hIJ : I ≤ jacobson J) (hNN : N ⊔ N' ≤ N ⊔ I • N') : N ⊔ N' = N ⊔ J • N' := by
+    (hN' : N'.FG) (hIJ : I ≤ jacobson J) (hNN : N' ≤ N ⊔ I • N') : N ⊔ N' = N ⊔ J • N' := by
   have hNN' : N ⊔ N' = N ⊔ I • N' :=
-    le_antisymm hNN (sup_le_sup_left (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _)
+    le_antisymm (sup_le le_sup_left hNN)
+    (sup_le_sup_left (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _)
   have h_comap := Submodule.comap_injective_of_surjective (LinearMap.range_eq_top.1 N.range_mkQ)
   have : (I • N').map N.mkQ = N'.map N.mkQ := by
     rw [← h_comap.eq_iff]
@@ -88,22 +89,22 @@ theorem sup_eq_sup_smul_of_le_smul_of_le_jacobson {I J : Ideal R} {N N' : Submod
 [Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
 See also `smul_le_of_le_smul_of_le_jacobson_bot` for the special case when `J = ⊥`.  -/
 theorem sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson {I J : Ideal R} {N N' : Submodule R M}
-    (hN' : N'.FG) (hIJ : I ≤ jacobson J) (hNN : N ⊔ N' ≤ N ⊔ I • N') : N ⊔ I • N' = N ⊔ J • N' :=
-  ((sup_le_sup_left smul_le_right _).antisymm hNN).trans
+    (hN' : N'.FG) (hIJ : I ≤ jacobson J) (hNN : N' ≤ N ⊔ I • N') : N ⊔ I • N' = N ⊔ J • N' :=
+  ((sup_le_sup_left smul_le_right _).antisymm (sup_le le_sup_left hNN)).trans
     (sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN)
 #align submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson Submodule.sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson
 
 theorem le_of_le_smul_of_le_jacobson_bot {R M} [CommRing R] [AddCommGroup M] [Module R M]
     {I : Ideal R} {N N' : Submodule R M} (hN' : N'.FG)
-    (hIJ : I ≤ jacobson ⊥) (hNN : N ⊔ N' ≤ N ⊔ I • N') : N' ≤ N := by
+    (hIJ : I ≤ jacobson ⊥) (hNN : N' ≤ N ⊔ I • N') : N' ≤ N := by
   rw [← sup_eq_left, sup_eq_sup_smul_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]
 
 /-- **Nakayama's Lemma** - Statement (4) in
 [Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
 See also `sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson` for a generalisation
 to the `jacobson` of any ideal -/
 theorem smul_le_of_le_smul_of_le_jacobson_bot {I : Ideal R} {N N' : Submodule R M} (hN' : N'.FG)
-    (hIJ : I ≤ jacobson ⊥) (hNN : N ⊔ N' ≤ N ⊔ I • N') : I • N' ≤ N :=
+    (hIJ : I ≤ jacobson ⊥) (hNN : N' ≤ N ⊔ I • N') : I • N' ≤ N :=
   smul_le_right.trans (le_of_le_smul_of_le_jacobson_bot hN' hIJ hNN)
 #align submodule.smul_le_of_le_smul_of_le_jacobson_bot Submodule.smul_le_of_le_smul_of_le_jacobson_bot
 

Mathlib/RingTheory/Valuation/ValuationRing.lean

@@ -356,10 +356,8 @@ instance (priority := 100) [ValuationRing R] : IsBezout R := by
   · erw [sup_eq_right.mpr h]; exact ⟨⟨_, rfl⟩⟩
   · erw [sup_eq_left.mpr h]; exact ⟨⟨_, rfl⟩⟩
 
-theorem iff_local_bezout_domain : ValuationRing R ↔ LocalRing R ∧ IsBezout R := by
+instance (priority := 100) [LocalRing R] [IsBezout R] : ValuationRing R := by
   classical
-  refine ⟨fun H => ⟨inferInstance, inferInstance⟩, ?_⟩
-  rintro ⟨h₁, h₂⟩
   refine iff_dvd_total.mpr ⟨fun a b => ?_⟩
   obtain ⟨g, e : _ = Ideal.span _⟩ := IsBezout.span_pair_isPrincipal a b
   obtain ⟨a, rfl⟩ := Ideal.mem_span_singleton'.mp
@@ -377,6 +375,9 @@ theorem iff_local_bezout_domain : ValuationRing R ↔ LocalRing R ∧ IsBezout R
   swap
   right
   all_goals exact mul_dvd_mul_right (isUnit_iff_forall_dvd.mp (isUnit_of_mul_isUnit_right h') _) _
+
+theorem iff_local_bezout_domain : ValuationRing R ↔ LocalRing R ∧ IsBezout R :=
+  ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ inferInstance⟩
 #align valuation_ring.iff_local_bezout_domain ValuationRing.iff_local_bezout_domain
 
 protected theorem tFAE (R : Type u) [CommRing R] [IsDomain R] :