diff --git a/src/algebra/associated.lean b/src/algebra/associated.lean
index af46a9205d880..f2abcb4255a80 100644
--- a/src/algebra/associated.lean
+++ b/src/algebra/associated.lean
@@ -19,11 +19,11 @@ theorem is_unit_iff_dvd_one [comm_monoid α] {x : α} : is_unit x ↔ x ∣ 1 :=
 
 theorem is_unit_iff_forall_dvd [comm_monoid α] {x : α} :
   is_unit x ↔ ∀ y, x ∣ y :=
-is_unit_iff_dvd_one.trans ⟨λ h y, dvd.trans h (one_dvd _), λ h, h _⟩
+is_unit_iff_dvd_one.trans ⟨λ h y, h.trans (one_dvd _), λ h, h _⟩
 
 theorem is_unit_of_dvd_unit {α} [comm_monoid α] {x y : α}
   (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
-is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
+is_unit_iff_dvd_one.2 $ xy.trans $ is_unit_iff_dvd_one.1 hu
 
 lemma is_unit_of_dvd_one [comm_monoid α] : ∀a ∣ 1, is_unit (a:α)
 | a ⟨b, eq⟩ := ⟨units.mk_of_mul_eq_one a b eq.symm, rfl⟩
@@ -42,7 +42,7 @@ begin
   split,
   { intro h, rw [← not_lt], intro hmn, apply h1,
     have : x ^ m * x ∣ x ^ m * 1,
-    { rw [← pow_succ', mul_one], exact dvd_trans (pow_dvd_pow _ (nat.succ_le_of_lt hmn)) h },
+    { rw [← pow_succ', mul_one], exact (pow_dvd_pow _ (nat.succ_le_of_lt hmn)).trans h },
     rwa [mul_dvd_mul_iff_left, ← is_unit_iff_dvd_one] at this, apply pow_ne_zero m h0 },
   { apply pow_dvd_pow }
 end
@@ -163,7 +163,7 @@ begin
   exact H _ o.1 _ o.2 h.symm
 end
 
-lemma irreducible_of_prime [comm_cancel_monoid_with_zero α] {p : α} (hp : prime p) :
+protected lemma prime.irreducible [comm_cancel_monoid_with_zero α] {p : α} (hp : prime p) :
   irreducible p :=
 ⟨hp.not_unit, λ a b hab,
   (show a * b ∣ a ∨ a * b ∣ b, from hab ▸ hp.dvd_or_dvd (hab ▸ (dvd_refl _))).elim
@@ -187,7 +187,7 @@ have hpd : p ∣ x * y, from ⟨z, by rwa [mul_right_inj' hp0] at h⟩,
   (λ ⟨d, hd⟩, or.inr ⟨d, by simp [*, pow_succ, mul_comm, mul_left_comm, mul_assoc]⟩)
 
 /-- If `p` and `q` are irreducible, then `p ∣ q` implies `q ∣ p`. -/
-lemma dvd_symm_of_irreducible [monoid α] {p q : α}
+lemma irreducible.dvd_symm [monoid α] {p q : α}
   (hp : irreducible p) (hq : irreducible q) : p ∣ q → q ∣ p :=
 begin
   tactic.unfreeze_local_instances,
@@ -195,9 +195,9 @@ begin
   rw is_unit.mul_right_dvd (or.resolve_left (of_irreducible_mul hq) hp.not_unit),
 end
 
-lemma dvd_symm_iff_of_irreducible [monoid α] {p q : α}
+lemma irreducible.dvd_comm [monoid α] {p q : α}
   (hp : irreducible p) (hq : irreducible q) : p ∣ q ↔ q ∣ p :=
-⟨dvd_symm_of_irreducible hp hq, dvd_symm_of_irreducible hq hp⟩
+⟨hp.dvd_symm hq, hq.dvd_symm hp⟩
 
 /-- Two elements of a `monoid` are `associated` if one of them is another one
 multiplied by a unit on the right. -/
@@ -242,22 +242,30 @@ theorem associated_one_of_associated_mul_one [comm_monoid α] {a b : α} :
   a * b ~ᵤ 1 → a ~ᵤ 1
 | ⟨u, h⟩ := associated_one_of_mul_eq_one (b * u) $ by simpa [mul_assoc] using h
 
-lemma associated_mul_mul [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
+lemma associated.mul_mul [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
   a₁ ~ᵤ b₁ → a₂ ~ᵤ b₂ → (a₁ * a₂) ~ᵤ (b₁ * b₂)
 | ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ := ⟨c₁ * c₂, by simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]⟩
 
-lemma associated_pow_pow [comm_monoid α] {a b : α} {n : ℕ} (h : a ~ᵤ b) :
+lemma associated.mul_left [comm_monoid α] (a : α) {b c : α} (h : b ~ᵤ c) :
+  (a * b) ~ᵤ (a * c) :=
+(associated.refl a).mul_mul h
+
+lemma associated.mul_right [comm_monoid α] {a b : α} (h : a ~ᵤ b) (c : α) :
+  (a * c) ~ᵤ (b * c) :=
+h.mul_mul (associated.refl c)
+
+lemma associated.pow_pow [comm_monoid α] {a b : α} {n : ℕ} (h : a ~ᵤ b) :
   a ^ n ~ᵤ b ^ n :=
 begin
   induction n with n ih, { simp [h] },
-  convert associated_mul_mul h ih;
-  rw pow_succ
+  convert h.mul_mul ih;
+    rw pow_succ
 end
 
-lemma dvd_of_associated [monoid α] {a b : α} : a ~ᵤ b → a ∣ b := λ ⟨u, hu⟩, ⟨u, hu.symm⟩
+protected lemma associated.dvd [monoid α] {a b : α} : a ~ᵤ b → a ∣ b := λ ⟨u, hu⟩, ⟨u, hu.symm⟩
 
-lemma dvd_dvd_of_associated [monoid α] {a b : α} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a :=
-⟨dvd_of_associated h, dvd_of_associated h.symm⟩
+protected lemma associated.dvd_dvd [monoid α] {a b : α} (h : a ~ᵤ b) : a ∣ b ∧ b ∣ a :=
+⟨h.dvd, h.symm.dvd⟩
 
 theorem associated_of_dvd_dvd [cancel_monoid_with_zero α]
   {a b : α} (hab : a ∣ b) (hba : b ∣ a) : a ~ᵤ b :=
@@ -276,7 +284,7 @@ begin
 end
 
 theorem dvd_dvd_iff_associated [cancel_monoid_with_zero α] {a b : α} : a ∣ b ∧ b ∣ a ↔ a ~ᵤ b :=
-⟨λ ⟨h1, h2⟩, associated_of_dvd_dvd h1 h2, dvd_dvd_of_associated⟩
+⟨λ ⟨h1, h2⟩, associated_of_dvd_dvd h1 h2, associated.dvd_dvd⟩
 
 lemma exists_associated_mem_of_dvd_prod [comm_cancel_monoid_with_zero α] {p : α}
   (hp : prime p) {s : multiset α} : (∀ r ∈ s, prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
@@ -286,64 +294,66 @@ multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.not_unit])
     cases hp.dvd_or_dvd hps with h h,
     { use [a, by simp],
       cases h with u hu,
-      cases ((irreducible_of_prime (hs a (multiset.mem_cons.2
-        (or.inl rfl)))).is_unit_or_is_unit hu).resolve_left hp.not_unit with v hv,
+      cases (((hs a (multiset.mem_cons.2 (or.inl rfl))).irreducible)
+        .is_unit_or_is_unit hu).resolve_left hp.not_unit with v hv,
       exact ⟨v, by simp [hu, hv]⟩ },
     { rcases ih (λ r hr, hs _ (multiset.mem_cons.2 (or.inr hr))) h with ⟨q, hq₁, hq₂⟩,
       exact ⟨q, multiset.mem_cons.2 (or.inr hq₁), hq₂⟩ }
   end)
 
-lemma dvd_iff_dvd_of_rel_left [monoid α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
+lemma associated.dvd_iff_dvd_left [monoid α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
 let ⟨u, hu⟩ := h in hu ▸ units.mul_right_dvd.symm
 
-lemma dvd_iff_dvd_of_rel_right [monoid α] {a b c : α} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c :=
+lemma associated.dvd_iff_dvd_right [monoid α] {a b c : α} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c :=
 let ⟨u, hu⟩ := h in hu ▸ units.dvd_mul_right.symm
 
-lemma eq_zero_iff_of_associated [monoid_with_zero α] {a b : α} (h : a ~ᵤ b) : a = 0 ↔ b = 0 :=
+lemma associated.eq_zero_iff [monoid_with_zero α] {a b : α} (h : a ~ᵤ b) : a = 0 ↔ b = 0 :=
 ⟨λ ha, let ⟨u, hu⟩ := h in by simp [hu.symm, ha],
   λ hb, let ⟨u, hu⟩ := h.symm in by simp [hu.symm, hb]⟩
 
-lemma ne_zero_iff_of_associated [monoid_with_zero α] {a b : α} (h : a ~ᵤ b) : a ≠ 0 ↔ b ≠ 0 :=
-not_congr $ eq_zero_iff_of_associated h
+lemma associated.ne_zero_iff [monoid_with_zero α] {a b : α} (h : a ~ᵤ b) : a ≠ 0 ↔ b ≠ 0 :=
+not_congr h.eq_zero_iff
 
-lemma prime_of_associated [comm_monoid_with_zero α] {p q : α} (h : p ~ᵤ q) (hp : prime p) :
+protected lemma associated.prime [comm_monoid_with_zero α] {p q : α} (h : p ~ᵤ q) (hp : prime p) :
   prime q :=
-⟨(ne_zero_iff_of_associated h).1 hp.ne_zero,
+⟨h.ne_zero_iff.1 hp.ne_zero,
   let ⟨u, hu⟩ := h in
     ⟨λ ⟨v, hv⟩, hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩,
       hu ▸ by { simp [units.mul_right_dvd], intros a b, exact hp.dvd_or_dvd }⟩⟩
 
-lemma associated_of_irreducible_of_dvd [cancel_monoid_with_zero α] {p q : α}
+lemma irreducible.associated_of_dvd [cancel_monoid_with_zero α] {p q : α}
   (p_irr : irreducible p) (q_irr : irreducible q) (dvd : p ∣ q) : associated p q :=
-associated_of_dvd_dvd dvd (dvd_symm_of_irreducible p_irr q_irr dvd)
+associated_of_dvd_dvd dvd (p_irr.dvd_symm q_irr dvd)
 
-lemma associated_of_prime_of_dvd [comm_cancel_monoid_with_zero α] {p q : α}
+lemma prime.associated_of_dvd [comm_cancel_monoid_with_zero α] {p q : α}
   (p_prime : prime p) (q_prime : prime q) (dvd : p ∣ q) : associated p q :=
-associated_of_irreducible_of_dvd (irreducible_of_prime p_prime) (irreducible_of_prime q_prime) dvd
+p_prime.irreducible.associated_of_dvd q_prime.irreducible dvd
 
-lemma prime_iff_of_associated [comm_monoid_with_zero α] {p q : α}
+lemma associated.prime_iff [comm_monoid_with_zero α] {p q : α}
   (h : p ~ᵤ q) : prime p ↔ prime q :=
-⟨prime_of_associated h, prime_of_associated h.symm⟩
+⟨h.prime, h.symm.prime⟩
+
+protected lemma associated.is_unit [monoid α] {a b : α} (h :  a ~ᵤ b) : is_unit a → is_unit b :=
+let ⟨u, hu⟩ := h in λ ⟨v, hv⟩, ⟨v * u, by simp [hv, hu.symm]⟩
 
-lemma is_unit_iff_of_associated [monoid α] {a b : α} (h :  a ~ᵤ b) : is_unit a ↔ is_unit b :=
-⟨let ⟨u, hu⟩ := h in λ ⟨v, hv⟩, ⟨v * u, by simp [hv, hu.symm]⟩,
-  let ⟨u, hu⟩ := h.symm in λ ⟨v, hv⟩, ⟨v * u, by simp [hv, hu.symm]⟩⟩
+lemma associated.is_unit_iff [monoid α] {a b : α} (h :  a ~ᵤ b) : is_unit a ↔ is_unit b :=
+⟨h.is_unit, h.symm.is_unit⟩
 
-lemma irreducible_of_associated [monoid α] {p q : α} (h : p ~ᵤ q)
+protected lemma associated.irreducible [monoid α] {p q : α} (h : p ~ᵤ q)
   (hp : irreducible p) : irreducible q :=
-⟨mt (is_unit_iff_of_associated h).2 hp.1,
+⟨mt h.symm.is_unit hp.1,
   let ⟨u, hu⟩ := h in λ a b hab,
   have hpab : p = a * (b * (u⁻¹ : units α)),
     from calc p = (p * u) * (u ⁻¹ : units α) : by simp
       ... = _ : by rw hu; simp [hab, mul_assoc],
   (hp.is_unit_or_is_unit hpab).elim or.inl (λ ⟨v, hv⟩, or.inr ⟨v * u, by simp [hv]⟩)⟩
 
-lemma irreducible_iff_of_associated [monoid α] {p q : α} (h : p ~ᵤ q) :
+protected lemma associated.irreducible_iff [monoid α] {p q : α} (h : p ~ᵤ q) :
   irreducible p ↔ irreducible q :=
-⟨irreducible_of_associated h, irreducible_of_associated h.symm⟩
+⟨h.irreducible, h.symm.irreducible⟩
 
-lemma associated_mul_left_cancel [comm_cancel_monoid_with_zero α] {a b c d : α}
-(h : a * b ~ᵤ c * d) (h₁ : a ~ᵤ c) (ha : a ≠ 0) : b ~ᵤ d :=
+lemma associated.of_mul_left [comm_cancel_monoid_with_zero α] {a b c d : α}
+  (h : a * b ~ᵤ c * d) (h₁ : a ~ᵤ c) (ha : a ≠ 0) : b ~ᵤ d :=
 let ⟨u, hu⟩ := h in let ⟨v, hv⟩ := associated.symm h₁ in
 ⟨u * (v : units α), mul_left_cancel' ha
   begin
@@ -351,9 +361,9 @@ let ⟨u, hu⟩ := h in let ⟨v, hv⟩ := associated.symm h₁ in
     simp [hv.symm, mul_assoc, mul_comm, mul_left_comm]
   end⟩
 
-lemma associated_mul_right_cancel [comm_cancel_monoid_with_zero α] {a b c d : α} :
+lemma associated.of_mul_right [comm_cancel_monoid_with_zero α] {a b c d : α} :
   a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c :=
-by rw [mul_comm a, mul_comm c]; exact associated_mul_left_cancel
+by rw [mul_comm a, mul_comm c]; exact associated.of_mul_left
 
 section unique_units
 variables [monoid α] [unique (units α)]
@@ -625,7 +635,7 @@ begin
     cases hbax with u hu,
     apply h (x * ↑u⁻¹),
     { rw is_unit_mk at hx,
-      rw is_unit_iff_of_associated,
+      rw associated.is_unit_iff,
       apply hx,
       use u,
       simp, },
diff --git a/src/algebra/divisibility.lean b/src/algebra/divisibility.lean
index e8b7483064814..314edd1abfcbb 100644
--- a/src/algebra/divisibility.lean
+++ b/src/algebra/divisibility.lean
@@ -64,7 +64,7 @@ match h₁, h₂ with
   ⟨d * e, show c = a * (d * e), by simp [h₃, h₄]⟩
 end
 
-alias dvd_trans ← dvd.trans
+alias dvd_trans ← has_dvd.dvd.trans
 
 theorem one_dvd (a : α) : 1 ∣ a := dvd.intro a (by simp)
 
diff --git a/src/algebra/gcd_monoid.lean b/src/algebra/gcd_monoid.lean
index d8864798d8b19..57a880e566598 100644
--- a/src/algebra/gcd_monoid.lean
+++ b/src/algebra/gcd_monoid.lean
@@ -90,16 +90,16 @@ def normalize : monoid_with_zero_hom α α :=
   classical.by_cases (λ hy : y = 0, by rw [hy, mul_zero, zero_mul, mul_zero]) $ λ hy,
   by simp only [norm_unit_mul hx hy, units.coe_mul]; simp only [mul_assoc, mul_left_comm y], }
 
-theorem associated_normalize {x : α} : associated x (normalize x) :=
+theorem associated_normalize (x : α) : associated x (normalize x) :=
 ⟨_, rfl⟩
 
-theorem normalize_associated {x : α} : associated (normalize x) x :=
-associated_normalize.symm
+theorem normalize_associated (x : α) : associated (normalize x) x :=
+(associated_normalize _).symm
 
-lemma associates.mk_normalize {x : α} : associates.mk (normalize x) = associates.mk x :=
-associates.mk_eq_mk_iff_associated.2 normalize_associated
+lemma associates.mk_normalize (x : α) : associates.mk (normalize x) = associates.mk x :=
+associates.mk_eq_mk_iff_associated.2 (normalize_associated _)
 
-@[simp] lemma normalize_apply {x : α} : normalize x = x * norm_unit x := rfl
+@[simp] lemma normalize_apply (x : α) : normalize x = x * norm_unit x := rfl
 
 @[simp] lemma normalize_zero : normalize (0 : α) = 0 := normalize.map_zero
 
@@ -108,7 +108,7 @@ associates.mk_eq_mk_iff_associated.2 normalize_associated
 lemma normalize_coe_units (u : units α) : normalize (u : α) = 1 := by simp
 
 lemma normalize_eq_zero {x : α} : normalize x = 0 ↔ x = 0 :=
-⟨λ hx, (associated_zero_iff_eq_zero x).1 $ hx ▸ associated_normalize,
+⟨λ hx, (associated_zero_iff_eq_zero x).1 $ hx ▸ associated_normalize _,
   by rintro rfl; exact normalize_zero⟩
 
 lemma normalize_eq_one {x : α} : normalize x = 1 ↔ is_unit x :=
@@ -237,7 +237,7 @@ section gcd
 
 theorem dvd_gcd_iff (a b c : α) : a ∣ gcd b c ↔ (a ∣ b ∧ a ∣ c) :=
 iff.intro
-  (assume h, ⟨dvd_trans h (gcd_dvd_left _ _), dvd_trans h (gcd_dvd_right _ _)⟩)
+  (assume h, ⟨h.trans (gcd_dvd_left _ _), h.trans (gcd_dvd_right _ _)⟩)
   (assume ⟨hab, hac⟩, dvd_gcd hab hac)
 
 theorem gcd_comm (a b : α) : gcd a b = gcd b a :=
@@ -248,12 +248,12 @@ dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
 theorem gcd_assoc (m n k : α) : gcd (gcd m n) k = gcd m (gcd n k) :=
 dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
   (dvd_gcd
-    (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n))
-    (dvd_gcd (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n))
+    ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_left m n))
+    (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_right m n))
       (gcd_dvd_right (gcd m n) k)))
   (dvd_gcd
-    (dvd_gcd (gcd_dvd_left m (gcd n k)) (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k)))
-    (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
+    (dvd_gcd (gcd_dvd_left m (gcd n k)) ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_left n k)))
+    ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))
 
 instance : is_commutative α gcd := ⟨gcd_comm⟩
 instance : is_associative α gcd := ⟨gcd_assoc⟩
