feat(EuclideanDomain): drop DecidableEq assumptions (#10255)

Mathlib/RingTheory/EuclideanDomain.lean

@@ -81,29 +81,31 @@ def gcdMonoid (R) [EuclideanDomain R] [DecidableEq R] : GCDMonoid R where
   lcm_zero_right := lcm_zero_right
 #align euclidean_domain.gcd_monoid EuclideanDomain.gcdMonoid
 
-variable {α : Type*} [EuclideanDomain α] [DecidableEq α]
+variable {α : Type*} [EuclideanDomain α]
 
-theorem span_gcd (x y : α) :
+theorem span_gcd [DecidableEq α] (x y : α) :
     span ({gcd x y} : Set α) = span ({x, y} : Set α) :=
   letI := EuclideanDomain.gcdMonoid α
   _root_.span_gcd x y
 #align euclidean_domain.span_gcd EuclideanDomain.span_gcd
 
-theorem gcd_isUnit_iff {x y : α} : IsUnit (gcd x y) ↔ IsCoprime x y :=
+theorem gcd_isUnit_iff [DecidableEq α] {x y : α} : IsUnit (gcd x y) ↔ IsCoprime x y :=
   letI := EuclideanDomain.gcdMonoid α
   _root_.gcd_isUnit_iff x y
 #align euclidean_domain.gcd_is_unit_iff EuclideanDomain.gcd_isUnit_iff
 
 -- this should be proved for UFDs surely?
 theorem isCoprime_of_dvd {x y : α} (nonzero : ¬(x = 0 ∧ y = 0))
     (H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x y :=
+  letI := Classical.decEq α
   letI := EuclideanDomain.gcdMonoid α
   _root_.isCoprime_of_dvd x y nonzero H
 #align euclidean_domain.is_coprime_of_dvd EuclideanDomain.isCoprime_of_dvd
 
 -- this should be proved for UFDs surely?
 theorem dvd_or_coprime (x y : α) (h : Irreducible x) :
     x ∣ y ∨ IsCoprime x y :=
+  letI := Classical.decEq α
   letI := EuclideanDomain.gcdMonoid α
   _root_.dvd_or_coprime x y h
 #align euclidean_domain.dvd_or_coprime EuclideanDomain.dvd_or_coprime