refactor(algebra/group_with_zero/defs): use is_*cancel_mul_zero (#17963)

Author: urkud

archive/imo/imo1988_q6.lean

@@ -292,6 +292,6 @@ begin
     { simp only [mul_one, one_mul, add_comm, zero_add] at h,
       have y_dvd : y ∣ y * k := dvd_mul_right y k,
       rw [← h, ← add_assoc, nat.dvd_add_left (dvd_mul_left y y)] at y_dvd,
-      obtain rfl|rfl := (nat.dvd_prime nat.prime_two).mp y_dvd; apply nat.eq_of_mul_eq_mul_left,
-      exacts [zero_lt_one, h.symm, zero_lt_two, h.symm] } }
+      obtain rfl|rfl := (nat.dvd_prime nat.prime_two).mp y_dvd; apply mul_left_cancel₀,
+      exacts [one_ne_zero, h.symm, two_ne_zero, h.symm] } }
 end

src/algebra/associated.lean

@@ -889,22 +889,19 @@ instance : no_zero_divisors (associates α) :=
     have a = 0 ∨ b = 0, from mul_eq_zero.1 this,
     this.imp (assume h, h.symm ▸ rfl) (assume h, h.symm ▸ rfl))⟩
 
-lemma eq_of_mul_eq_mul_left :
-  ∀(a b c : associates α), a ≠ 0 → a * b = a * c → b = c :=
-begin
-  rintros ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h,
-  rcases quotient.exact' h with ⟨u, hu⟩,
-  have hu : a * (b * ↑u) = a * c, { rwa [← mul_assoc] },
-  exact quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩
-end
-
-lemma eq_of_mul_eq_mul_right :
-  ∀(a b c : associates α), b ≠ 0 → a * b = c * b → a = c :=
-λ a b c bne0, (mul_comm b a) ▸ (mul_comm b c) ▸ (eq_of_mul_eq_mul_left b a c bne0)
+instance : cancel_comm_monoid_with_zero (associates α) :=
+{ mul_left_cancel_of_ne_zero :=
+    begin
+      rintros ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h,
+      rcases quotient.exact' h with ⟨u, hu⟩,
+      rw [mul_assoc] at hu,
+      exact quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩
+    end,
+  .. (infer_instance : comm_monoid_with_zero (associates α)) }
 
 lemma le_of_mul_le_mul_left (a b c : associates α) (ha : a ≠ 0) :
   a * b ≤ a * c → b ≤ c
-| ⟨d, hd⟩ := ⟨d, eq_of_mul_eq_mul_left a _ _ ha $ by rwa ← mul_assoc⟩
+| ⟨d, hd⟩ := ⟨d, mul_left_cancel₀ ha $ by rwa ← mul_assoc⟩
 
 lemma one_or_eq_of_le_of_prime :
   ∀(p m : associates α), prime p → m ≤ p → (m = 1 ∨ m = p)
@@ -922,11 +919,6 @@ match h m d dvd_rfl with
   or.inl $ bot_unique $ associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
 end
 