@@ -281,7 +281,7 @@ dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_left _ _
 dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_right _ _) (one_dvd _)
 
 theorem gcd_dvd_gcd {a b c d: α} (hab : a ∣ b) (hcd : c ∣ d) : gcd a c ∣ gcd b d :=
-dvd_gcd (dvd.trans (gcd_dvd_left _ _) hab) (dvd.trans (gcd_dvd_right _ _) hcd)
+dvd_gcd ((gcd_dvd_left _ _).trans hab) ((gcd_dvd_right _ _).trans hcd)
 
 @[simp] theorem gcd_same (a : α) : gcd a a = normalize a :=
 gcd_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_refl a))
@@ -324,15 +324,15 @@ gcd_dvd_gcd (dvd_refl _) (dvd_mul_left _ _)
 theorem gcd_dvd_gcd_mul_right_right (m n k : α) : gcd m n ∣ gcd m (n * k) :=
 gcd_dvd_gcd (dvd_refl _) (dvd_mul_right _ _)
 
-theorem gcd_eq_of_associated_left {m n : α} (h : associated m n) (k : α) : gcd m k = gcd n k :=
+theorem associated.gcd_eq_left {m n : α} (h : associated m n) (k : α) : gcd m k = gcd n k :=
 dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
-  (gcd_dvd_gcd (dvd_of_associated h) (dvd_refl _))
-  (gcd_dvd_gcd (dvd_of_associated h.symm) (dvd_refl _))
+  (gcd_dvd_gcd h.dvd (dvd_refl _))
+  (gcd_dvd_gcd h.symm.dvd (dvd_refl _))
 
-theorem gcd_eq_of_associated_right {m n : α} (h : associated m n) (k : α) : gcd k m = gcd k n :=
+theorem associated.gcd_eq_right {m n : α} (h : associated m n) (k : α) : gcd k m = gcd k n :=
 dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
-  (gcd_dvd_gcd (dvd_refl _) (dvd_of_associated h))
-  (gcd_dvd_gcd (dvd_refl _) (dvd_of_associated h.symm))
+  (gcd_dvd_gcd (dvd_refl _) h.dvd)
+  (gcd_dvd_gcd (dvd_refl _) h.symm.dvd)
 
 lemma dvd_gcd_mul_of_dvd_mul {m n k : α} (H : k ∣ m * n) : k ∣ (gcd k m) * n :=
 begin
@@ -376,9 +376,9 @@ begin
   rw h,
   have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _,
   apply mul_dvd_mul,
