fix(ring_theory/power_series/basic): remove duplicate instance (#12744)

src/ring_theory/power_series/basic.lean

@@ -648,7 +648,7 @@ section comm_ring
 variable [comm_ring R]
 
 /-- Multivariate formal power series over a local ring form a local ring. -/
-instance is_local_ring [local_ring R] : local_ring (mv_power_series σ R) :=
+instance [local_ring R] : local_ring (mv_power_series σ R) :=
 { is_local := by { intro φ, rcases local_ring.is_local (constant_coeff σ R φ) with ⟨u,h⟩|⟨u,h⟩;
     [left, right];
     { refine is_unit_of_mul_eq_one _ _ (mul_inv_of_unit _ u _),
@@ -677,11 +677,6 @@ instance map.is_local_ring_hom : is_local_ring_hom (map σ f) :=
   exact is_unit_of_mul_eq_one φ (inv_of_unit φ c) (mul_inv_of_unit φ c hc.symm)
 end⟩
 
-variables [local_ring R] [local_ring S]
-
-instance : local_ring (mv_power_series σ R) :=
-{ is_local := local_ring.is_local }
-
 end local_ring
 
 section field