chore(algebra/associated): use more dot notation (#8556)

I was getting annoyed that working with definitions such as `irreducible`, `prime` and `associated`, I had to write quite verbose terms like `dvd_symm_of_irreducible (irreducible_of_prime (prime_of_factor _ hp)) (irreducible_of_prime (prime_of_factor _ hq)) hdvd`, where a lot of redundancy can be eliminated with dot notation: `(prime_of_factor _ hp).irreducible.dvd_symm (prime_of_factor _ hq).irreducible hdvd`. This PR changes the spelling of many of the lemmas in `algebra/associated.lean` to make usage of dot notation easier. It also adds a few shortcut lemmas that address common patterns.

Since this change touches a lot of files, I'll add a RFC label / [open a thread on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/RFC.3A.20adding.20dot.20notations.20.238556) to see what everyone thinks.

Renamings:
 * `irreducible_of_prime` → `prime.irreducible`
 * `dvd_symm_of_irreducible` → `irreducible.dvd_symm`
 * `dvd_symm_iff_of_irreducible` → `irreducible.dvd_comm` (cf. `eq.symm` versus `eq_comm`)
 * `associated_mul_mul` → `associated.mul_mul`
 * `associated_pow_pow` → `associated.pow_pow`
 * `dvd_of_associated` → `associated.dvd`
 * `dvd_dvd_of_associated` → `associated.dvd_dvd`
 * `dvd_iff_dvd_of_rel_{left,right}` → `associated.dvd_iff_dvd_{left,right}`
 * `{eq,ne}_zero_iff_of_associated` → `associated.{eq,ne}_zero_iff`
 * `{irreducible,prime}_of_associated` → `associated.{irreducible,prime}`
 * `{irreducible,is_unit,prime}_iff_of_associated` → `associated.{irreducible,is_unit,prime}_iff`
  * `associated_of_{irreducible,prime}_of_dvd` → `{irreducible,prime}.associated_of_dvd`
 * `gcd_eq_of_associated_{left,right}` → `associated.gcd_eq_{left,right}`
 * `{irreducible,prime}_of_degree_eq_one_of_monic` → `monic.{irreducible,prime}_of_degree_eq_one`
  * `gcd_monoid.prime_of_irreducible` → `irreducible.prime` (since the GCD case is probably the only case we care about for this implication. And we could generalize to Schreier domains if not)

Additions:
 * `associated.is_unit := (associated.is_unit_iff _).mp` (to match `associated.prime` and `associated.irreducible`)
 * `associated.mul_left := associated.mul_mul (associated.refl _) _`
 * `associated.mul_right := associated.mul_mul _  (associated.refl _)`

Other changes:
 * `associated_normalize`, `normalize_associated`, `associates.mk_normalize`, `normalize_apply`, `prime_X_sub_C`: make their final parameter explicit, since it is only inferrable when trying to apply these lemmas. This change helped to golf a few proofs from tactic mode to term mode.
 * slight golfing and style fixes



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: YaelDillies <yael.dillies@gmail.com>

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,17 +187,17 @@ 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,
   rintros ⟨q', rfl⟩,
   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,74 +294,76 @@ 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
     rw [← hv, mul_assoc c (v : α) d, mul_left_comm c, ← hu],
     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, },

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)