-  { have hm'k : m' ∣ k := dvd_trans (dvd_mul_right m' n') hm'n',
+  { have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n',
     exact dvd_gcd hm'k hm' },
-  { have hn'k : n' ∣ k := dvd_trans (dvd_mul_left n' m') hm'n',
+  { have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n',
     exact dvd_gcd hn'k hn' }
 end
 
@@ -494,11 +494,11 @@ dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
 theorem lcm_assoc (m n k : α) : lcm (lcm m n) k = lcm m (lcm n k) :=
 dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
   (lcm_dvd
-    (lcm_dvd (dvd_lcm_left _ _) (dvd.trans (dvd_lcm_left _ _) (dvd_lcm_right _ _)))
-    (dvd.trans (dvd_lcm_right _ _) (dvd_lcm_right _ _)))
+    (lcm_dvd (dvd_lcm_left _ _) ((dvd_lcm_left _ _).trans (dvd_lcm_right _ _)))
+    ((dvd_lcm_right _ _).trans (dvd_lcm_right _ _)))
   (lcm_dvd
-    (dvd.trans (dvd_lcm_left _ _) (dvd_lcm_left _ _))
-    (lcm_dvd (dvd.trans (dvd_lcm_right _ _) (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))
+    ((dvd_lcm_left _ _).trans (dvd_lcm_left _ _))
+    (lcm_dvd ((dvd_lcm_right _ _).trans (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))
 
 instance : is_commutative α lcm := ⟨lcm_comm⟩
 instance : is_associative α lcm := ⟨lcm_assoc⟩
@@ -508,7 +508,7 @@ lemma lcm_eq_normalize {a b c : α} (habc : lcm a b ∣ c) (hcab : c ∣ lcm a b
 normalize_lcm a b ▸ normalize_eq_normalize habc hcab
 
 theorem lcm_dvd_lcm {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : lcm a c ∣ lcm b d :=
-lcm_dvd (dvd.trans hab (dvd_lcm_left _ _)) (dvd.trans hcd (dvd_lcm_right _ _))
+lcm_dvd (hab.trans (dvd_lcm_left _ _)) (hcd.trans (dvd_lcm_right _ _))
 
 @[simp] theorem lcm_units_coe_left (u : units α) (a : α) : lcm ↑u a = normalize a :=
 lcm_eq_normalize (lcm_dvd units.coe_dvd (dvd_refl _)) (dvd_lcm_right _ _)
@@ -537,7 +537,7 @@ classical.by_cases (by rintro rfl; simp only [zero_mul, lcm_zero_left, normalize
 assume ha : a ≠ 0,
 suffices lcm (a * b) (a * c) = normalize (a * lcm b c),
   by simpa only [normalize.map_mul, normalize_lcm],
-have a ∣ lcm (a * b) (a * c), from dvd.trans (dvd_mul_right _ _) (dvd_lcm_left _ _),
+have a ∣ lcm (a * b) (a * c), from (dvd_mul_right _ _).trans (dvd_lcm_left _ _),
 let ⟨d, eq⟩ := this in
 lcm_eq_normalize
   (lcm_dvd (mul_dvd_mul_left a (dvd_lcm_left _ _)) (mul_dvd_mul_left a (dvd_lcm_right _ _)))
@@ -570,13 +570,13 @@ lcm_dvd_lcm (dvd_refl _) (dvd_mul_right _ _)
 
 theorem lcm_eq_of_associated_left {m n : α} (h : associated m n) (k : α) : lcm m k = lcm n k :=
 dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
-  (lcm_dvd_lcm (dvd_of_associated h) (dvd_refl _))
-  (lcm_dvd_lcm (dvd_of_associated h.symm) (dvd_refl _))
+  (lcm_dvd_lcm h.dvd (dvd_refl _))
+  (lcm_dvd_lcm h.symm.dvd (dvd_refl _))
 
 theorem lcm_eq_of_associated_right {m n : α} (h : associated m n) (k : α) : lcm k m = lcm k n :=
 dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
-  (lcm_dvd_lcm (dvd_refl _) (dvd_of_associated h))
-  (lcm_dvd_lcm (dvd_refl _) (dvd_of_associated h.symm))
+  (lcm_dvd_lcm (dvd_refl _) h.dvd)
+  (lcm_dvd_lcm (dvd_refl _) h.symm.dvd)
 
 end lcm
 
@@ -588,14 +588,14 @@ begin
   cases hi.is_unit_or_is_unit hy with hu hu; cases hu with u hu,
   { right, transitivity (gcd (x * b) (a * b)), apply dvd_gcd (dvd_mul_right x b) h,
     rw gcd_mul_right, rw ← hu,
-    apply dvd_of_associated, transitivity (normalize b), symmetry, use u, apply mul_comm,
+    apply associated.dvd, transitivity (normalize b), symmetry, use u, apply mul_comm,
     apply normalize_associated, },
   { left, rw [hy, ← hu],
-    transitivity, {apply dvd_of_associated, symmetry, use u}, apply gcd_dvd_right, }
+    transitivity, { apply associated.dvd, symmetry, use u }, apply gcd_dvd_right, }
 end ⟩⟩
 
 theorem irreducible_iff_prime {p : α} : irreducible p ↔ prime p :=
-⟨prime_of_irreducible, irreducible_of_prime⟩
+⟨prime_of_irreducible, prime.irreducible⟩
 
 end gcd_monoid
 end gcd_monoid
@@ -696,18 +696,18 @@ noncomputable def gcd_monoid_of_gcd [decidable_eq α] (gcd : α → α → α)
   dvd_gcd := λ a b c, dvd_gcd,
   normalize_gcd := normalize_gcd,
   lcm := λ a b, if a = 0 then 0 else classical.some (dvd_normalize_iff.2
-          (dvd.trans (gcd_dvd_left a b) (dvd.intro b rfl))),
+          ((gcd_dvd_left a b).trans (dvd.intro b rfl))),
   gcd_mul_lcm := λ a b, by {
     split_ifs with a0,
     { rw [mul_zero, a0, zero_mul, normalize_zero] },
     { exact (classical.some_spec (dvd_normalize_iff.2
-                  (dvd.trans (gcd_dvd_left a b) (dvd.intro b rfl)))).symm } },
+                  ((gcd_dvd_left a b).trans (dvd.intro b rfl)))).symm } },
   lcm_zero_left := λ a, if_pos rfl,
   lcm_zero_right := λ a, by {
     split_ifs with a0, { refl },
     rw ← normalize_eq_zero at a0,
     have h := (classical.some_spec (dvd_normalize_iff.2
-                  (dvd.trans (gcd_dvd_left a 0) (dvd.intro 0 rfl)))).symm,
+                  ((gcd_dvd_left a 0).trans (dvd.intro 0 rfl)))).symm,
     have gcd0 : gcd a 0 = normalize a,
     { rw ← normalize_gcd,
       exact normalize_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_zero a)) },
@@ -751,7 +751,7 @@ let exists_gcd := λ a b, dvd_normalize_iff.2 (lcm_dvd (dvd.intro b rfl) (dvd.in
   gcd_dvd_left := λ a b, by {
     split_ifs,
     { rw h, apply dvd_zero },
-    { apply dvd_of_associated normalize_associated },
+    { exact (normalize_associated _).dvd },
     have h0 : lcm a b ≠ 0,
     { intro con,
       have h := lcm_dvd (dvd.intro b rfl) (dvd.intro_left a rfl),
@@ -762,7 +762,7 @@ let exists_gcd := λ a b, dvd_normalize_iff.2 (lcm_dvd (dvd.intro b rfl) (dvd.in
     apply dvd_lcm_right },
   gcd_dvd_right := λ a b, by {
     split_ifs,
-    { apply dvd_of_associated normalize_associated },
+    { exact (normalize_associated _).dvd },
     { rw h_1, apply dvd_zero },
     have h0 : lcm a b ≠ 0,
     { intro con,
diff --git a/src/algebra/gcd_monoid/finset.lean b/src/algebra/gcd_monoid/finset.lean
index c53ac2680cf00..43fb0af2ed3b9 100644
--- a/src/algebra/gcd_monoid/finset.lean
+++ b/src/algebra/gcd_monoid/finset.lean
@@ -182,9 +182,7 @@ begin
   { simp },
   intros b t hbt h,
   rw [gcd_insert, gcd_insert, h, ← gcd_mul_left],
-  apply gcd_eq_of_associated_right,
-  apply associated_mul_mul _ (associated.refl _),
-  apply normalize_associated,
+  apply ((normalize_associated a).mul_right _).gcd_eq_right
 end
 
 lemma gcd_mul_right {a : α} : s.gcd (λ x, f x * a) = s.gcd f * normalize a :=
@@ -194,9 +192,7 @@ begin
   { simp },
   intros b t hbt h,
   rw [gcd_insert, gcd_insert, h, ← gcd_mul_right],
-  apply gcd_eq_of_associated_right,
-  apply associated_mul_mul (associated.refl _),
-  apply normalize_associated,
+  apply ((normalize_associated a).mul_left _).gcd_eq_right
 end
 
 end gcd
@@ -219,8 +215,7 @@ begin
   rw [gcd_insert, gcd_insert, gcd_comm (f b), ← gcd_assoc, hi (λ x hx, h _ (mem_insert_of_mem hx)),
       gcd_comm a, gcd_assoc, gcd_comm a (gcd_monoid.gcd _ _),
       gcd_comm (g b), gcd_assoc _ _ a, gcd_comm _ a],
-  refine congr rfl _,
-  apply gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)),
+  exact congr_arg _ (gcd_eq_of_dvd_sub_right (h _ (mem_insert_self _ _)))
 end
 
 end integral_domain
diff --git a/src/algebra/gcd_monoid/multiset.lean b/src/algebra/gcd_monoid/multiset.lean
index d382c69c799aa..26af4c8b20bc9 100644
--- a/src/algebra/gcd_monoid/multiset.lean
+++ b/src/algebra/gcd_monoid/multiset.lean
@@ -64,7 +64,7 @@ multiset.induction_on s (by simp) $ λ a s IH, begin
   by_cases a ∈ s; simp [IH, h],
   unfold lcm,
   rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same],
-  apply lcm_eq_of_associated_left associated_normalize,
+  apply lcm_eq_of_associated_left (associated_normalize _),
 end
 
 @[simp] lemma lcm_ndunion (s₁ s₂ : multiset α) :
@@ -132,7 +132,7 @@ multiset.induction_on s (by simp) $ λ a s IH, begin
   by_cases a ∈ s; simp [IH, h],
   unfold gcd,
   rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same],
-  apply gcd_eq_of_associated_left associated_normalize,
+  apply (associated_normalize _).gcd_eq_left,
 end
 
 @[simp] lemma gcd_ndunion (s₁ s₂ : multiset α) :
diff --git a/src/algebra/group_power/basic.lean b/src/algebra/group_power/basic.lean
index 8151f5c4f8c4e..ebb42154f9ce2 100644
--- a/src/algebra/group_power/basic.lean
+++ b/src/algebra/group_power/basic.lean
@@ -450,8 +450,8 @@ variables [semiring R]
 lemma min_pow_dvd_add {n m : ℕ} {a b c : R} (ha : c ^ n ∣ a) (hb : c ^ m ∣ b) :
   c ^ (min n m) ∣ a + b :=
 begin
-  replace ha := dvd.trans (pow_dvd_pow c (min_le_left n m)) ha,
-  replace hb := dvd.trans (pow_dvd_pow c (min_le_right n m)) hb,
+  replace ha := (pow_dvd_pow c (min_le_left n m)).trans ha,
+  replace hb := (pow_dvd_pow c (min_le_right n m)).trans hb,
   exact dvd_add ha hb
 end
 
diff --git a/src/algebra/squarefree.lean b/src/algebra/squarefree.lean
index 651f91c425987..5492acb29e8a2 100644
--- a/src/algebra/squarefree.lean
+++ b/src/algebra/squarefree.lean
@@ -63,12 +63,12 @@ end
 @[simp]
 lemma prime.squarefree [comm_cancel_monoid_with_zero R] {x : R} (h : prime x) :
   squarefree x :=
-(irreducible_of_prime h).squarefree
+h.irreducible.squarefree
 
 lemma squarefree_of_dvd_of_squarefree [comm_monoid R]
   {x y : R} (hdvd : x ∣ y) (hsq : squarefree y) :
   squarefree x :=
-λ a h, hsq _ (dvd.trans h hdvd)
+λ a h, hsq _ (h.trans hdvd)
 
 namespace multiplicity
 variables [comm_monoid R] [decidable_rel (has_dvd.dvd : R → R → Prop)]
@@ -173,7 +173,7 @@ begin
         intro con,
         apply not_irreducible_zero (irreducible_of_factor 0
             (multiset.mem_erase_dup.1 (multiset.mem_of_le hs con))) },
-      rw [dvd_iff_dvd_of_rel_right (factors_prod h0).symm],
+      rw (factors_prod h0).symm.dvd_iff_dvd_right,
       refine ⟨⟨multiset.prod_dvd_prod (le_trans hs (multiset.erase_dup_le _)), h0⟩, _⟩,
       have h := unique_factorization_monoid.factors_unique irreducible_of_factor
         (λ x hx, irreducible_of_factor x (multiset.mem_of_le
diff --git a/src/data/int/gcd.lean b/src/data/int/gcd.lean
index dd3d280fb4565..36524cc424548 100644
--- a/src/data/int/gcd.lean
+++ b/src/data/int/gcd.lean
@@ -256,10 +256,10 @@ begin
 end
 
 theorem gcd_dvd_gcd_of_dvd_left {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd i j ∣ gcd k j :=
-int.coe_nat_dvd.1 $ dvd_gcd (dvd.trans (gcd_dvd_left i j) H) (gcd_dvd_right i j)
+int.coe_nat_dvd.1 $ dvd_gcd ((gcd_dvd_left i j).trans H) (gcd_dvd_right i j)
 
 theorem gcd_dvd_gcd_of_dvd_right {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd j i ∣ gcd j k :=
-int.coe_nat_dvd.1 $ dvd_gcd (gcd_dvd_left j i) (dvd.trans (gcd_dvd_right j i) H)
+int.coe_nat_dvd.1 $ dvd_gcd (gcd_dvd_left j i) ((gcd_dvd_right j i).trans H)
 
 theorem gcd_dvd_gcd_mul_left (i j k : ℤ) : gcd i j ∣ gcd (k * i) j :=
 gcd_dvd_gcd_of_dvd_left _ (dvd_mul_left _ _)
diff --git a/src/data/int/modeq.lean b/src/data/int/modeq.lean
index 030285457d93c..332fb68aa262a 100644
--- a/src/data/int/modeq.lean
+++ b/src/data/int/modeq.lean
@@ -131,7 +131,7 @@ begin
 end
 
 theorem of_modeq_mul_left (m : ℤ) (h : a ≡ b [ZMOD m * n]) : a ≡ b [ZMOD n] :=
-by rw [modeq_iff_dvd] at *; exact dvd.trans (dvd_mul_left n m) h
+by rw [modeq_iff_dvd] at *; exact (dvd_mul_left n m).trans h
 
 theorem of_modeq_mul_right (m : ℤ) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n] :=
 mul_comm m n ▸ of_modeq_mul_left _
diff --git a/src/data/nat/gcd.lean b/src/data/nat/gcd.lean
index dfbfdf7caaa37..034720732aba5 100644
--- a/src/data/nat/gcd.lean
+++ b/src/data/nat/gcd.lean
@@ -32,7 +32,7 @@ gcd.induction m n (λn _ kn, by rw gcd_zero_left; exact kn)
   (λn m mpos IH H1 H2, by rw gcd_rec; exact IH ((dvd_mod_iff H1).2 H2) H1)
 
 theorem dvd_gcd_iff {m n k : ℕ} : k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n :=
-iff.intro (λ h, ⟨dvd_trans h (gcd_dvd m n).left, dvd_trans h (gcd_dvd m n).right⟩)
+iff.intro (λ h, ⟨h.trans (gcd_dvd m n).left, h.trans (gcd_dvd m n).right⟩)
           (λ h, dvd_gcd h.left h.right)
 
 theorem gcd_comm (m n : ℕ) : gcd m n = gcd n m :=
@@ -50,12 +50,12 @@ by rw gcd_comm; apply gcd_eq_left_iff_dvd
 theorem gcd_assoc (m n k : ℕ) : gcd (gcd m n) k = gcd m (gcd n k) :=
 dvd_antisymm
   (dvd_gcd
-    (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n))
-    (dvd_gcd (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n))
+    ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_left m n))
+    (dvd_gcd ((gcd_dvd_left (gcd m n) k).trans (gcd_dvd_right m n))
       (gcd_dvd_right (gcd m n) k)))
   (dvd_gcd
-    (dvd_gcd (gcd_dvd_left m (gcd n k)) (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k)))
-    (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
+    (dvd_gcd (gcd_dvd_left m (gcd n k)) ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_left n k)))
+    ((gcd_dvd_right m (gcd n k)).trans (gcd_dvd_right n k)))
 
 @[simp] theorem gcd_one_right (n : ℕ) : gcd n 1 = 1 :=
 eq.trans (gcd_comm n 1) $ gcd_one_left n
