refactor: use Is*CancelMulZero (#1137)

This is a Lean 4 version of leanprover-community/mathlib#17963

Mathlib/Algebra/Associated.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Jens Wagemaker
 
 ! This file was ported from Lean 3 source module algebra.associated
-! leanprover-community/mathlib commit dcf2250875895376a142faeeac5eabff32c48655
+! leanprover-community/mathlib commit 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1099,28 +1099,19 @@ instance : PartialOrder (Associates α) where
 instance : OrderedCommMonoid (Associates α) where
     mul_le_mul_left := fun a _ ⟨d, hd⟩ c => hd.symm ▸ mul_assoc c a d ▸ le_mul_right
 
+instance : CancelCommMonoidWithZero (Associates α) :=
+{ (by infer_instance : CommMonoidWithZero (Associates α)) with
+  mul_left_cancel_of_ne_zero := by
+    rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h
+    rcases Quotient.exact' h with ⟨u, hu⟩
+    have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
+    exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩ }
+
 instance : NoZeroDivisors (Associates α) :=
-  ⟨by
-    intro x y
-    exact
-      Quotient.inductionOn₂ x y <| fun a b h =>
-      have : a * b = 0 := (associated_zero_iff_eq_zero _).1 (Quotient.exact h)
-      have : a = 0 ∨ b = 0 := mul_eq_zero.1 this
-      this.imp (fun h => by rw [h]; rfl) fun h => by rw [h]; rfl⟩
-
-theorem eq_of_mul_eq_mul_left : ∀ a b c : Associates α, a ≠ 0 → a * b = a * c → b = c := by
-  rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ha h
-  rcases Quotient.exact' h with ⟨u, hu⟩
-  have hu : a * (b * ↑u) = a * c := by rwa [← mul_assoc]
-  exact Quotient.sound' ⟨u, mul_left_cancel₀ (mk_ne_zero.1 ha) hu⟩
-#align associates.eq_of_mul_eq_mul_left Associates.eq_of_mul_eq_mul_left
-
-theorem eq_of_mul_eq_mul_right : ∀ a b c : Associates α, b ≠ 0 → a * b = c * b → a = c :=
-  fun a b c bne0 => mul_comm b a ▸ mul_comm b c ▸ eq_of_mul_eq_mul_left b a c bne0
-#align associates.eq_of_mul_eq_mul_right Associates.eq_of_mul_eq_mul_right
+  by infer_instance
 
 theorem 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]⟩
 #align associates.le_of_mul_le_mul_left Associates.le_of_mul_le_mul_left
 
 theorem one_or_eq_of_le_of_prime : ∀ p m : Associates α, Prime p → m ≤ p → m = 1 ∨ m = p
@@ -1150,15 +1141,10 @@ theorem one_or_eq_of_le_of_prime : ∀ p m : Associates α, Prime p → m ≤ p
           exact Or.inl <| bot_unique <| Associates.le_of_mul_le_mul_left d m 1 ‹d ≠ 0› this
 #align associates.one_or_eq_of_le_of_prime Associates.one_or_eq_of_le_of_prime
 
-instance : CancelCommMonoidWithZero (Associates α) :=
-  { (inferInstance : CommMonoidWithZero (Associates α)) with
-    mul_left_cancel_of_ne_zero := by apply eq_of_mul_eq_mul_left
-    mul_right_cancel_of_ne_zero := by apply eq_of_mul_eq_mul_right }
-
 instance : CanonicallyOrderedMonoid (Associates α) where
-    exists_mul_of_le := by intro a b h; exact h
-    le_self_mul := fun a b => ⟨b, rfl⟩
-    bot_le := by apply one_le
+    exists_mul_of_le := fun h => h
+    le_self_mul := fun _ b => ⟨b, rfl⟩
+    bot_le := fun _ => one_le
 
 theorem dvdNotUnit_iff_lt {a b : Associates α} : DvdNotUnit a b ↔ a < b :=
   dvd_and_not_dvd_iff.symm

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 
 ! This file was ported from Lean 3 source module algebra.group_with_zero.basic
-! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64
+! leanprover-community/mathlib commit 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -149,14 +149,8 @@ variable [CancelMonoidWithZero M₀] {a b c : M₀}
 
 -- see Note [lower instance priority]
 instance (priority := 10) CancelMonoidWithZero.toNoZeroDivisors : NoZeroDivisors M₀ :=
-  ⟨fun {a b} ab0 => by
-    by_cases a = 0
-    · left
-      exact h
-
-    right
-    apply CancelMonoidWithZero.mul_left_cancel_of_ne_zero h
-    rw [ab0, mul_zero]⟩
+  ⟨fun ab0 => or_iff_not_imp_left.mpr <| fun ha => mul_left_cancel₀ ha <|
+    ab0.trans (mul_zero _).symm⟩
 #align cancel_monoid_with_zero.to_no_zero_divisors CancelMonoidWithZero.toNoZeroDivisors
 
 theorem mul_left_inj' (hc : c ≠ 0) : a * c = b * c ↔ a = b :=

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 
 ! This file was ported from Lean 3 source module algebra.group_with_zero.defs
-! leanprover-community/mathlib commit 2aa04f651209dc8f37b9937a8c4c20c79571ac52
+! leanprover-community/mathlib commit 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -56,11 +56,35 @@ class IsLeftCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
   /-- Multiplicatin by a nonzero element is left cancellative. -/
   protected mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c
 
+section IsLeftCancelMulZero
+
+variable [Mul M₀] [Zero M₀] [IsLeftCancelMulZero M₀] {a b c : M₀}
+
+theorem mul_left_cancel₀ (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
+  IsLeftCancelMulZero.mul_left_cancel_of_ne_zero ha h
+
+theorem mul_right_injective₀ (ha : a ≠ 0) : Function.Injective ((· * ·) a) :=
+  fun _ _ => mul_left_cancel₀ ha
+
+end IsLeftCancelMulZero
+
 /-- A mixin for right cancellative multiplication by nonzero elements. -/
 class IsRightCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀] : Prop where
   /-- Multiplicatin by a nonzero element is right cancellative. -/
   protected mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c
 
+section IsRightCancelMulZero
+
+variable [Mul M₀] [Zero M₀] [IsRightCancelMulZero M₀] {a b c : M₀}
+
+theorem mul_right_cancel₀ (hb : b ≠ 0) (h : a * b = c * b) : a = c :=
+  IsRightCancelMulZero.mul_right_cancel_of_ne_zero hb h
+
+theorem mul_left_injective₀ (hb : b ≠ 0) : Function.Injective fun a => a * b :=
+  fun _ _ => mul_right_cancel₀ hb
+
+end IsRightCancelMulZero
+
 /-- A mixin for cancellative multiplication by nonzero elements. -/
 class IsCancelMulZero (M₀ : Type u) [Mul M₀] [Zero M₀]
   extends IsLeftCancelMulZero M₀, IsRightCancelMulZero M₀ : Prop
@@ -88,75 +112,44 @@ class MonoidWithZero (M₀ : Type u) extends Monoid M₀, MulZeroOneClass M₀,
 
 /-- A type `M` is a `CancelMonoidWithZero` if it is a monoid with zero element, `0` is left
 and right absorbing, and left/right multiplication by a non-zero element is injective. -/
