feat: port RingTheory.Valuation.ValuationSubring (#4791)

Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com>

Mathlib.lean

@@ -2651,6 +2651,7 @@ import Mathlib.RingTheory.Valuation.Integers
 import Mathlib.RingTheory.Valuation.Integral
 import Mathlib.RingTheory.Valuation.Quotient
 import Mathlib.RingTheory.Valuation.ValuationRing
+import Mathlib.RingTheory.Valuation.ValuationSubring
 import Mathlib.RingTheory.WittVector.Basic
 import Mathlib.RingTheory.WittVector.Defs
 import Mathlib.RingTheory.WittVector.IsPoly

Mathlib/Order/RelClasses.lean

@@ -862,7 +862,7 @@ instance [PartialOrder α] : IsPartialOrder α (· ≤ ·) where
 
 instance [PartialOrder α] : IsPartialOrder α (· ≥ ·) where
 
-instance [LinearOrder α] : IsTotal α (· ≤ ·) :=
+instance LE.isTotal [LinearOrder α] : IsTotal α (· ≤ ·) :=
   ⟨le_total⟩
 
 instance [LinearOrder α] : IsTotal α (· ≥ ·) :=

Mathlib/RingTheory/Valuation/ValuationRing.lean

@@ -148,7 +148,8 @@ noncomputable instance : LinearOrder (ValueGroup A K) where
   le_total := ValuationRing.le_total _ _
   decidableLE := by classical infer_instance
 
-noncomputable instance : LinearOrderedCommGroupWithZero (ValueGroup A K) where
+noncomputable instance linearOrderedCommGroupWithZero :
+    LinearOrderedCommGroupWithZero (ValueGroup A K) where
   mul_assoc := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩; apply Quotient.sound'; rw [mul_assoc]; apply Setoid.refl'
   one_mul := by rintro ⟨a⟩; apply Quotient.sound'; rw [one_mul]; apply Setoid.refl'
   mul_one := by rintro ⟨a⟩; apply Quotient.sound'; rw [mul_one]; apply Setoid.refl'
@@ -247,7 +248,7 @@ section
 
 variable (A : Type u) [CommRing A] [IsDomain A] [ValuationRing A]
 
-instance (priority := 100) : LocalRing A :=
+instance (priority := 100) localRing : LocalRing A :=
   LocalRing.of_isUnit_or_isUnit_one_sub_self
     (by
       intro a