@@ -90,10 +90,10 @@ or.elim (nat.eq_zero_or_pos k)
     nat.div_mul_cancel H1, nat.div_mul_cancel H2])
 
 theorem gcd_dvd_gcd_of_dvd_left {m k : ℕ} (n : ℕ) (H : m ∣ k) : gcd m n ∣ gcd k n :=
-dvd_gcd (dvd.trans (gcd_dvd_left m n) H) (gcd_dvd_right m n)
+dvd_gcd ((gcd_dvd_left m n).trans H) (gcd_dvd_right m n)
 
 theorem gcd_dvd_gcd_of_dvd_right {m k : ℕ} (n : ℕ) (H : m ∣ k) : gcd n m ∣ gcd n k :=
-dvd_gcd (gcd_dvd_left n m) (dvd.trans (gcd_dvd_right n m) H)
+dvd_gcd (gcd_dvd_left n m) ((gcd_dvd_right n m).trans H)
 
 theorem gcd_dvd_gcd_mul_left (m n k : ℕ) : gcd m n ∣ gcd (k * m) n :=
 gcd_dvd_gcd_of_dvd_left _ (dvd_mul_left _ _)
@@ -182,7 +182,7 @@ theorem dvd_lcm_right (m n : ℕ) : n ∣ lcm m n :=
 lcm_comm n m ▸ dvd_lcm_left n m
 
 theorem gcd_mul_lcm (m n : ℕ) : gcd m n * lcm m n = m * n :=