-class CancelMonoidWithZero (M₀ : Type _) extends MonoidWithZero M₀ where
-  /-- Left multiplication by a non-zero element is injective. -/
-  protected mul_left_cancel_of_ne_zero : ∀ {a b c : M₀}, a ≠ 0 → a * b = a * c → b = c
-  /-- Right multiplication by a non-zero element is injective. -/
-  protected mul_right_cancel_of_ne_zero : ∀ {a b c : M₀}, b ≠ 0 → a * b = c * b → a = c
-
-section CancelMonoidWithZero
-
-variable [CancelMonoidWithZero M₀] {a b c : M₀}
-
-theorem mul_left_cancel₀ (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
-  CancelMonoidWithZero.mul_left_cancel_of_ne_zero ha h
-
-theorem mul_right_cancel₀ (hb : b ≠ 0) (h : a * b = c * b) : a = c :=
-  CancelMonoidWithZero.mul_right_cancel_of_ne_zero hb h
-
-theorem mul_right_injective₀ (ha : a ≠ 0) : Function.Injective ((· * ·) a) :=
-  fun _ _ => mul_left_cancel₀ ha
-
-theorem mul_left_injective₀ (hb : b ≠ 0) : Function.Injective fun a => a * b :=
-  fun _ _ => mul_right_cancel₀ hb
-
-/-- A `CancelMonoidWithZero` satisfies `IsCancelMulZero`. -/
-instance (priority := 100) CancelMonoidWithZero.to_IsCancelMulZero : IsCancelMulZero M₀ :=
-{ mul_left_cancel_of_ne_zero := fun ha h ↦
-    CancelMonoidWithZero.mul_left_cancel_of_ne_zero ha h
-  mul_right_cancel_of_ne_zero :=  fun hb h ↦
-    CancelMonoidWithZero.mul_right_cancel_of_ne_zero hb h, }
-
-end CancelMonoidWithZero
+class CancelMonoidWithZero (M₀ : Type _) extends MonoidWithZero M₀, IsCancelMulZero 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. -/
 class CommMonoidWithZero (M₀ : Type _) extends CommMonoid M₀, MonoidWithZero M₀
 
-namespace CommMonoidWithZero
+section CommSemigroup
 
-variable [CommMonoidWithZero M₀]
+variable [CommSemigroup M₀] [Zero M₀]
 
 lemma IsLeftCancelMulZero.to_IsRightCancelMulZero [IsLeftCancelMulZero M₀] :
     IsRightCancelMulZero M₀ :=
-{ mul_right_cancel_of_ne_zero := by
-    intros a b c ha h
-    rw [mul_comm, mul_comm c] at h
-    exact IsLeftCancelMulZero.mul_left_cancel_of_ne_zero ha h }
+{ mul_right_cancel_of_ne_zero :=
+    fun hb h => mul_left_cancel₀ hb <| (mul_comm _ _).trans (h.trans (mul_comm _ _)) }
 
 lemma IsRightCancelMulZero.to_IsLeftCancelMulZero [IsRightCancelMulZero M₀] :
     IsLeftCancelMulZero M₀ :=
-{ mul_left_cancel_of_ne_zero := by
-    intros a b c ha h
-    rw [mul_comm a, mul_comm a c] at h
-    exact IsRightCancelMulZero.mul_right_cancel_of_ne_zero ha h }
+{ mul_left_cancel_of_ne_zero :=
+    fun hb h => mul_right_cancel₀ hb <| (mul_comm _ _).trans (h.trans (mul_comm _ _)) }
 
 lemma IsLeftCancelMulZero.to_IsCancelMulZero [IsLeftCancelMulZero M₀] :
     IsCancelMulZero M₀ :=
-{ mul_right_cancel_of_ne_zero := fun ha h ↦
-    IsLeftCancelMulZero.to_IsRightCancelMulZero.mul_right_cancel_of_ne_zero ha h }
+{ IsLeftCancelMulZero.to_IsRightCancelMulZero with }
 
 lemma IsRightCancelMulZero.to_IsCancelMulZero [IsRightCancelMulZero M₀] :
     IsCancelMulZero M₀ :=
-{ mul_left_cancel_of_ne_zero := fun ha h ↦
-    IsRightCancelMulZero.to_IsLeftCancelMulZero.mul_left_cancel_of_ne_zero ha h }
+{ IsRightCancelMulZero.to_IsLeftCancelMulZero with }
 
-end CommMonoidWithZero
+end CommSemigroup
 
 /-- A type `M` is a `CancelCommMonoidWithZero` if it is a commutative monoid with zero element,
  `0` is left and right absorbing,
   and left/right multiplication by a non-zero element is injective. -/
-class CancelCommMonoidWithZero (M₀ : Type _) extends CommMonoidWithZero M₀, CancelMonoidWithZero M₀
+class CancelCommMonoidWithZero (M₀ : Type _) extends CommMonoidWithZero M₀, IsLeftCancelMulZero M₀
+
+instance (priority := 100) CancelCommMonoidWithZero.to_CancelMonoidWithZero
+    [CancelCommMonoidWithZero M₀] : CancelMonoidWithZero M₀ :=
+{ IsLeftCancelMulZero.to_IsCancelMulZero with }
 
 /-- 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.

Mathlib/Algebra/Ring/Regular.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Yury Kudryashov, Neil Strickland
 
 ! This file was ported from Lean 3 source module algebra.ring.regular
-! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
+! leanprover-community/mathlib commit 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -67,24 +67,22 @@ Note this is not an instance as it forms a typeclass loop. -/
 @[reducible]
 def NoZeroDivisors.toCancelCommMonoidWithZero [CommRing α] [NoZeroDivisors α] :
     CancelCommMonoidWithZero α :=
-  { NoZeroDivisors.toCancelMonoidWithZero, (by infer_instance : CommMonoidWithZero α) with }
+  { NoZeroDivisors.toCancelMonoidWithZero, ‹CommRing α› with }
 #align no_zero_divisors.to_cancel_comm_monoid_with_zero NoZeroDivisors.toCancelCommMonoidWithZero
 
 section IsDomain
 
 -- see Note [lower instance priority]
 instance (priority := 100) IsDomain.toCancelMonoidWithZero [Semiring α] [IsDomain α] :
     CancelMonoidWithZero α :=
-  { mul_left_cancel_of_ne_zero := IsLeftCancelMulZero.mul_left_cancel_of_ne_zero
-    mul_right_cancel_of_ne_zero := IsRightCancelMulZero.mul_right_cancel_of_ne_zero }
+  { }
 #align is_domain.to_cancel_monoid_with_zero IsDomain.toCancelMonoidWithZero
 
 variable [CommSemiring α] [IsDomain α]
 
 -- see Note [lower instance priority]
 instance (priority := 100) IsDomain.toCancelCommMonoidWithZero : CancelCommMonoidWithZero α :=
-  { mul_left_cancel_of_ne_zero := IsLeftCancelMulZero.mul_left_cancel_of_ne_zero
-    mul_right_cancel_of_ne_zero := IsRightCancelMulZero.mul_right_cancel_of_ne_zero }
+  { mul_left_cancel_of_ne_zero := IsLeftCancelMulZero.mul_left_cancel_of_ne_zero }
 #align is_domain.to_cancel_comm_monoid_with_zero IsDomain.toCancelCommMonoidWithZero
 
 end IsDomain

Mathlib/Data/Nat/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.nat.basic
-! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025
+! leanprover-community/mathlib commit 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -116,9 +116,7 @@ protected theorem nsmul_eq_mul (m n : ℕ) : m • n = m * n :=
 instance cancelCommMonoidWithZero : CancelCommMonoidWithZero ℕ :=
   { (inferInstance : CommMonoidWithZero ℕ) with
     mul_left_cancel_of_ne_zero :=
-      fun {_ _ _} h1 h2 => Nat.eq_of_mul_eq_mul_left (Nat.pos_of_ne_zero h1) h2,
-    mul_right_cancel_of_ne_zero :=
-      fun {_ _ _} h1 h2 => Nat.eq_of_mul_eq_mul_right (Nat.pos_of_ne_zero h1) h2 }
+      fun h1 h2 => Nat.eq_of_mul_eq_mul_left (Nat.pos_of_ne_zero h1) h2 }
 #align nat.cancel_comm_monoid_with_zero Nat.cancelCommMonoidWithZero
 
 attribute [simp]

Mathlib/Data/Nat/Choose/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Bhavik Mehta, Stuart Presnell
 
 ! This file was ported from Lean 3 source module data.nat.choose.basic
-! leanprover-community/mathlib commit d012cd09a9b256d870751284dd6a29882b0be105
+! leanprover-community/mathlib commit 2f3994e1b117b1e1da49bcfb67334f33460c3ce4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -144,10 +144,9 @@ theorem choose_mul_factorial_mul_factorial : ∀ {n k}, k ≤ n → choose n k *
 #align nat.choose_mul_factorial_mul_factorial Nat.choose_mul_factorial_mul_factorial
 
 theorem 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) := by
-  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 _
+    n.choose k * k.choose s = n.choose s * (n - s).choose (k - s) :=
+  have h : (n - k)! * (k - s)! * s ! ≠ 0:= by apply_rules [factorial_ne_zero, mul_ne_zero]
+  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)! :=