-instance : cancel_comm_monoid_with_zero (associates α) :=
-{ mul_left_cancel_of_ne_zero := eq_of_mul_eq_mul_left,
-  mul_right_cancel_of_ne_zero := eq_of_mul_eq_mul_right,
-  .. (infer_instance : comm_monoid_with_zero (associates α)) }
-
 instance : canonically_ordered_monoid (associates α) :=
 { exists_mul_of_le := λ a b, id,
   le_self_mul := λ a b, ⟨b, rfl⟩,

src/algebra/char_p/basic.lean

@@ -411,9 +411,9 @@ or.elim (eq_zero_or_eq_zero_of_mul_eq_zero this)
   have p ∣ e, from (cast_eq_zero_iff R p e).mp he,
   have e ∣ p, from dvd_of_mul_left_eq d (eq.symm hmul),
   have e = p, from dvd_antisymm ‹e ∣ p› ‹p ∣ e›,
-  have h₀ : p > 0, from gt_of_ge_of_gt hp (nat.zero_lt_succ 1),
+  have h₀ : 0 < p, from two_pos.trans_le hp,
   have d * p = 1 * p, by rw ‹e = p› at hmul; rw [one_mul]; exact eq.symm hmul,
-  show d = 1 ∨ d = p, from or.inl (eq_of_mul_eq_mul_right h₀ this))
+  show d = 1 ∨ d = p, from or.inl (mul_right_cancel₀ h₀.ne' this))
 
 section nontrivial
 

src/algebra/group_with_zero/defs.lean

@@ -38,29 +38,75 @@ class mul_zero_class (M₀ : Type*) extends has_mul M₀, has_zero M₀ :=
 (zero_mul : ∀ a : M₀, 0 * a = 0)
 (mul_zero : ∀ a : M₀, a * 0 = 0)
 
+section mul_zero_class
+
+variables [mul_zero_class M₀] {a b : M₀}
+
+@[ematch, simp] lemma zero_mul (a : M₀) : 0 * a = 0 :=
+mul_zero_class.zero_mul a
+
+@[ematch, simp] lemma mul_zero (a : M₀) : a * 0 = 0 :=
+mul_zero_class.mul_zero a
+
+end mul_zero_class
+
 /-- A mixin for left cancellative multiplication by nonzero elements. -/
 @[protect_proj] class is_left_cancel_mul_zero (M₀ : Type u) [has_mul M₀] [has_zero M₀] : Prop :=
 (mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c)
 
+section is_left_cancel_mul_zero
+
+variables [has_mul M₀] [has_zero M₀] [is_left_cancel_mul_zero M₀] {a b c : M₀}
+
+lemma mul_left_cancel₀ (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
+is_left_cancel_mul_zero.mul_left_cancel_of_ne_zero ha h
+
+lemma mul_right_injective₀ (ha : a ≠ 0) : function.injective ((*) a) :=
+λ b c, mul_left_cancel₀ ha
+
+end is_left_cancel_mul_zero
+
 /-- A mixin for right cancellative multiplication by nonzero elements. -/
 @[protect_proj] class is_right_cancel_mul_zero (M₀ : Type u) [has_mul M₀] [has_zero M₀] : Prop :=
 (mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c)
 
+section is_right_cancel_mul_zero
+
+variables [has_mul M₀] [has_zero M₀] [is_right_cancel_mul_zero M₀] {a b c : M₀}
+
+lemma mul_right_cancel₀ (hb : b ≠ 0) (h : a * b = c * b) : a = c :=
+is_right_cancel_mul_zero.mul_right_cancel_of_ne_zero hb h
+
+lemma mul_left_injective₀ (hb : b ≠ 0) : function.injective (λ a, a * b) :=
+λ a c, mul_right_cancel₀ hb
+
+end is_right_cancel_mul_zero
+
 /-- A mixin for cancellative multiplication by nonzero elements. -/
 @[protect_proj] class is_cancel_mul_zero (M₀ : Type u) [has_mul M₀] [has_zero M₀]
   extends is_left_cancel_mul_zero M₀, is_right_cancel_mul_zero M₀ : Prop
 
-section mul_zero_class
+section comm_semigroup_with_zero
 
-variables [mul_zero_class M₀] {a b : M₀}
+variables [comm_semigroup M₀] [has_zero M₀]
 
-@[ematch, simp] lemma zero_mul (a : M₀) : 0 * a = 0 :=
-mul_zero_class.zero_mul a
+lemma is_left_cancel_mul_zero.to_is_right_cancel_mul_zero [is_left_cancel_mul_zero M₀] :
+  is_right_cancel_mul_zero M₀ :=
+⟨λ a b c ha h, mul_left_cancel₀ ha $ (mul_comm _ _).trans $ (h.trans (mul_comm _ _))⟩
 
-@[ematch, simp] lemma mul_zero (a : M₀) : a * 0 = 0 :=
-mul_zero_class.mul_zero a
+lemma is_right_cancel_mul_zero.to_is_left_cancel_mul_zero [is_right_cancel_mul_zero M₀] :
+  is_left_cancel_mul_zero M₀ :=
+⟨λ a b c ha h, mul_right_cancel₀ ha $ (mul_comm _ _).trans $ (h.trans (mul_comm _ _))⟩
 
-end mul_zero_class
+lemma is_left_cancel_mul_zero.to_is_cancel_mul_zero [is_left_cancel_mul_zero M₀] :
+  is_cancel_mul_zero M₀ :=
+{ .. ‹is_left_cancel_mul_zero M₀›, .. is_left_cancel_mul_zero.to_is_right_cancel_mul_zero }
+
+lemma is_right_cancel_mul_zero.to_is_cancel_mul_zero [is_right_cancel_mul_zero M₀] :
+  is_cancel_mul_zero M₀ :=
+{ .. ‹is_right_cancel_mul_zero M₀›, .. is_right_cancel_mul_zero.to_is_left_cancel_mul_zero }
+
+end comm_semigroup_with_zero
 
 /-- Predicate typeclass for expressing that `a * b = 0` implies `a = 0` or `b = 0`
 for all `a` and `b` of type `G₀`. -/
@@ -97,31 +143,11 @@ class cancel_monoid_with_zero (M₀ : Type*) extends monoid_with_zero M₀ :=
 (mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c)
 (mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c)
 
-section cancel_monoid_with_zero
-
-variables [cancel_monoid_with_zero M₀] {a b c : M₀}
-
-lemma mul_left_cancel₀ (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
-cancel_monoid_with_zero.mul_left_cancel_of_ne_zero ha h
-
-lemma mul_right_cancel₀ (hb : b ≠ 0) (h : a * b = c * b) : a = c :=
-cancel_monoid_with_zero.mul_right_cancel_of_ne_zero hb h
-
-lemma mul_right_injective₀ (ha : a ≠ 0) : function.injective ((*) a) :=
-λ b c, mul_left_cancel₀ ha
-
-lemma mul_left_injective₀ (hb : b ≠ 0) : function.injective (λ a, a * b) :=
-λ a c, mul_right_cancel₀ hb
-
 /-- A `cancel_monoid_with_zero` satisfies `is_cancel_mul_zero`. -/
 @[priority 100]
-instance cancel_monoid_with_zero.to_is_cancel_mul_zero : is_cancel_mul_zero M₀ :=
-{ mul_left_cancel_of_ne_zero := λ a b c ha h,
-    cancel_monoid_with_zero.mul_left_cancel_of_ne_zero ha h,
-  mul_right_cancel_of_ne_zero :=  λ a b c hb h,
-    cancel_monoid_with_zero.mul_right_cancel_of_ne_zero hb h, }
-
-end cancel_monoid_with_zero
+instance cancel_monoid_with_zero.to_is_cancel_mul_zero [cancel_monoid_with_zero M₀] :
+  is_cancel_mul_zero M₀ :=
+{ .. ‹cancel_monoid_with_zero M₀› }
 
 /-- A type `M` is a commutative “monoid with zero” if it is a commutative monoid with zero
 element, and `0` is left and right absorbing. -/
@@ -132,8 +158,13 @@ class comm_monoid_with_zero (M₀ : Type*) extends comm_monoid M₀, monoid_with
  `0` is left and right absorbing,
   and left/right multiplication by a non-zero element is injective. -/
 @[protect_proj, ancestor comm_monoid_with_zero cancel_monoid_with_zero]
-class cancel_comm_monoid_with_zero (M₀ : Type*) extends
-  comm_monoid_with_zero M₀, cancel_monoid_with_zero M₀.
+class cancel_comm_monoid_with_zero (M₀ : Type*) extends comm_monoid_with_zero M₀ :=
+(mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c)
+
+@[priority 100]
+instance cancel_comm_monoid_with_zero.to_cancel_monoid_with_zero
+  [h : cancel_comm_monoid_with_zero M₀] : cancel_monoid_with_zero M₀ :=
+{ .. h, .. @is_left_cancel_mul_zero.to_is_right_cancel_mul_zero M₀ _ _ { .. h } }
 
 /-- A type `G₀` is a “group with zero” if it is a monoid with zero element (distinct from `1`)
 such that every nonzero element is invertible.
@@ -147,42 +178,6 @@ class group_with_zero (G₀ : Type u) extends
 (inv_zero : (0 : G₀)⁻¹ = 0)
 (mul_inv_cancel : ∀ a:G₀, a ≠ 0 → a * a⁻¹ = 1)
 
-namespace comm_monoid_with_zero
-
-variable [comm_monoid_with_zero M₀]
-
-lemma is_left_cancel_mul_zero.to_is_right_cancel_mul_zero [is_left_cancel_mul_zero M₀] :
-  is_right_cancel_mul_zero M₀ :=
-{ mul_right_cancel_of_ne_zero := λ a b c ha h,
-  begin
-    rw [mul_comm, mul_comm c] at h,
-    exact is_left_cancel_mul_zero.mul_left_cancel_of_ne_zero ha h,
-  end }
-
-lemma is_right_cancel_mul_zero.to_is_left_cancel_mul_zero [is_right_cancel_mul_zero M₀] :
-  is_left_cancel_mul_zero M₀ :=
-{ mul_left_cancel_of_ne_zero := λ a b c ha h,
-  begin
-    rw [mul_comm a, mul_comm a c] at h,
-    exact is_right_cancel_mul_zero.mul_right_cancel_of_ne_zero ha h,
-  end }
-
-lemma is_left_cancel_mul_zero.to_is_cancel_mul_zero [is_left_cancel_mul_zero M₀] :
-  is_cancel_mul_zero M₀ :=
-{ mul_left_cancel_of_ne_zero := λ _ _ _,
-    is_left_cancel_mul_zero.mul_left_cancel_of_ne_zero,
-  mul_right_cancel_of_ne_zero := λ _ _ _,
-    is_left_cancel_mul_zero.to_is_right_cancel_mul_zero.mul_right_cancel_of_ne_zero }
-
-lemma is_right_cancel_mul_zero.to_is_cancel_mul_zero [is_right_cancel_mul_zero M₀] :
-  is_cancel_mul_zero M₀ :=
-{ mul_left_cancel_of_ne_zero := λ _ _ _,
-    is_right_cancel_mul_zero.to_is_left_cancel_mul_zero.mul_left_cancel_of_ne_zero,
-  mul_right_cancel_of_ne_zero := λ _ _ _,
-    is_right_cancel_mul_zero.mul_right_cancel_of_ne_zero }
-
-end comm_monoid_with_zero
-
 section group_with_zero
 
 variables [group_with_zero G₀]

src/algebra/ring/regular.lean

@@ -71,18 +71,12 @@ section is_domain
 @[priority 100] -- see Note [lower instance priority]
 instance is_domain.to_cancel_monoid_with_zero [semiring α] [is_domain α] :
   cancel_monoid_with_zero α :=
-{ mul_left_cancel_of_ne_zero := λ a b c ha h,
-    is_cancel_mul_zero.mul_left_cancel_of_ne_zero ha h,
-  mul_right_cancel_of_ne_zero := λ a b c ha h,
-    is_cancel_mul_zero.mul_right_cancel_of_ne_zero ha h,
-  .. semiring.to_monoid_with_zero α }
+{ .. semiring.to_monoid_with_zero α, .. ‹is_domain α› }
 
 variables [comm_semiring α] [is_domain α]
 
 @[priority 100] -- see Note [lower instance priority]
 instance is_domain.to_cancel_comm_monoid_with_zero : cancel_comm_monoid_with_zero α :=
-{ mul_left_cancel_of_ne_zero := λ a b c ha H, is_domain.mul_left_cancel_of_ne_zero ha H,
-  mul_right_cancel_of_ne_zero := λ a b c hb H, is_domain.mul_right_cancel_of_ne_zero hb H,
-  .. (infer_instance : comm_semiring α) }
+{ .. ‹comm_semiring α›, .. ‹is_domain α› }
 
 end is_domain

src/data/nat/basic.lean

@@ -79,15 +79,10 @@ instance : semiring ℕ                     := infer_instance
 
 protected lemma nat.nsmul_eq_mul (m n : ℕ) : m • n = m * n := rfl
 
-theorem nat.eq_of_mul_eq_mul_right {n m k : ℕ} (Hm : 0 < m) (H : n * m = k * m) : n = k :=
-by rw [mul_comm n m, mul_comm k m] at H; exact nat.eq_of_mul_eq_mul_left Hm H
-
 instance nat.cancel_comm_monoid_with_zero : cancel_comm_monoid_with_zero ℕ :=
 { mul_left_cancel_of_ne_zero :=
     λ _ _ _ h1 h2, nat.eq_of_mul_eq_mul_left (nat.pos_of_ne_zero h1) h2,
-  mul_right_cancel_of_ne_zero :=
-    λ _ _ _ h1 h2, nat.eq_of_mul_eq_mul_right (nat.pos_of_ne_zero h1) h2,
-  .. (infer_instance : comm_monoid_with_zero ℕ) }
+  .. nat.comm_semiring }
 
 attribute [simp] nat.not_lt_zero nat.succ_ne_zero nat.succ_ne_self
   nat.zero_ne_one nat.one_ne_zero

src/data/nat/choose/basic.lean

@@ -124,9 +124,8 @@ end
 lemma choose_mul {n k s : ℕ} (hkn : k ≤ n) (hsk : s ≤ k) :
   n.choose k * k.choose s = n.choose s * (n - s).choose (k - s) :=
 begin
-  have h : 0 < (n - k)! * (k - s)! * s! :=
-    mul_pos (mul_pos (factorial_pos _) (factorial_pos _)) (factorial_pos _),
-  refine eq_of_mul_eq_mul_right h _,
+  have h : (n - k)! * (k - s)! * s! ≠ 0, by apply_rules [mul_ne_zero, factorial_ne_zero],
+  refine mul_right_cancel₀ h _,
   calc
     n.choose k * k.choose s * ((n - k)! * (k - s)! * s!)
         = n.choose k * (k.choose s * s! * (k - s)!) * (n - k)!

src/data/nat/gcd/basic.lean

@@ -104,9 +104,9 @@ end
 
 theorem gcd_div {m n k : ℕ} (H1 : k ∣ m) (H2 : k ∣ n) :
   gcd (m / k) (n / k) = gcd m n / k :=
-or.elim (nat.eq_zero_or_pos k)
+(decidable.eq_or_ne k 0).elim
   (λk0, by rw [k0, nat.div_zero, nat.div_zero, nat.div_zero, gcd_zero_right])
-  (λH3, nat.eq_of_mul_eq_mul_right H3 $ by rw [
+  (λH3, mul_right_cancel₀ H3 $ by rw [
     nat.div_mul_cancel (dvd_gcd H1 H2), ←gcd_mul_right,
     nat.div_mul_cancel H1, nat.div_mul_cancel H2])
 

src/data/rat/defs.lean

@@ -162,8 +162,7 @@ begin
       all_goals { exact int.coe_nat_dvd.2 (nat.gcd_dvd_left _ _) } },
     intros a c h,
     suffices bd : b / a.gcd b = d / c.gcd d,
-    { refine ⟨_, bd⟩,
-      apply nat.eq_of_mul_eq_mul_left hb,
+    { refine ⟨mul_left_cancel₀ hb.ne' _, bd⟩,
       rw [← nat.mul_div_assoc _ (nat.gcd_dvd_left _ _), mul_comm,
           nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), bd,
           ← nat.mul_div_assoc _ (nat.gcd_dvd_right _ _), h, mul_comm,

src/number_theory/cyclotomic/primitive_roots.lean

@@ -362,12 +362,12 @@ begin
       pnat.pow_coe, pnat.pow_coe, nat.totient_prime_pow hpri.out (k - s).succ_pos,
       nat.totient_prime_pow hpri.out k.succ_pos, mul_comm _ (↑p - 1), mul_assoc,
       mul_comm (↑p ^ (k.succ - 1))] at this,
-    replace this := nat.eq_of_mul_eq_mul_left (tsub_pos_iff_lt.2 (nat.prime.one_lt hpri.out)) this,
+    replace this := mul_left_cancel₀ (tsub_pos_iff_lt.2 hpri.out.one_lt).ne' this,
     have Hex : k.succ - 1 = (k - s).succ - 1 + s,
     { simp only [nat.succ_sub_succ_eq_sub, tsub_zero],
       exact (nat.sub_add_cancel hs).symm },
     rw [Hex, pow_add] at this,
-    exact nat.eq_of_mul_eq_mul_left (pow_pos hpri.out.pos _) this },
+    exact mul_left_cancel₀ (pow_ne_zero _ hpri.out.ne_zero) this },
   all_goals { apply_instance }
 end