-by delta lcm; rw [nat.mul_div_cancel' (dvd.trans (gcd_dvd_left m n) (dvd_mul_right m n))]
+by delta lcm; rw [nat.mul_div_cancel' ((gcd_dvd_left m n).trans (dvd_mul_right m n))]
 
 theorem lcm_dvd {m n k : ℕ} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k :=
 or.elim (nat.eq_zero_or_pos k)
@@ -192,17 +192,17 @@ or.elim (nat.eq_zero_or_pos k)
        exact dvd_gcd (mul_dvd_mul_left _ H2) (mul_dvd_mul_right H1 _))
 
 lemma lcm_dvd_iff {m n k : ℕ} : lcm m n ∣ k ↔ m ∣ k ∧ n ∣ k :=
-⟨λ h, ⟨dvd_trans (dvd_lcm_left _ _) h, dvd_trans (dvd_lcm_right _ _) h⟩,
+⟨λ h, ⟨(dvd_lcm_left _ _).trans h, (dvd_lcm_right _ _).trans h⟩,
   and_imp.2 lcm_dvd⟩
 
 theorem lcm_assoc (m n k : ℕ) : lcm (lcm m n) k = lcm m (lcm n k) :=
 dvd_antisymm
   (lcm_dvd
-    (lcm_dvd (dvd_lcm_left m (lcm n k)) (dvd.trans (dvd_lcm_left n k) (dvd_lcm_right m (lcm n k))))
-    (dvd.trans (dvd_lcm_right n k) (dvd_lcm_right m (lcm n k))))
+    (lcm_dvd (dvd_lcm_left m (lcm n k)) ((dvd_lcm_left n k).trans (dvd_lcm_right m (lcm n k))))
+    ((dvd_lcm_right n k).trans (dvd_lcm_right m (lcm n k))))
   (lcm_dvd
-    (dvd.trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
-    (lcm_dvd (dvd.trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k))
+    ((dvd_lcm_left m n).trans (dvd_lcm_left (lcm m n) k))
+    (lcm_dvd ((dvd_lcm_right m n).trans (dvd_lcm_left (lcm m n) k))
       (dvd_lcm_right (lcm m n) k)))
 
 theorem lcm_ne_zero {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0 :=
@@ -405,9 +405,9 @@ replace h : gcd k (m * n) = m' * n' := h,
 rw h,
 have hm'n' : m' * n' ∣ k := h ▸ gcd_dvd_left _ _,
 apply mul_dvd_mul,
-  { have hm'k : m' ∣ k := dvd_trans (dvd_mul_right m' n') hm'n',
+  { have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n',
     exact dvd_gcd hm'k hm' },
-  { have hn'k : n' ∣ k := dvd_trans (dvd_mul_left n' m') hm'n',
+  { have hn'k : n' ∣ k := (dvd_mul_left n' m').trans hm'n',
     exact dvd_gcd hn'k hn' }
 end
 
diff --git a/src/data/nat/modeq.lean b/src/data/nat/modeq.lean
index 575eca3e334d8..3aba336e62664 100644
--- a/src/data/nat/modeq.lean
+++ b/src/data/nat/modeq.lean
@@ -69,7 +69,7 @@ theorem mod_modeq (a n) : a % n ≡ a [MOD n] := mod_mod _ _
 namespace modeq
 
 protected theorem modeq_of_dvd (d : m ∣ n) (h : a ≡ b [MOD n]) : a ≡ b [MOD m] :=
-modeq_of_dvd (dvd_trans (int.coe_nat_dvd.2 d) h.dvd)
+modeq_of_dvd ((int.coe_nat_dvd.2 d).trans h.dvd)
 
 protected theorem mul_left' (c : ℕ) (h : a ≡ b [MOD n]) : c * a ≡ c * b [MOD (c * n)] :=
 by unfold modeq at *; rw [mul_mod_mul_left, mul_mod_mul_left, h]
@@ -125,7 +125,7 @@ protected theorem add_right_cancel' (c : ℕ) (h : a + c ≡ b + c [MOD n]) : a
 modeq.rfl.add_right_cancel h
 
 theorem of_modeq_mul_left (m : ℕ) (h : a ≡ b [MOD m * n]) : a ≡ b [MOD n] :=
-by { rw [modeq_iff_dvd] at *, exact dvd.trans (dvd_mul_left (n : ℤ) (m : ℤ)) h }
+by { rw [modeq_iff_dvd] at *, exact (dvd_mul_left (n : ℤ) (m : ℤ)).trans h }
 
 theorem of_modeq_mul_right (m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n] :=
 mul_comm m n ▸ of_modeq_mul_left _
diff --git a/src/data/nat/prime.lean b/src/data/nat/prime.lean
index 8e37cd14516ab..56c18ca58223c 100644
--- a/src/data/nat/prime.lean
+++ b/src/data/nat/prime.lean
@@ -212,7 +212,7 @@ if n1 : n = 1 then by simp [n1] else (min_fac_has_prop n1).2.1
 
 theorem min_fac_prime {n : ℕ} (n1 : n ≠ 1) : prime (min_fac n) :=
 let ⟨f2, fd, a⟩ := min_fac_has_prop n1 in
-prime_def_lt'.2 ⟨f2, λ m m2 l d, not_le_of_gt l (a m m2 (dvd_trans d fd))⟩
+prime_def_lt'.2 ⟨f2, λ m m2 l d, not_le_of_gt l (a m m2 (d.trans fd))⟩
 
 theorem min_fac_le_of_dvd {n : ℕ} : ∀ {m : ℕ}, 2 ≤ m → m ∣ n → min_fac n ≤ m :=
 by by_cases n1 : n = 1;
@@ -428,7 +428,7 @@ lemma factors_chain : ∀ {n a}, (∀ p, prime p → p ∣ n → a ≤ p) → li
   begin
     rw factors,
     refine list.chain.cons ((le_min_fac.2 h).resolve_left dec_trivial) (factors_chain _),
-    exact λ p pp d, min_fac_le_of_dvd pp.two_le (dvd_trans d $ div_dvd_of_dvd $ min_fac_dvd _),
+    exact λ p pp d, min_fac_le_of_dvd pp.two_le (d.trans $ div_dvd_of_dvd $ min_fac_dvd _),
   end
 
 lemma factors_chain_2 (n) : list.chain (≤) 2 (factors n) := factors_chain $ λ p pp _, pp.two_le
@@ -470,8 +470,8 @@ begin
   apply iff.intro,
   { intro h,
     exact ⟨min_fac (gcd m n), min_fac_prime h,
-      (dvd.trans (min_fac_dvd (gcd m n)) (gcd_dvd_left m n)),
-      (dvd.trans (min_fac_dvd (gcd m n)) (gcd_dvd_right m n))⟩ },
+      ((min_fac_dvd (gcd m n)).trans (gcd_dvd_left m n)),
+      ((min_fac_dvd (gcd m n)).trans (gcd_dvd_right m n))⟩ },
   { intro h,
     cases h with p hp,
     apply nat.not_coprime_of_dvd_of_dvd (prime.one_lt hp.1) hp.2.1 hp.2.2 }
@@ -497,7 +497,7 @@ begin
   induction n with n ih,
   { simp },
   { rw [pow_succ'] at *,
-    rcases ih (dvd_trans (dvd_mul_right _ _) h) with ⟨c, rfl⟩,
+    rcases ih ((dvd_mul_right _ _).trans h) with ⟨c, rfl⟩,
     rw [mul_assoc] at h,
     rcases hp.dvd_mul.1 (nat.dvd_of_mul_dvd_mul_left (pow_pos hp.pos _) h)
       with ⟨d, rfl⟩|⟨d, rfl⟩,
diff --git a/src/data/polynomial/cancel_leads.lean b/src/data/polynomial/cancel_leads.lean
index f29ae6c3493e3..fa7b7dc77cc73 100644
--- a/src/data/polynomial/cancel_leads.lean
+++ b/src/data/polynomial/cancel_leads.lean
@@ -37,7 +37,7 @@ variables {p q}
 
 lemma dvd_cancel_leads_of_dvd_of_dvd {r : polynomial R} (pq : p ∣ q) (pr : p ∣ r) :
   p ∣ q.cancel_leads r :=
-dvd_sub (dvd.trans pr (dvd.intro_left _ rfl)) (dvd.trans pq (dvd.intro_left _ rfl))
+dvd_sub (pr.trans (dvd.intro_left _ rfl)) (pq.trans (dvd.intro_left _ rfl))
 
 end comm_ring
 
diff --git a/src/data/polynomial/field_division.lean b/src/data/polynomial/field_division.lean
index b1f6ee4e8d624..15502edd1f7db 100644
--- a/src/data/polynomial/field_division.lean
+++ b/src/data/polynomial/field_division.lean
@@ -344,12 +344,12 @@ lemma degree_normalize : degree (normalize p) = degree p := by simp
 
 lemma prime_of_degree_eq_one (hp1 : degree p = 1) : prime p :=
 have prime (normalize p),
-  from prime_of_degree_eq_one_of_monic (hp1 ▸ degree_normalize)
+  from monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
     (monic_normalize (λ hp0, absurd hp1 (hp0.symm ▸ by simp; exact dec_trivial))),
-prime_of_associated normalize_associated this
+(normalize_associated _).prime this
 
 lemma irreducible_of_degree_eq_one (hp1 : degree p = 1) : irreducible p :=
-irreducible_of_prime (prime_of_degree_eq_one hp1)
+(prime_of_degree_eq_one hp1).irreducible
 
 theorem not_irreducible_C (x : R) : ¬irreducible (C x) :=
 if H : x = 0 then by { rw [H, C_0], exact not_irreducible_zero }
diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
index d342ccda758f1..f5c1fb1dec489 100644
--- a/src/data/polynomial/ring_division.lean
+++ b/src/data/polynomial/ring_division.lean
@@ -128,28 +128,28 @@ by rw [nat_degree_one, nat_degree_mul hp0 hq0, eq_comm,
   degree (u : polynomial R) = 0 :=
 degree_eq_zero_of_is_unit ⟨u, rfl⟩
 
-theorem prime_X_sub_C {r : R} : prime (X - C r) :=
+theorem prime_X_sub_C (r : R) : prime (X - C r) :=
 ⟨X_sub_C_ne_zero r, not_is_unit_X_sub_C,
  λ _ _, by { simp_rw [dvd_iff_is_root, is_root.def, eval_mul, mul_eq_zero], exact id }⟩
 
 theorem prime_X : prime (X : polynomial R) :=
-by { convert (prime_X_sub_C : prime (X - C 0 : polynomial R)), simp }
+by { convert (prime_X_sub_C (0 : R)), simp }
 
-lemma prime_of_degree_eq_one_of_monic (hp1 : degree p = 1)
-  (hm : monic p) : prime p :=
+lemma monic.prime_of_degree_eq_one (hp1 : degree p = 1) (hm : monic p) :
+  prime p :=
 have p = X - C (- p.coeff 0),
   by simpa [hm.leading_coeff] using eq_X_add_C_of_degree_eq_one hp1,
-this.symm ▸ prime_X_sub_C
+this.symm ▸ prime_X_sub_C _
 
 theorem irreducible_X_sub_C (r : R) : irreducible (X - C r) :=
-irreducible_of_prime prime_X_sub_C
+(prime_X_sub_C r).irreducible
 
 theorem irreducible_X : irreducible (X : polynomial R) :=
-irreducible_of_prime prime_X
+prime.irreducible prime_X
 
-lemma irreducible_of_degree_eq_one_of_monic (hp1 : degree p = 1)
-  (hm : monic p) : irreducible p :=
-irreducible_of_prime (prime_of_degree_eq_one_of_monic hp1 hm)
+lemma monic.irreducible_of_degree_eq_one (hp1 : degree p = 1) (hm : monic p) :
+  irreducible p :=
+(hm.prime_of_degree_eq_one hp1).irreducible
 
 theorem eq_of_monic_of_associated (hp : p.monic) (hq : q.monic) (hpq : associated p q) : p = q :=
 begin
@@ -188,7 +188,7 @@ begin
   rw [root_multiplicity_eq_multiplicity (p * q), dif_neg hpq,
       root_multiplicity_eq_multiplicity p, dif_neg hp,
       root_multiplicity_eq_multiplicity q, dif_neg hq,
-      @multiplicity.mul' _ _ _ (X - C x) _ _ prime_X_sub_C],
+      multiplicity.mul' (prime_X_sub_C x)],
 end
 
 lemma root_multiplicity_X_sub_C_self {x : R} :
diff --git a/src/field_theory/algebraic_closure.lean b/src/field_theory/algebraic_closure.lean
index bc3fbc83d0597..5452aea47acb5 100644
--- a/src/field_theory/algebraic_closure.lean
+++ b/src/field_theory/algebraic_closure.lean
@@ -74,7 +74,7 @@ theorem of_exists_root (H : ∀ p : polynomial k, p.monic → irreducible p →
 ⟨λ p, or.inr $ λ q hq hqp,
  have irreducible (q * C (leading_coeff q)⁻¹),
    by { rw ← coe_norm_unit_of_ne_zero hq.ne_zero,
-        exact irreducible_of_associated associated_normalize hq },
+        exact (associated_normalize _).irreducible hq },
  let ⟨x, hx⟩ := H (q * C (leading_coeff q)⁻¹) (monic_mul_leading_coeff_inv hq.ne_zero) this in
  degree_mul_leading_coeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx⟩
 
diff --git a/src/field_theory/minpoly.lean b/src/field_theory/minpoly.lean
index e3dac9b2afe7f..e265e42bd9cf0 100644
--- a/src/field_theory/minpoly.lean
+++ b/src/field_theory/minpoly.lean
@@ -290,7 +290,7 @@ theorem unique' [nontrivial B] {p : polynomial A} (hp1 : _root_.irreducible p)
   (hp2 : polynomial.aeval x p = 0) (hp3 : p.monic) : p = minpoly A x :=
 let ⟨q, hq⟩ := dvd A x hp2 in
 eq_of_monic_of_associated hp3 (monic ⟨p, ⟨hp3, hp2⟩⟩) $
-mul_one (minpoly A x) ▸ hq.symm ▸ associated_mul_mul (associated.refl _) $
+mul_one (minpoly A x) ▸ hq.symm ▸ associated.mul_left _ $
 associated_one_iff_is_unit.2 $ (hp1.is_unit_or_is_unit hq).resolve_left $ not_is_unit A x
 
 lemma unique'' [nontrivial B] {p : polynomial A}
@@ -299,7 +299,7 @@ lemma unique'' [nontrivial B] {p : polynomial A}
 begin
   have : p.leading_coeff ≠ 0 := leading_coeff_ne_zero.mpr hp1.ne_zero,
   apply unique',
-  { exact irreducible_of_associated ⟨⟨C p.leading_coeff⁻¹, C p.leading_coeff,
+  { exact associated.irreducible ⟨⟨C p.leading_coeff⁻¹, C p.leading_coeff,
       by rwa [←C_mul, inv_mul_cancel, C_1], by rwa [←C_mul, mul_inv_cancel, C_1]⟩, rfl⟩ hp1 },
   { rw [aeval_mul, hp2, zero_mul] },
   { rwa [polynomial.monic, leading_coeff_mul, leading_coeff_C, mul_inv_cancel] },
@@ -399,7 +399,7 @@ lemma root {x : B} (hx : is_integral A x) {y : A} (h : is_root (minpoly A x) y)
   algebra_map A B y = x :=
 have key : minpoly A x = X - C y :=
 eq_of_monic_of_associated (monic hx) (monic_X_sub_C y) (associated_of_dvd_dvd
-  (dvd_symm_of_irreducible (irreducible_X_sub_C y) (irreducible hx) (dvd_iff_is_root.2 h))
+  ((irreducible_X_sub_C y).dvd_symm (irreducible hx) (dvd_iff_is_root.2 h))
   (dvd_iff_is_root.2 h)),
 by { have := aeval A x, rwa [key, alg_hom.map_sub, aeval_X, aeval_C, sub_eq_zero, eq_comm] at this }
 
diff --git a/src/field_theory/polynomial_galois_group.lean b/src/field_theory/polynomial_galois_group.lean
index 901f16d281fd5..e1e4775ecccbb 100644
--- a/src/field_theory/polynomial_galois_group.lean
+++ b/src/field_theory/polynomial_galois_group.lean
@@ -279,7 +279,7 @@ begin
     exact splits_of_splits_of_dvd _
       (minpoly.ne_zero qx_int)
       (normal.splits h_normal _)
-      (dvd_symm_of_irreducible (minpoly.irreducible qx_int) hr (minpoly.dvd F _ hx)) },
+      ((minpoly.irreducible qx_int).dvd_symm hr (minpoly.dvd F _ hx)) },
   have key2 : ∀ {p₁ p₂ : polynomial F}, P p₁ → P p₂ → P (p₁ * p₂),
   { intros p₁ p₂ hp₁ hp₂,
     by_cases h₁ : p₁.comp q = 0,
@@ -332,7 +332,7 @@ begin
   { rw [←finite_dimensional.finrank_mul_finrank F F⟮α⟯ p.splitting_field,
         intermediate_field.adjoin.finrank hα, this] },
   suffices : minpoly F α ∣ p,
-  { have key := dvd_symm_of_irreducible (minpoly.irreducible hα) p_irr this,
+  { have key := (minpoly.irreducible hα).dvd_symm p_irr this,
     apply le_antisymm,
     { exact nat_degree_le_of_dvd this p_irr.ne_zero },
     { exact nat_degree_le_of_dvd key (minpoly.ne_zero hα) } },
diff --git a/src/field_theory/splitting_field.lean b/src/field_theory/splitting_field.lean
index b50aad9a27cad..ea41b0339a788 100644
--- a/src/field_theory/splitting_field.lean
+++ b/src/field_theory/splitting_field.lean
@@ -112,9 +112,9 @@ else or.inr $ λ p hp hpf, ((principal_ideal_ring.irreducible_iff_prime.1 hp).2.
 lemma splits_of_splits_mul {f g : polynomial K} (hfg : f * g ≠ 0) (h : splits i (f * g)) :
   splits i f ∧ splits i g :=
 ⟨or.inr $ λ g hgi hg, or.resolve_left h hfg hgi
-   (by rw map_mul; exact dvd.trans hg (dvd_mul_right _ _)),
+   (by rw map_mul; exact hg.trans (dvd_mul_right _ _)),
  or.inr $ λ g hgi hg, or.resolve_left h hfg hgi
-   (by rw map_mul; exact dvd.trans hg (dvd_mul_left _ _))⟩
+   (by rw map_mul; exact hg.trans (dvd_mul_left _ _))⟩
 
 lemma splits_of_splits_of_dvd {f g : polynomial K} (hf0 : f ≠ 0) (hf : splits i f) (hgf : g ∣ f) :
   splits i g :=
@@ -355,7 +355,7 @@ unique_factorization_monoid.induction_on_prime f (λ _, splits_zero _)
   (λ a p ha0 hp ih hfi, splits_mul _
     (splits_of_degree_eq_one _
       ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.resolve_left
-        hp.1 (irreducible_of_prime hp) (by rw map_id)))
+        hp.1 hp.irreducible (by rw map_id)))
     (ih (splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).2))
 
 end UFD
diff --git a/src/group_theory/specific_groups/cyclic.lean b/src/group_theory/specific_groups/cyclic.lean
index e6ebb69991724..58f20ec317542 100644
--- a/src/group_theory/specific_groups/cyclic.lean
+++ b/src/group_theory/specific_groups/cyclic.lean
@@ -268,7 +268,7 @@ have h : ∑ m in (range d.succ).filter (∣ d.succ),
   finset.sum_congr rfl
     (λ m hm, have hmd : m < d.succ, from mem_range.1 (mem_filter.1 hm).1,
       have hm : m ∣ d.succ, from (mem_filter.1 hm).2,
-      card_order_of_eq_totient_aux₁ (dvd.trans hm hd) (finset.card_pos.2
+      card_order_of_eq_totient_aux₁ (hm.trans hd) (finset.card_pos.2
         ⟨a ^ (d.succ / m), mem_filter.2 ⟨mem_univ _,
           by { rw [order_of_pow a, ha, gcd_eq_right (div_dvd_of_dvd hm),
                 nat.div_div_self hm (succ_pos _)]
diff --git a/src/number_theory/divisors.lean b/src/number_theory/divisors.lean
index 28d237a53e5b1..9344cfca703b3 100644
--- a/src/number_theory/divisors.lean
+++ b/src/number_theory/divisors.lean
@@ -127,14 +127,14 @@ begin
 end
 
 lemma divisors_subset_of_dvd {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) : divisors m ⊆ divisors n :=
-finset.subset_iff.2 $ λ x hx, nat.mem_divisors.mpr (⟨dvd.trans (nat.mem_divisors.mp hx).1 h, hzero⟩)
+finset.subset_iff.2 $ λ x hx, nat.mem_divisors.mpr (⟨(nat.mem_divisors.mp hx).1.trans h, hzero⟩)
 
 lemma divisors_subset_proper_divisors {m : ℕ} (hzero : n ≠ 0) (h : m ∣ n) (hdiff : m ≠ n) :
   divisors m ⊆ proper_divisors n :=
 begin
   apply finset.subset_iff.2,
   intros x hx,
-  exact nat.mem_proper_divisors.2 (⟨dvd.trans (nat.mem_divisors.1 hx).1 h,
+  exact nat.mem_proper_divisors.2 (⟨(nat.mem_divisors.1 hx).1.trans h,
     lt_of_le_of_lt (divisor_le hx) (lt_of_le_of_ne (divisor_le (nat.mem_divisors.2
     ⟨h, hzero⟩)) hdiff)⟩)
 end
diff --git a/src/number_theory/padics/padic_integers.lean b/src/number_theory/padics/padic_integers.lean
index fa56f60427f14..e7ab51a636a2b 100644
--- a/src/number_theory/padics/padic_integers.lean
+++ b/src/number_theory/padics/padic_integers.lean
@@ -568,7 +568,7 @@ begin
 end
 
 lemma irreducible_p : irreducible (p : ℤ_[p]) :=
-irreducible_of_prime prime_p
+prime.irreducible prime_p
 
 instance : discrete_valuation_ring ℤ_[p] :=
 discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization
diff --git a/src/ring_theory/dedekind_domain.lean b/src/ring_theory/dedekind_domain.lean
index ec054bd9db396..ef77b8f3315f9 100644
--- a/src/ring_theory/dedekind_domain.lean
+++ b/src/ring_theory/dedekind_domain.lean
@@ -660,7 +660,7 @@ instance ideal.unique_factorization_monoid :
       exact ⟨x * y, ideal.mul_mem_mul x_mem y_mem,
              mt this.is_prime.mem_or_mem (not_or x_not_mem y_not_mem)⟩,
     end⟩,
-     λ h, irreducible_of_prime h⟩,
+    prime.irreducible⟩,
   .. ideal.wf_dvd_monoid }
 
 noncomputable instance ideal.normalization_monoid : normalization_monoid (ideal A) :=
diff --git a/src/ring_theory/discrete_valuation_ring.lean b/src/ring_theory/discrete_valuation_ring.lean
index 7e44203f3d96f..07ad6a74f82b3 100644
--- a/src/ring_theory/discrete_valuation_ring.lean
+++ b/src/ring_theory/discrete_valuation_ring.lean
@@ -120,7 +120,7 @@ begin
         apply hQ1,
         simp },
       erw span_singleton_prime hq at hQ2,
-      replace hQ2 := irreducible_of_prime hQ2,
+      replace hQ2 := hQ2.irreducible,
       rw irreducible_iff_uniformizer at hQ2,
       exact hQ2.symm } },
   { rintro ⟨RPID, Punique⟩,
@@ -162,7 +162,7 @@ begin
   clear hp hq p q,
   intros p hp,
   obtain ⟨n, hn⟩ := hR hp.ne_zero,
-  have : irreducible (ϖ ^ n) := irreducible_of_associated hn.symm hp,
+  have : irreducible (ϖ ^ n) := hn.symm.irreducible hp,
   rcases lt_trichotomy n 1 with (H|rfl|H),
   { obtain rfl : n = 0, { clear hn this, revert H n, exact dec_trivial },
     simpa only [not_irreducible_one, pow_zero] using this, },
@@ -398,7 +398,7 @@ lemma add_val_def (r : R) (u : units R) {ϖ : R} (hϖ : irreducible ϖ) (n : ℕ
   add_val R r = n :=
 by rw [add_val, add_valuation_apply, hr,
     eq_of_associated_left (associated_of_irreducible R hϖ
-      (irreducible_of_prime (classical.some_spec (exists_prime R)))),
+      (classical.some_spec (exists_prime R)).irreducible),
     eq_of_associated_right (associated.symm ⟨u, mul_comm _ _⟩),
     multiplicity_pow_self_of_prime (principal_ideal_ring.irreducible_iff_prime.1 hϖ)]
 
@@ -424,7 +424,7 @@ lemma add_val_pow (a : R) (n : ℕ) : add_val R (a ^ n) = n • add_val R a :=
 
 lemma add_val_eq_top_iff {a : R} : add_val R a = ⊤ ↔ a = 0 :=
 begin
-  have hi := (irreducible_of_prime (classical.some_spec (exists_prime R))),
+  have hi := (classical.some_spec (exists_prime R)).irreducible,
   split,
   { contrapose,
     intro h,
@@ -444,10 +444,10 @@ begin
     { rw [ha0, add_val_zero, top_le_iff, add_val_eq_top_iff] at h,
       rw h,
       apply dvd_zero },
-    obtain ⟨n, ha⟩ := associated_pow_irreducible ha0 (irreducible_of_prime hp),
+    obtain ⟨n, ha⟩ := associated_pow_irreducible ha0 hp.irreducible,
     rw [add_val, add_valuation_apply, add_valuation_apply,
       multiplicity_le_multiplicity_iff] at h,
-    exact dvd.trans (dvd_of_associated ha) (h n (dvd_of_associated ha.symm)), },
+    exact ha.dvd.trans (h n ha.symm.dvd), },
   { rw [add_val, add_valuation_apply, add_valuation_apply],
     exact multiplicity_le_multiplicity_of_dvd_right h }
 end
diff --git a/src/ring_theory/eisenstein_criterion.lean b/src/ring_theory/eisenstein_criterion.lean
index 6b0ea20da2a46..34e58c28cff9f 100644
--- a/src/ring_theory/eisenstein_criterion.lean
+++ b/src/ring_theory/eisenstein_criterion.lean
@@ -82,7 +82,7 @@ begin
   rintros p q rfl,
   rw [map_mul] at hf,
   rcases mul_eq_mul_prime_pow (show prime (X : polynomial (ideal.quotient P)),
-    from prime_of_degree_eq_one_of_monic degree_X monic_X) hf with
+    from monic_X.prime_of_degree_eq_one degree_X) hf with
       ⟨m, n, b, c, hmnd, hbc, hp, hq⟩,
   have hmn : 0 < m → 0 < n → false,
   { assume hm0 hn0,
diff --git a/src/ring_theory/euclidean_domain.lean b/src/ring_theory/euclidean_domain.lean
index 83e3caea25d8a..918ac5d5cf82a 100644
--- a/src/ring_theory/euclidean_domain.lean
+++ b/src/ring_theory/euclidean_domain.lean
@@ -66,7 +66,7 @@ begin
   apply is_coprime_of_dvd,
   { unfreezingI { rintro ⟨rfl, rfl⟩ }, simpa using h },
   { unfreezingI { rintro z nu nz ⟨w, rfl⟩ dy },
-    refine h' (dvd.trans _ dy),
+    refine h' (dvd_trans _ dy),
     simpa using mul_dvd_mul_left z (is_unit_iff_dvd_one.1 $
       (of_irreducible_mul h).resolve_left nu) }
 end
diff --git a/src/ring_theory/int/basic.lean b/src/ring_theory/int/basic.lean
index a44b7880a02f3..8f01d07563fec 100644
--- a/src/ring_theory/int/basic.lean
+++ b/src/ring_theory/int/basic.lean
@@ -51,7 +51,7 @@ end
 
 theorem nat.irreducible_iff_prime {p : ℕ} : irreducible p ↔ prime p :=
 begin
-  refine ⟨λ h, _, irreducible_of_prime⟩,
+  refine ⟨λ h, _, prime.irreducible⟩,
   rw ← nat.prime_iff,
   refine ⟨_, λ m hm, _⟩,
   { cases p, { exfalso, apply h.ne_zero rfl },
@@ -352,10 +352,7 @@ lemma int.associated_nat_abs (k : ℤ) : associated k k.nat_abs :=
 associated_of_dvd_dvd (int.coe_nat_dvd_right.mpr (dvd_refl _)) (int.nat_abs_dvd.mpr (dvd_refl _))
 
 lemma int.prime_iff_nat_abs_prime {k : ℤ} : prime k ↔ nat.prime k.nat_abs :=
-begin
-  rw nat.prime_iff_prime_int,
-  rw prime_iff_of_associated (int.associated_nat_abs k),
-end
+(int.associated_nat_abs k).prime_iff.trans nat.prime_iff_prime_int.symm
 
 theorem int.associated_iff_nat_abs {a b : ℤ} : associated a b ↔ a.nat_abs = b.nat_abs :=
 begin
diff --git a/src/ring_theory/multiplicity.lean b/src/ring_theory/multiplicity.lean
index 4c38873344c4f..b9c2fdcef8eb8 100644
--- a/src/ring_theory/multiplicity.lean
+++ b/src/ring_theory/multiplicity.lean
@@ -65,7 +65,7 @@ let ⟨n, hn⟩ := h in mt (is_unit_iff_forall_dvd.1 ∘ is_unit.pow (n + 1)) $
 λ h, hn (h b)
 
 lemma finite_of_finite_mul_left {a b c : α} : finite a (b * c) → finite a c :=
-λ ⟨n, hn⟩, ⟨n, λ h, hn (dvd.trans h (by simp [mul_pow]))⟩
+λ ⟨n, hn⟩, ⟨n, λ h, hn (h.trans (by simp [mul_pow]))⟩
 
 lemma finite_of_finite_mul_right {a b c : α} : finite a (b * c) → finite a b :=
 by rw mul_comm; exact finite_of_finite_mul_left
@@ -80,7 +80,7 @@ lemma pow_multiplicity_dvd {a b : α} (h : finite a b) : a ^ get (multiplicity a
 pow_dvd_of_le_multiplicity (by rw enat.coe_get)
 
 lemma is_greatest  {a b : α} {m : ℕ} (hm : multiplicity a b < m) : ¬a ^ m ∣ b :=
-λ h, by rw [enat.lt_coe_iff] at hm; exact nat.find_spec hm.fst (dvd.trans (pow_dvd_pow _ hm.snd) h)
+λ h, by rw [enat.lt_coe_iff] at hm; exact nat.find_spec hm.fst ((pow_dvd_pow _ hm.snd).trans h)
 
 lemma is_greatest' {a b : α} {m : ℕ} (h : finite a b) (hm : get (multiplicity a b) h < m) :
   ¬a ^ m ∣ b :=
@@ -169,21 +169,21 @@ lemma multiplicity_le_multiplicity_iff {a b c d : α} : multiplicity a b ≤ mul
 
 lemma multiplicity_le_multiplicity_of_dvd_left {a b c : α} (hdvd : a ∣ b) :
   multiplicity b c ≤ multiplicity a c :=
-multiplicity_le_multiplicity_iff.2 $ λ n h, dvd_trans (pow_dvd_pow_of_dvd hdvd n) h
+multiplicity_le_multiplicity_iff.2 $ λ n h, (pow_dvd_pow_of_dvd hdvd n).trans h
 
 lemma eq_of_associated_left {a b c : α} (h : associated a b) :
   multiplicity b c = multiplicity a c :=
-le_antisymm (multiplicity_le_multiplicity_of_dvd_left (dvd_of_associated h))
-  (multiplicity_le_multiplicity_of_dvd_left (dvd_of_associated h.symm))
+le_antisymm (multiplicity_le_multiplicity_of_dvd_left h.dvd)
+  (multiplicity_le_multiplicity_of_dvd_left h.symm.dvd)
 
 lemma multiplicity_le_multiplicity_of_dvd_right {a b c : α} (h : b ∣ c) :
   multiplicity a b ≤ multiplicity a c :=
-multiplicity_le_multiplicity_iff.2 $ λ n hb, dvd.trans hb h
+multiplicity_le_multiplicity_iff.2 $ λ n hb, hb.trans h
 
 lemma eq_of_associated_right {a b c : α} (h : associated b c) :
   multiplicity a b = multiplicity a c :=
-le_antisymm (multiplicity_le_multiplicity_of_dvd_right (dvd_of_associated h))
-  (multiplicity_le_multiplicity_of_dvd_right (dvd_of_associated h.symm))
+le_antisymm (multiplicity_le_multiplicity_of_dvd_right h.dvd)
+  (multiplicity_le_multiplicity_of_dvd_right h.symm.dvd)
 
 lemma dvd_of_multiplicity_pos {a b : α} (h : (0 : enat) < multiplicity a b) : a ∣ b :=
 by rw [← pow_one a]; exact pow_dvd_of_le_multiplicity (enat.pos_iff_one_le.1 h)
diff --git a/src/ring_theory/polynomial/content.lean b/src/ring_theory/polynomial/content.lean
index 553e6d72747e3..cf6e2574c83f2 100644
--- a/src/ring_theory/polynomial/content.lean
+++ b/src/ring_theory/polynomial/content.lean
@@ -191,7 +191,7 @@ begin
   rw C_dvd_iff_dvd_coeff,
   split,
   { intros h i,
-    apply dvd_trans h (content_dvd_coeff _) },
+    apply h.trans (content_dvd_coeff _) },
   { intro h,
     rw [content, finset.dvd_gcd_iff],
     intros i hi,
@@ -328,7 +328,7 @@ begin
     content_C_mul, h, mul_one, content_prim_part, content_prim_part, mul_one, mul_one] },
   rw [← normalize_content, normalize_eq_one, is_unit_iff_dvd_one,
       content_eq_gcd_leading_coeff_content_erase_lead, leading_coeff_mul, gcd_comm],
-  apply dvd_trans (gcd_mul_dvd_mul_gcd _ _ _),
+  apply (gcd_mul_dvd_mul_gcd _ _ _).trans,
   rw [content_mul_aux, ih, content_prim_part, mul_one, gcd_comm,
       ← content_eq_gcd_leading_coeff_content_erase_lead, content_prim_part, one_mul,
       mul_comm q.prim_part, content_mul_aux, ih, content_prim_part, mul_one, gcd_comm,
@@ -372,7 +372,7 @@ lemma is_primitive.dvd_prim_part_iff_dvd {p q : polynomial R}
   (hp : p.is_primitive) (hq : q ≠ 0) :
   p ∣ q.prim_part ↔ p ∣ q :=
 begin
-  refine ⟨λ h, dvd.trans h (dvd.intro_left _ q.eq_C_content_mul_prim_part.symm), λ h, _⟩,
+  refine ⟨λ h, h.trans (dvd.intro_left _ q.eq_C_content_mul_prim_part.symm), λ h, _⟩,
   rcases h with ⟨r, rfl⟩,
   apply dvd.intro _,
   rw [prim_part_mul hq, hp.prim_part_eq],
@@ -386,7 +386,7 @@ begin
   have h : ∃ (n : ℕ) (r : polynomial R), r.nat_degree = n ∧ r.is_primitive ∧ p ∣ r ∧ q ∣ r :=
     ⟨(p * q).nat_degree, p * q, rfl, hp.mul hq, dvd_mul_right _ _, dvd_mul_left _ _⟩,
   rcases nat.find_spec h with ⟨r, rdeg, rprim, pr, qr⟩,
-  refine ⟨r, rprim, λ s, ⟨_, λ rs, ⟨dvd.trans pr rs, dvd.trans qr rs⟩⟩⟩,
+  refine ⟨r, rprim, λ s, ⟨_, λ rs, ⟨pr.trans rs, qr.trans rs⟩⟩⟩,
   suffices hs : ∀ (n : ℕ) (s : polynomial R), s.nat_degree = n → (p ∣ s ∧ q ∣ s → r ∣ s),
   { apply hs s.nat_degree s rfl },
   clear s,
@@ -415,7 +415,7 @@ begin
   rw [ne.def, ← leading_coeff_eq_zero, ← C_eq_zero] at hC0,
   rw [sub_add_cancel, ← rprim.dvd_prim_part_iff_dvd (mul_ne_zero hC0 s0)] at h,
   rcases is_unit_prim_part_C r.leading_coeff with ⟨u, hu⟩,
-  apply dvd.trans h (dvd_of_associated (associated.symm ⟨u, _⟩)),
+  apply h.trans (associated.symm ⟨u, _⟩).dvd,
   rw [prim_part_mul (mul_ne_zero hC0 s0), hu, mul_comm],
 end
 
@@ -426,7 +426,7 @@ begin
   split; intro h,
   { rcases h with ⟨r, rfl⟩,
     rw [content_mul, p.is_primitive_prim_part.dvd_prim_part_iff_dvd hq],
-    exact ⟨dvd.intro _ rfl, dvd.trans p.prim_part_dvd (dvd.intro _ rfl)⟩ },
+    exact ⟨dvd.intro _ rfl, p.prim_part_dvd.trans (dvd.intro _ rfl)⟩ },
   { rw [p.eq_C_content_mul_prim_part, q.eq_C_content_mul_prim_part],
     exact mul_dvd_mul (ring_hom.map_dvd C h.1) h.2 }
 end
diff --git a/src/ring_theory/polynomial/gauss_lemma.lean b/src/ring_theory/polynomial/gauss_lemma.lean
index 66f7b3256fe3b..34f8e8ac43e68 100644
--- a/src/ring_theory/polynomial/gauss_lemma.lean
+++ b/src/ring_theory/polynomial/gauss_lemma.lean
@@ -145,12 +145,13 @@ begin
     apply map_injective (algebra_map R K) (is_fraction_ring.injective _ _),
     rw [map_mul, map_mul, hs, hr, mul_assoc, mul_comm r],
     simp },
-  rw [← hp.dvd_prim_part_iff_dvd, prim_part_mul, hq.prim_part_eq, dvd_iff_dvd_of_rel_right] at h,
+  rw [← hp.dvd_prim_part_iff_dvd, prim_part_mul, hq.prim_part_eq,
+      associated.dvd_iff_dvd_right] at h,
   { exact h },
   { symmetry,
     rcases is_unit_prim_part_C s with ⟨u, hu⟩,
     use u,
-    simp [hu], },
+    rw hu },
   iterate 2 { apply mul_ne_zero hq.ne_zero,
     rw [ne.def, C_eq_zero],
     contrapose! s0,
diff --git a/src/ring_theory/principal_ideal_domain.lean b/src/ring_theory/principal_ideal_domain.lean
index 6d2aa60943acc..920ae580637a6 100644
--- a/src/ring_theory/principal_ideal_domain.lean
+++ b/src/ring_theory/principal_ideal_domain.lean
@@ -193,7 +193,7 @@ variables [integral_domain R] [is_principal_ideal_ring R]
 lemma irreducible_iff_prime {p : R} : irreducible p ↔ prime p :=
 ⟨λ hp, (ideal.span_singleton_prime hp.ne_zero).1 $
     (is_maximal_of_irreducible hp).is_prime,
-  irreducible_of_prime⟩
+  prime.irreducible⟩
 
 lemma associates_irreducible_iff_prime : ∀{p : associates R}, irreducible p ↔ prime p :=
 associates.irreducible_iff_prime_iff.1 (λ _, irreducible_iff_prime)
diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean
index 6c8bae46bb857..a41b8f01435a3 100644
--- a/src/ring_theory/roots_of_unity.lean
+++ b/src/ring_theory/roots_of_unity.lean
@@ -882,7 +882,7 @@ begin
       rw map_dvd_map (int.cast_ring_hom ℚ) int.cast_injective Pmonic,
       intro hdiv,
       refine hdiff (eq_of_monic_of_associated Pmonic Qmonic _),
-      exact associated_of_dvd_dvd hdiv (dvd_symm_of_irreducible Pirr Qirr hdiv) },
+      exact associated_of_dvd_dvd hdiv (Pirr.dvd_symm Qirr hdiv) },
     { apply (map_dvd_map (int.cast_ring_hom ℚ) int.cast_injective Pmonic).2,
       exact minpoly_dvd_X_pow_sub_one h hpos },
     { apply (map_dvd_map (int.cast_ring_hom ℚ) int.cast_injective Qmonic).2,
diff --git a/src/ring_theory/unique_factorization_domain.lean b/src/ring_theory/unique_factorization_domain.lean
index da99bdf74e1a5..a11387d9b3763 100644
--- a/src/ring_theory/unique_factorization_domain.lean
+++ b/src/ring_theory/unique_factorization_domain.lean
@@ -77,7 +77,7 @@ lemma exists_irreducible_factor {a : α} (ha : ¬ is_unit a) (ha0 : a ≠ 0) :
       (irreducible_or_factor x hx).elim
         (λ hxi, ⟨x, hxi, hxy ▸ by simp⟩)
         (λ hxf, let ⟨i, hi⟩ := ih x ⟨hx0, y, hy, hxy.symm⟩ hx hx0 hxf in
-          ⟨i, hi.1, dvd.trans hi.2 (hxy ▸ by simp)⟩)) a ha ha0)
+          ⟨i, hi.1, hi.2.trans (hxy ▸ by simp)⟩)) a ha ha0)
 
 @[elab_as_eliminator] lemma induction_on_irreducible {P : α → Prop} (a : α)
   (h0 : P 0) (hu : ∀ u : α, is_unit u → P u)
