feat(algebra/euclidean_domain): some cleanup (#3752)

Lower the priority of simp-lemmas which have an equivalent version in `group_with_zero`, so that the version of `group_with_zero` is found by `squeeze_simp` for types that have both structures.
Add docstrings
Remove outdated comment

Author: fpvandoorn

src/algebra/euclidean_domain.lean

@@ -14,24 +14,18 @@ universe u
 section prio
 set_option default_priority 100 -- see Note [default priority]
 set_option old_structure_cmd true
+/-- A Euclidean domain is an integral domain with quotient and remainder functions-/
 @[protect_proj without mul_left_not_lt r_well_founded]
 class euclidean_domain (α : Type u) extends comm_ring α, nontrivial α :=
 (quotient : α → α → α)
 (quotient_zero : ∀ a, quotient a 0 = 0)
 (remainder : α → α → α)
  -- This could be changed to the same order as int.mod_add_div.
- -- We normally write qb+r rather than r + qb though.
+ -- We normally write `qb+r` rather than `r + qb` though.
 (quotient_mul_add_remainder_eq : ∀ a b, b * quotient a b + remainder a b = a)
 (r : α → α → Prop)
 (r_well_founded : well_founded r)
 (remainder_lt : ∀ a {b}, b ≠ 0 → r (remainder a b) b)
-/- `val_le_mul_left` is often not a required in definitions of a euclidean
-  domain since given the other properties we can show there is a
-  (noncomputable) euclidean domain α with the property `val_le_mul_left`.
-  So potentially this definition could be split into two different ones
-  (euclidean_domain_weak and euclidean_domain_strong) with a noncomputable
-  function from weak to strong. I've currently divided the lemmas into
-  strong and weak depending on whether they require `val_le_mul_left` or not. -/
 (mul_left_not_lt : ∀ a {b}, b ≠ 0 → ¬r (a * b) a)
 end prio
 
@@ -104,15 +98,15 @@ mod_eq_zero.2 (one_dvd _)
 @[simp] lemma zero_mod (b : α) : 0 % b = 0 :=
 mod_eq_zero.2 (dvd_zero _)
 
-@[simp] lemma div_zero (a : α) : a / 0 = 0 :=
+@[simp, priority 900] lemma div_zero (a : α) : a / 0 = 0 :=
 euclidean_domain.quotient_zero a
 
-@[simp] lemma zero_div {a : α} : 0 / a = 0 :=
+@[simp, priority 900] lemma zero_div {a : α} : 0 / a = 0 :=
 classical.by_cases
   (λ a0 : a = 0, a0.symm ▸ div_zero 0)
   (λ a0, by simpa only [zero_mul] using mul_div_cancel 0 a0)
 
-@[simp] lemma div_self {a : α} (a0 : a ≠ 0) : a / a = 1 :=
+@[simp, priority 900] lemma div_self {a : α} (a0 : a ≠ 0) : a / a = 1 :=
 by simpa only [one_mul] using mul_div_cancel 1 a0
 
 lemma eq_div_of_mul_eq_left {a b c : α} (hb : b ≠ 0) (h : a * b = c) : a = c / b :=
@@ -148,6 +142,8 @@ end
 section gcd
 variable [decidable_eq α]
 
+/-- The greatest common denominator of two elements of a Euclidean domain.
+  It is defined using the Euclidean algorithm. -/
 def gcd : α → α → α
 | a := λ b, if a0 : a = 0 then b else
   have h:_ := mod_lt b a0,
@@ -195,6 +191,16 @@ gcd_eq_left.2 (one_dvd _)
 @[simp] theorem gcd_self (a : α) : gcd a a = a :=
 gcd_eq_left.2 (dvd_refl _)
 
+/--
+An implementation of the extended GCD algorithm.
+At each step we are computing a triple `(r, s, t)`, where `r` is the next value of the GCD
+algorithm, to compute the greatest common divisor of the input (say `x` and `y`), and `s` and `t`
+are the coefficients in front of `x` and `y` to obtain `r` (i.e. `r = s * x + t * y`).
+The function `xgcd_aux` takes in two triples, and from these recursively computes the next triple:
+```
+xgcd_aux (r, s, t) (r', s', t') = xgcd_aux (r' % r, s' - (r' / r) * s, t' - (r' / r) * t) (r, s, t)
+```
+-/
 def xgcd_aux : α → α → α → α → α → α → α × α × α
 | r := λ s t r' s' t',
 if hr : r = 0 then (r', s', t')
@@ -261,6 +267,7 @@ end gcd
 section lcm
 variables [decidable_eq α]
 
+/-- The least common multiple of two elements of a Euclidean domain. -/
 def lcm (x y : α) : α :=
 x * y / gcd x y
 

src/analysis/special_functions/trigonometric.lean

@@ -1408,8 +1408,7 @@ else
 lemma tan_arg {x : ℂ} : real.tan (arg x) = x.im / x.re :=
 begin
   by_cases h : x = 0,
-  { simp only [h, euclidean_domain.zero_div,
-    complex.zero_im, complex.arg_zero, real.tan_zero, complex.zero_re] },
+  { simp only [h, zero_div, complex.zero_im, complex.arg_zero, real.tan_zero, complex.zero_re] },
   rw [real.tan_eq_sin_div_cos, sin_arg, cos_arg h,
       div_div_div_cancel_right _ (mt abs_eq_zero.1 h)]
 end

src/analysis/specific_limits.lean

@@ -697,7 +697,7 @@ lemma self_div_two_le_harmonic_two_pow (n : ℕ) : (n / 2 : ℝ) ≤ harmonic_se
 begin
   induction n with n hn,
   unfold harmonic_series,
-  simp only [one_div, nat.cast_zero, euclidean_domain.zero_div, nat.cast_succ, sum_singleton,
+  simp only [one_div, nat.cast_zero, zero_div, nat.cast_succ, sum_singleton,
     inv_one, zero_add, nat.pow_zero, range_one, zero_le_one],
   have : harmonic_series (2^n) + 1 / 2 ≤ harmonic_series (2^(n+1)),
   { have := half_le_harmonic_double_sub_harmonic (2^n) (by {apply nat.pow_pos, linarith}),