From 59291cd6b565a11235d8ba3b3859044136ee2166 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 29 Jul 2023 10:38:03 +0000
Subject: [PATCH] fix: make EuclideanDomain.gcdMonoid computable (#6076)

This of course still works non-computably in the presence of `Classical.decEq`, but the caller now has the option.
---
 Mathlib/RingTheory/EuclideanDomain.lean | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/Mathlib/RingTheory/EuclideanDomain.lean b/Mathlib/RingTheory/EuclideanDomain.lean
index 14035d7f1d582..b5a9acba27f03 100644
--- a/Mathlib/RingTheory/EuclideanDomain.lean
+++ b/Mathlib/RingTheory/EuclideanDomain.lean
@@ -23,9 +23,7 @@ euclidean domain
 -/
 
 
-noncomputable section
-
-open Classical
+section
 
 open EuclideanDomain Set Ideal
 
@@ -71,7 +69,8 @@ end GCDMonoid
 namespace EuclideanDomain
 
 /-- Create a `GCDMonoid` whose `GCDMonoid.gcd` matches `EuclideanDomain.gcd`. -/
-def gcdMonoid (R) [EuclideanDomain R] : GCDMonoid R where
+-- porting note: added `DecidableEq R`
+def gcdMonoid (R) [EuclideanDomain R] [DecidableEq R] : GCDMonoid R where
   gcd := gcd
   lcm := lcm
   gcd_dvd_left := gcd_dvd_left
@@ -84,26 +83,26 @@ def gcdMonoid (R) [EuclideanDomain R] : GCDMonoid R where
 
 variable {α : Type _} [EuclideanDomain α] [DecidableEq α]
 
-theorem span_gcd {α} [EuclideanDomain α] (x y : α) :
+theorem span_gcd (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 {α} [EuclideanDomain α] {x y : α} : IsUnit (gcd x y) ↔ IsCoprime x y :=
+theorem gcd_isUnit_iff {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 {α} [EuclideanDomain α] {x y : α} (nonzero : ¬(x = 0 ∧ y = 0))
+theorem isCoprime_of_dvd {x y : α} (nonzero : ¬(x = 0 ∧ y = 0))
     (H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x y :=
   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 {α} [EuclideanDomain α] (x y : α) (h : Irreducible x) :
+theorem dvd_or_coprime (x y : α) (h : Irreducible x) :
     x ∣ y ∨ IsCoprime x y :=
   letI := EuclideanDomain.gcdMonoid α
   _root_.dvd_or_coprime x y h