@@ -102,7 +102,7 @@ wf_dvd_monoid.induction_on_irreducible a
     let ⟨s, hs⟩ := ih ha0 in
     ⟨i ::ₘ s, ⟨by clear _let_match; finish,
       by { rw multiset.prod_cons,
-           exact associated_mul_mul (by refl) hs.2 }⟩⟩)
+           exact hs.2.mul_left _ }⟩⟩)
 
 end wf_dvd_monoid
 
@@ -176,19 +176,19 @@ by haveI := classical.dec_eq α; exact
     multiset.rel_zero_left.2 $
       multiset.eq_zero_of_forall_not_mem (λ x hx,
         have is_unit g.prod, by simpa [associated_one_iff_is_unit] using h.symm,
-        (hg x hx).not_unit (is_unit_iff_dvd_one.2 (dvd.trans (multiset.dvd_prod hx)
+        (hg x hx).not_unit (is_unit_iff_dvd_one.2 ((multiset.dvd_prod hx).trans
           (is_unit_iff_dvd_one.1 this)))))
   (λ p f ih g hf hg hfg,
     let ⟨b, hbg, hb⟩ := exists_associated_mem_of_dvd_prod
       (irreducible_iff_prime.1 (hf p (by simp)))
       (λ q hq, irreducible_iff_prime.1 (hg _ hq)) $
-        (dvd_iff_dvd_of_rel_right hfg).1
+        hfg.dvd_iff_dvd_right.1
           (show p ∣ (p ::ₘ f).prod, by simp) in
     begin
       rw ← multiset.cons_erase hbg,
       exact multiset.rel.cons hb (ih (λ q hq, hf _ (by simp [hq]))
         (λ q (hq : q ∈ g.erase b), hg q (multiset.mem_of_mem_erase hq))
-        (associated_mul_left_cancel
+        (associated.of_mul_left
           (by rwa [← multiset.prod_cons, ← multiset.prod_cons, multiset.cons_erase hbg]) hb
         (hf p (by simp)).ne_zero))
     end)
@@ -204,20 +204,20 @@ by haveI := classical.dec_eq α; exact
     multiset.rel_zero_left.2 $
     multiset.eq_zero_of_forall_not_mem $ λ x hx,
     have is_unit g.prod, by simpa [associated_one_iff_is_unit] using h.symm,
-    (irreducible_of_prime $ hg x hx).not_unit $ is_unit_iff_dvd_one.2 $
-    dvd.trans (multiset.dvd_prod hx) (is_unit_iff_dvd_one.1 this))
+    (hg x hx).not_unit $ is_unit_iff_dvd_one.2 $
+    (multiset.dvd_prod hx).trans (is_unit_iff_dvd_one.1 this))
   (λ p f ih g hf hg hfg,
     let ⟨b, hbg, hb⟩ := exists_associated_mem_of_dvd_prod
       (hf p (by simp)) (λ q hq, hg _ hq) $
-        (dvd_iff_dvd_of_rel_right hfg).1
+        hfg.dvd_iff_dvd_right.1
           (show p ∣ (p ::ₘ f).prod, by simp) in
     begin
       rw ← multiset.cons_erase hbg,
       exact multiset.rel.cons hb (ih (λ q hq, hf _ (by simp [hq]))
         (λ q (hq : q ∈ g.erase b), hg q (multiset.mem_of_mem_erase hq))
-        (associated_mul_left_cancel
+        (associated.of_mul_left
           (by rwa [← multiset.prod_cons, ← multiset.prod_cons, multiset.cons_erase hbg]) hb
-        (hf p (by simp)).ne_zero))
+        (hf p (by simp)).ne_zero)),
     end)
 
 /-- If an irreducible has a prime factorization,
@@ -279,7 +279,7 @@ lemma wf_dvd_monoid.of_exists_prime_factors : wf_dvd_monoid α :=
     cases hadd; apply (classical.some_spec (pf _ _)).1 _ hadd },
   { rw multiset.prod_add,
     transitivity a * c,
-    { apply associated_mul_mul; apply (classical.some_spec (pf _ _)).2 },
+    { apply associated.mul_mul; apply (classical.some_spec (pf _ _)).2 },
     { rw ← b_eq,
       apply (classical.some_spec (pf _ _)).2.symm, } }
 end⟩
@@ -288,10 +288,10 @@ lemma irreducible_iff_prime_of_exists_prime_factors {p : α} : irreducible p ↔
 begin
   by_cases hp0 : p = 0,
   { simp [hp0] },
-  refine ⟨λ h, _, irreducible_of_prime⟩,
+  refine ⟨λ h, _, prime.irreducible⟩,
   obtain ⟨f, hf⟩ := pf p hp0,
   obtain ⟨q, hq, rfl⟩ := prime_factors_irreducible h hf,
-  rw prime_iff_of_associated hq,
+  rw hq.prime_iff,
   exact hf.1 q (multiset.mem_cons_self _ _)
 end
 
@@ -335,20 +335,20 @@ theorem irreducible_iff_prime_of_exists_unique_irreducible_factors [comm_cancel_
             { exact λ i hi, (multiset.mem_add.1 hi).elim (hfa.1 _) (hfb.1 _), },
             calc multiset.prod (p ::ₘ fx)
                   ~ᵤ a * b : by rw [hx, multiset.prod_cons];
-                    exact associated_mul_mul (by refl) hfx.2
+                    exact hfx.2.mul_left _
               ... ~ᵤ (fa).prod * (fb).prod :
-                associated_mul_mul hfa.2.symm hfb.2.symm
+                hfa.2.symm.mul_mul hfb.2.symm
               ... = _ : by rw multiset.prod_add, },
           exact let ⟨q, hqf, hq⟩ := multiset.exists_mem_of_rel_of_mem h
           (multiset.mem_cons_self p _) in
         (multiset.mem_add.1 hqf).elim
-          (λ hqa, or.inl $ (dvd_iff_dvd_of_rel_left hq).2 $
-            (dvd_iff_dvd_of_rel_right hfa.2).1
+          (λ hqa, or.inl $ hq.dvd_iff_dvd_left.2 $
+            hfa.2.dvd_iff_dvd_right.1
               (multiset.dvd_prod hqa))
-          (λ hqb, or.inr $ (dvd_iff_dvd_of_rel_left hq).2 $
-            (dvd_iff_dvd_of_rel_right hfb.2).1
+          (λ hqb, or.inr $ hq.dvd_iff_dvd_left.2 $
+            hfb.2.dvd_iff_dvd_right.1
               (multiset.dvd_prod hqb))
-        end⟩, irreducible_of_prime⟩
+        end⟩, prime.irreducible⟩
 
 theorem unique_factorization_monoid.of_exists_unique_irreducible_factors
   [comm_cancel_monoid_with_zero α]
@@ -385,12 +385,12 @@ begin
   rw [factors],
   split_ifs with ane0, { simp },
   intros x hx, rcases multiset.mem_map.1 hx with ⟨y, ⟨hy, rfl⟩⟩,
-  rw prime_iff_of_associated (normalize_associated),
+  rw (normalize_associated _).prime_iff,
   exact (classical.some_spec (unique_factorization_monoid.exists_prime_factors a ane0)).1 y hy,
 end
 
 theorem irreducible_of_factor {a : α} : ∀ (x : α), x ∈ factors a → irreducible x :=
-λ x h, irreducible_of_prime (prime_of_factor x h)
+λ x h, (prime_of_factor x h).irreducible
 
 theorem normalize_factor {a : α} : ∀ (x : α), x ∈ factors a → normalize x = x :=
 begin
@@ -424,9 +424,7 @@ have multiset.rel associated (p ::ₘ factors b) (factors a),
     (associated.symm $ calc multiset.prod (factors a) ~ᵤ a : factors_prod ha0
       ... = p * b : hb
       ... ~ᵤ multiset.prod (p ::ₘ factors b) :
-        by rw multiset.prod_cons; exact associated_mul_mul
-          (associated.refl _)
-          (associated.symm (factors_prod hb0))),
+        by rw multiset.prod_cons; exact (factors_prod hb0).symm.mul_left _),
 multiset.exists_mem_of_rel_of_mem this (by simp)
 
 @[simp] lemma factors_zero : factors (0 : α) = 0 := dif_pos rfl
@@ -460,8 +458,8 @@ begin
     exact irreducible_of_factor x hx },
   { exact irreducible_of_factor },
   { rw multiset.prod_add,
-    exact associated.trans (associated_mul_mul (factors_prod hx) (factors_prod hy))
-      (factors_prod (mul_ne_zero hx hy)).symm, }
+    exact ((factors_prod hx).mul_mul (factors_prod hy)).trans
+      (factors_prod (mul_ne_zero hx hy)).symm }
 end
 
 @[simp] lemma factors_pow {x : α} (n : ℕ) :
@@ -480,7 +478,7 @@ begin
   split,
   { rintro ⟨c, rfl⟩,
     simp [hx, right_ne_zero_of_mul hy] },
-  { rw [← dvd_iff_dvd_of_rel_left (factors_prod hx), ← dvd_iff_dvd_of_rel_right (factors_prod hy)],
+  { rw [← (factors_prod hx).dvd_iff_dvd_left, ← (factors_prod hy).dvd_iff_dvd_right],
     apply multiset.prod_dvd_prod }
 end
 
@@ -586,7 +584,7 @@ begin
       refine ⟨p * a', b', c', _, mul_left_comm _ _ _, rfl⟩,
       intros q q_dvd_pa' q_dvd_b',
       cases left_dvd_or_dvd_right_of_dvd_prime_mul p_prime q_dvd_pa' with p_dvd_q q_dvd_a',
-      { have : p ∣ c' * b' := dvd_mul_of_dvd_right (dvd_trans p_dvd_q q_dvd_b') _,
+      { have : p ∣ c' * b' := dvd_mul_of_dvd_right (p_dvd_q.trans q_dvd_b') _,
         contradiction },
       exact coprime q_dvd_a' q_dvd_b'  } }
 end
@@ -616,9 +614,8 @@ begin
     apply dvd.intro _ rfl },
   { rw [multiset.le_iff_exists_add],
     rintro ⟨u, hu⟩,
-    rw [← dvd_iff_dvd_of_rel_right (factors_prod hb), hu, prod_add, prod_repeat],
-    apply dvd.trans (dvd_of_associated (associated_pow_pow _)) (dvd.intro u.prod rfl),
-    apply associated_normalize }
+    rw [← (factors_prod hb).dvd_iff_dvd_right, hu, prod_add, prod_repeat],
+    exact (associated.pow_pow $ associated_normalize a).dvd.trans (dvd.intro u.prod rfl) }
 end
 
 lemma multiplicity_eq_count_factors {a b : R} (ha : irreducible a) (hb : b ≠ 0) :