refactor(algebra/group/defs): remove left-right_cancel_comm_monoids (#7134)

adomani · urkud · adomani · commit 46302c7055a8 · 2021-04-12T23:25:53.000Z
There were 6 distinct classes
* `(add_)left_cancel_comm_monoid`,
* `(add_)right_cancel_comm_monoid`,
* `(add_)cancel_comm_monoid`.

I removed them all, except for the last 2:
* `(add_)cancel_comm_monoid`.

The new typeclass `cancel_comm_monoid` requires only `a * b = a * c → b = c`, and deduces the other version from commutativity.



Co-authored-by: Yury G. Kudryashov &lt;urkud@urkud.name&gt;
diff --git a/src/algebra/group/defs.lean b/src/algebra/group/defs.lean
@@ -240,14 +240,13 @@ by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b]
 
 end monoid
 
-/-- A commutative monoid is a monoid with commutative `(*)`. -/
-@[protect_proj, ancestor monoid comm_semigroup]
-class comm_monoid (M : Type u) extends monoid M, comm_semigroup M
-
 /-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
 @[protect_proj, ancestor add_monoid add_comm_semigroup]
 class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
-attribute [to_additive] comm_monoid
+
+/-- A commutative monoid is a monoid with commutative `(*)`. -/
+@[protect_proj, ancestor monoid comm_semigroup, to_additive]
+class comm_monoid (M : Type u) extends monoid M, comm_semigroup M
 
 section left_cancel_monoid
 
@@ -256,21 +255,11 @@ Main examples are `ℕ` and groups. This is the right typeclass for many sum lem
 is useful to define the sum over the empty set, so `add_left_cancel_semigroup` is not enough. -/
 @[protect_proj, ancestor add_left_cancel_semigroup add_monoid]
 class add_left_cancel_monoid (M : Type u) extends add_left_cancel_semigroup M, add_monoid M
--- TODO: I found 1 (one) lemma assuming `[add_left_cancel_monoid]`.
--- Should we port more lemmas to this typeclass?
 
 /-- A monoid in which multiplication is left-cancellative. -/
 @[protect_proj, ancestor left_cancel_semigroup monoid, to_additive add_left_cancel_monoid]
 class left_cancel_monoid (M : Type u) extends left_cancel_semigroup M, monoid M
 
-/-- Commutative version of add_left_cancel_monoid. -/
-@[protect_proj, ancestor add_left_cancel_monoid add_comm_monoid]
-class add_left_cancel_comm_monoid (M : Type u) extends add_left_cancel_monoid M, add_comm_monoid M
-
-/-- Commutative version of left_cancel_monoid. -/
-@[protect_proj, ancestor left_cancel_monoid comm_monoid, to_additive add_left_cancel_comm_monoid]
-class left_cancel_comm_monoid (M : Type u) extends left_cancel_monoid M, comm_monoid M
-
 end left_cancel_monoid
 
 section right_cancel_monoid
@@ -285,14 +274,6 @@ class add_right_cancel_monoid (M : Type u) extends add_right_cancel_semigroup M,
 @[protect_proj, ancestor right_cancel_semigroup monoid, to_additive add_right_cancel_monoid]
 class right_cancel_monoid (M : Type u) extends right_cancel_semigroup M, monoid M
 
-/-- Commutative version of add_right_cancel_monoid. -/
-@[protect_proj, ancestor add_right_cancel_monoid add_comm_monoid]
-class add_right_cancel_comm_monoid (M : Type u) extends add_right_cancel_monoid M, add_comm_monoid M
-
-/-- Commutative version of right_cancel_monoid. -/
-@[protect_proj, ancestor right_cancel_monoid comm_monoid, to_additive add_right_cancel_comm_monoid]
-class right_cancel_comm_monoid (M : Type u) extends right_cancel_monoid M, comm_monoid M
-
 end right_cancel_monoid
 
 section cancel_monoid
@@ -309,14 +290,18 @@ class add_cancel_monoid (M : Type u)
 class cancel_monoid (M : Type u) extends left_cancel_monoid M, right_cancel_monoid M
 
 /-- Commutative version of add_cancel_monoid. -/
-@[protect_proj, ancestor add_left_cancel_comm_monoid add_right_cancel_comm_monoid]
-class add_cancel_comm_monoid (M : Type u)
-  extends add_left_cancel_comm_monoid M, add_right_cancel_comm_monoid M
+@[protect_proj, ancestor add_left_cancel_monoid add_comm_monoid]
+class add_cancel_comm_monoid (M : Type u) extends add_left_cancel_monoid M, add_comm_monoid M
 
 /-- Commutative version of cancel_monoid. -/
-@[protect_proj, ancestor left_cancel_comm_monoid right_cancel_comm_monoid,
-  to_additive add_cancel_comm_monoid]
-class cancel_comm_monoid (M : Type u) extends left_cancel_comm_monoid M, right_cancel_comm_monoid M
+@[protect_proj, ancestor left_cancel_monoid comm_monoid, to_additive add_cancel_comm_monoid]
+class cancel_comm_monoid (M : Type u) extends left_cancel_monoid M, comm_monoid M
+
+@[priority 100, to_additive] -- see Note [lower instance priority]
+instance cancel_comm_monoid.to_cancel_monoid (M : Type u) [cancel_comm_monoid M] :
+  cancel_monoid M :=
+{ mul_right_cancel := λ a b c h, mul_left_cancel $ by rw [mul_comm, h, mul_comm],
+  .. ‹cancel_comm_monoid M› }
 
 end cancel_monoid
 
diff --git a/src/algebra/group/inj_surj.lean b/src/algebra/group/inj_surj.lean
@@ -123,6 +123,16 @@ protected def comm_monoid [comm_monoid M₂] (f : M₁ → M₂) (hf : injective
   comm_monoid M₁ :=
 { .. hf.comm_semigroup f mul, .. hf.monoid f one mul }
 
+/-- A type endowed with `1` and `*` is a cancel commutative monoid,
+if it admits an injective map that preserves `1` and `*` to a cancel commutative monoid. -/
+@[to_additive add_cancel_comm_monoid
+"A type endowed with `0` and `+` is an additive cancel commutative monoid,
+if it admits an injective map that preserves `0` and `+` to an additive cancel commutative monoid."]
+protected def cancel_comm_monoid [cancel_comm_monoid M₂] (f : M₁ → M₂) (hf : injective f)
+  (one : f 1 = 1) (mul : ∀ x y, f (x * y) = f x * f y) :
+  cancel_comm_monoid M₁ :=
+{ .. hf.left_cancel_semigroup f mul, .. hf.comm_monoid f one mul }
+
 variables [has_inv M₁] [has_div M₁]
 
 /-- A type endowed with `1`, `*`, `⁻¹`, and `/` is a `div_inv_monoid`
diff --git a/src/algebra/group/prod.lean b/src/algebra/group/prod.lean
@@ -137,7 +137,7 @@ instance [comm_monoid M] [comm_monoid N] : comm_monoid (M × N) :=
 
 @[to_additive]
 instance [cancel_comm_monoid M] [cancel_comm_monoid N] : cancel_comm_monoid (M × N) :=
-{ .. prod.left_cancel_monoid, .. prod.right_cancel_monoid, .. prod.comm_monoid }
+{ .. prod.left_cancel_monoid, .. prod.comm_monoid }
 
 instance [monoid_with_zero M] [monoid_with_zero N] : monoid_with_zero (M × N) :=
 { .. prod.monoid, .. prod.mul_zero_class }
diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean
@@ -73,7 +73,6 @@ instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u)
   [s : ordered_comm_group α] :
   ordered_cancel_comm_monoid α :=
 { mul_left_cancel       := @mul_left_cancel α _,
-  mul_right_cancel      := @mul_right_cancel α _,
   le_of_mul_le_mul_left := @ordered_comm_group.le_of_mul_le_mul_left α _,
   ..s }
 
@@ -587,7 +586,6 @@ instance linear_ordered_comm_group.to_linear_ordered_cancel_comm_monoid :
   linear_ordered_cancel_comm_monoid α :=
 { le_of_mul_le_mul_left := λ x y z, le_of_mul_le_mul_left',
   mul_left_cancel := λ x y z, mul_left_cancel,
-  mul_right_cancel := λ x y z, mul_right_cancel,
   ..‹linear_ordered_comm_group α› }
 
 /-- Pullback a `linear_ordered_comm_group` under an injective map. -/
diff --git a/src/algebra/ordered_monoid.lean b/src/algebra/ordered_monoid.lean
@@ -1069,7 +1069,6 @@ def function.injective.ordered_cancel_comm_monoid {β : Type*}
 { le_of_mul_le_mul_left := λ a b c (ab : f (a * b) ≤ f (a * c)),
     (by { rw [mul, mul] at ab, exact le_of_mul_le_mul_left' ab }),
   ..hf.left_cancel_semigroup f mul,
-  ..hf.right_cancel_semigroup f mul,
   ..hf.ordered_comm_monoid f one mul }
 
 section mono
@@ -1224,7 +1223,6 @@ instance [ordered_comm_monoid α] : ordered_comm_monoid (order_dual α) :=
 instance [ordered_cancel_comm_monoid α] : ordered_cancel_comm_monoid (order_dual α) :=
 { le_of_mul_le_mul_left := λ a b c : α, le_of_mul_le_mul_left',
   mul_left_cancel := @mul_left_cancel α _,
-  mul_right_cancel := @mul_right_cancel α _,
   ..order_dual.ordered_comm_monoid }
 
 @[to_additive]
@@ -1244,8 +1242,7 @@ instance [ordered_cancel_comm_monoid M] [ordered_cancel_comm_monoid N] :
   ordered_cancel_comm_monoid (M × N) :=
 { mul_le_mul_left := λ a b h c, ⟨mul_le_mul_left' h.1 _, mul_le_mul_left' h.2 _⟩,
   le_of_mul_le_mul_left := λ a b c h, ⟨le_of_mul_le_mul_left' h.1, le_of_mul_le_mul_left' h.2⟩,
- .. prod.comm_monoid, .. prod.left_cancel_semigroup, .. prod.right_cancel_semigroup,
- .. prod.partial_order M N }
+ .. prod.cancel_comm_monoid, .. prod.partial_order M N }
 
 end prod
 
@@ -1272,13 +1269,11 @@ instance [ordered_comm_monoid α] : ordered_add_comm_monoid (additive α) :=
 
 instance [ordered_cancel_add_comm_monoid α] : ordered_cancel_comm_monoid (multiplicative α) :=
 { le_of_mul_le_mul_left := @ordered_cancel_add_comm_monoid.le_of_add_le_add_left α _,
-  ..multiplicative.right_cancel_semigroup,
   ..multiplicative.left_cancel_semigroup,
   ..multiplicative.ordered_comm_monoid }
 
 instance [ordered_cancel_comm_monoid α] : ordered_cancel_add_comm_monoid (additive α) :=
 { le_of_add_le_add_left := @ordered_cancel_comm_monoid.le_of_mul_le_mul_left α _,
-  ..additive.add_right_cancel_semigroup,
   ..additive.add_left_cancel_semigroup,
   ..additive.ordered_add_comm_monoid }
 
diff --git a/src/algebra/ordered_ring.lean b/src/algebra/ordered_ring.lean
@@ -630,7 +630,6 @@ instance ordered_ring.to_ordered_semiring : ordered_semiring α :=
 { mul_zero                   := mul_zero,
   zero_mul                   := zero_mul,
   add_left_cancel            := @add_left_cancel α _,
-  add_right_cancel           := @add_right_cancel α _,
   le_of_add_le_add_left      := @le_of_add_le_add_left α _,
   mul_lt_mul_of_pos_left     := @ordered_ring.mul_lt_mul_of_pos_left α _,
   mul_lt_mul_of_pos_right    := @ordered_ring.mul_lt_mul_of_pos_right α _,
@@ -719,7 +718,6 @@ instance linear_ordered_ring.to_linear_ordered_semiring : linear_ordered_semirin
 { mul_zero                   := mul_zero,
   zero_mul                   := zero_mul,
   add_left_cancel            := @add_left_cancel α _,
-  add_right_cancel           := @add_right_cancel α _,
   le_of_add_le_add_left      := @le_of_add_le_add_left α _,
   mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left α _,
   mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right α _,
@@ -920,7 +918,6 @@ let s : linear_ordered_semiring α := @linear_ordered_ring.to_linear_ordered_sem
 { zero_mul                   := @linear_ordered_semiring.zero_mul α s,
   mul_zero                   := @linear_ordered_semiring.mul_zero α s,
   add_left_cancel            := @linear_ordered_semiring.add_left_cancel α s,
-  add_right_cancel           := @linear_ordered_semiring.add_right_cancel α s,
   le_of_add_le_add_left      := @linear_ordered_semiring.le_of_add_le_add_left α s,
   mul_lt_mul_of_pos_left     := @linear_ordered_semiring.mul_lt_mul_of_pos_left α s,
   mul_lt_mul_of_pos_right    := @linear_ordered_semiring.mul_lt_mul_of_pos_right α s,
@@ -942,7 +939,6 @@ let s : linear_ordered_semiring α := @linear_ordered_ring.to_linear_ordered_sem
 { zero_mul                   := @linear_ordered_semiring.zero_mul α s,
   mul_zero                   := @linear_ordered_semiring.mul_zero α s,
   add_left_cancel            := @linear_ordered_semiring.add_left_cancel α s,
-  add_right_cancel           := @linear_ordered_semiring.add_right_cancel α s,
   le_of_add_le_add_left      := @linear_ordered_semiring.le_of_add_le_add_left α s,
   mul_lt_mul_of_pos_left     := @linear_ordered_semiring.mul_lt_mul_of_pos_left α s,
   mul_lt_mul_of_pos_right    := @linear_ordered_semiring.mul_lt_mul_of_pos_right α s,
diff --git a/src/algebra/punit_instances.lean b/src/algebra/punit_instances.lean
@@ -60,7 +60,6 @@ intros; trivial
 
 instance : linear_ordered_cancel_add_comm_monoid punit :=
 { add_left_cancel := λ _ _ _ _, subsingleton.elim _ _,
-  add_right_cancel := λ _ _ _ _, subsingleton.elim _ _,
   le_of_add_le_add_left := λ _ _ _ _, trivial,
   le_total := λ _ _, or.inl trivial,
   decidable_le := λ _ _, decidable.true,
diff --git a/src/data/finsupp/basic.lean b/src/data/finsupp/basic.lean
@@ -2262,21 +2262,11 @@ instance [partial_order M] [has_zero M] : partial_order (α →₀ M) :=
 { le_antisymm := λ f g hfg hgf, ext $ λ s, le_antisymm (hfg s) (hgf s),
   .. finsupp.preorder }
 
-instance [ordered_cancel_add_comm_monoid M] : add_left_cancel_semigroup (α →₀ M) :=
-{ add_left_cancel := λ a b c h, ext $ λ s,
-  by { rw ext_iff at h, exact add_left_cancel (h s) },
-  .. finsupp.add_monoid }
-
-instance [ordered_cancel_add_comm_monoid M] : add_right_cancel_semigroup (α →₀ M) :=
-{ add_right_cancel := λ a b c h, ext $ λ s,
-  by { rw ext_iff at h, exact add_right_cancel (h s) },
-  .. finsupp.add_monoid }
-
 instance [ordered_cancel_add_comm_monoid M] : ordered_cancel_add_comm_monoid (α →₀ M) :=
 { add_le_add_left := λ a b h c s, add_le_add_left (h s) (c s),
   le_of_add_le_add_left := λ a b c h s, le_of_add_le_add_left (h s),
-  .. finsupp.add_comm_monoid, .. finsupp.partial_order,
-  .. finsupp.add_left_cancel_semigroup, .. finsupp.add_right_cancel_semigroup }
+  add_left_cancel := λ a b c h, ext $ λ s, add_left_cancel (ext_iff.1 h s),
+  .. finsupp.add_comm_monoid, .. finsupp.partial_order }
 
 lemma le_def [preorder M] [has_zero M] {f g : α →₀ M} : f ≤ g ↔ ∀ x, f x ≤ g x := iff.rfl
 
diff --git a/src/data/multiset/basic.lean b/src/data/multiset/basic.lean
@@ -375,8 +375,6 @@ instance : ordered_cancel_add_comm_monoid (multiset α) :=
   zero_add              := multiset.zero_add,
   add_zero              := λ s, by rw [multiset.add_comm, multiset.zero_add],
   add_left_cancel       := multiset.add_left_cancel,
-  add_right_cancel      := λ s₁ s₂ s₃ h, multiset.add_left_cancel s₂ $
-    by simpa [multiset.add_comm] using h,
   add_le_add_left       := λ s₁ s₂ h s₃, (multiset.add_le_add_left _).2 h,
   le_of_add_le_add_left := λ s₁ s₂ s₃, (multiset.add_le_add_left _).1,
   ..@multiset.partial_order α }
diff --git a/src/data/nat/basic.lean b/src/data/nat/basic.lean
@@ -48,7 +48,6 @@ instance : comm_semiring nat :=
 
 instance : linear_ordered_semiring nat :=
 { add_left_cancel            := @nat.add_left_cancel,
-  add_right_cancel           := @nat.add_right_cancel,
   lt                         := nat.lt,
   add_le_add_left            := @nat.add_le_add_left,
   le_of_add_le_add_left      := @nat.le_of_add_le_add_left,
diff --git a/src/data/num/lemmas.lean b/src/data/num/lemmas.lean
@@ -307,7 +307,6 @@ by refine {
 
 instance : ordered_cancel_add_comm_monoid num :=
 { add_left_cancel            := by {intros a b c, transfer_rw, apply add_left_cancel},
-  add_right_cancel           := by {intros a b c, transfer_rw, apply add_right_cancel},
   lt                         := (<),
   lt_iff_le_not_le           := by {intros a b, transfer_rw, apply lt_iff_le_not_le},
   le                         := (≤),
diff --git a/src/data/pnat/basic.lean b/src/data/pnat/basic.lean
@@ -79,44 +79,33 @@ theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n := subtype.eq
 
 @[simp] lemma coe_inj {m n : ℕ+} : (m : ℕ) = n ↔ m = n := set_coe.ext_iff
 
+lemma coe_injective : function.injective (coe : ℕ+ → ℕ) := subtype.coe_injective
 
 @[simp] theorem mk_coe (n h) : ((⟨n, h⟩ : ℕ+) : ℕ) = n := rfl
 
-instance : add_comm_semigroup ℕ+ :=
-{ add       := λ a b, ⟨(a  + b : ℕ), add_pos a.pos b.pos⟩,
-  add_comm  := λ a b, subtype.eq (add_comm a b),
-  add_assoc := λ a b c, subtype.eq (add_assoc a b c) }
+instance : has_add ℕ+ := ⟨λ a b, ⟨(a  + b : ℕ), add_pos a.pos b.pos⟩⟩
+
+instance : add_comm_semigroup ℕ+ := coe_injective.add_comm_semigroup coe (λ _ _, rfl)
 
 @[simp] theorem add_coe (m n : ℕ+) : ((m + n : ℕ+) : ℕ) = m + n := rfl
 instance coe_add_hom : is_add_hom (coe : ℕ+ → ℕ) := ⟨add_coe⟩
 
 instance : add_left_cancel_semigroup ℕ+ :=
-{ add_left_cancel := λ a b c h, by {
-    replace h := congr_arg (coe : ℕ+ → ℕ) h,
-    rw [add_coe, add_coe] at h,
-    exact eq ((add_right_inj (a : ℕ)).mp h)},
-  .. (pnat.add_comm_semigroup) }
+coe_injective.add_left_cancel_semigroup coe (λ _ _, rfl)
 
 instance : add_right_cancel_semigroup ℕ+ :=
-{ add_right_cancel := λ a b c h, by {
-    replace h := congr_arg (coe : ℕ+ → ℕ) h,
-    rw [add_coe, add_coe] at h,
-    exact eq ((add_left_inj (b : ℕ)).mp h)},
-  .. (pnat.add_comm_semigroup) }
+coe_injective.add_right_cancel_semigroup coe (λ _ _, rfl)
 
 @[simp] theorem ne_zero (n : ℕ+) : (n : ℕ) ≠ 0 := ne_of_gt n.2
 
 theorem to_pnat'_coe {n : ℕ} : 0 < n → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos
 
 @[simp] theorem coe_to_pnat' (n : ℕ+) : (n : ℕ).to_pnat' = n := eq (to_pnat'_coe n.pos)
 
-instance : comm_monoid ℕ+ :=
-{ mul       := λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩,
-  mul_assoc := λ a b c, subtype.eq (mul_assoc _ _ _),
-  one       := succ_pnat 0,
-  one_mul   := λ a, subtype.eq (one_mul _),
-  mul_one   := λ a, subtype.eq (mul_one _),
-  mul_comm  := λ a b, subtype.eq (mul_comm _ _) }
+instance : has_mul ℕ+ := ⟨λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩⟩
+instance : has_one ℕ+ := ⟨succ_pnat 0⟩
+
+instance : comm_monoid ℕ+ := coe_injective.comm_monoid coe rfl (λ _ _, rfl)
 
 theorem lt_add_one_iff : ∀ {a b : ℕ+}, a < b + 1 ↔ a ≤ b :=
 λ a b, nat.lt_add_one_iff
@@ -129,7 +118,7 @@ theorem add_one_le_iff : ∀ {a b : ℕ+}, a + 1 ≤ b ↔ a < b :=
 instance : order_bot ℕ+ :=
 { bot := 1,
   bot_le := λ a, a.property,
-  ..(by apply_instance : partial_order ℕ+) }
+  .. pnat.linear_order }
 
 @[simp] lemma bot_eq_zero : (⊥ : ℕ+) = 1 := rfl
 
@@ -173,30 +162,16 @@ lemma coe_eq_one_iff {m : ℕ+} :
 by induction n with n ih;
  [refl, rw [pow_succ', pow_succ, mul_coe, mul_comm, ih]]
 
-instance : left_cancel_semigroup ℕ+ :=
-{ mul_left_cancel := λ a b c h, by {
-   replace h := congr_arg (coe : ℕ+ → ℕ) h,
-   exact eq ((nat.mul_right_inj a.pos).mp h)},
-  .. (pnat.comm_monoid) }
-
-instance : right_cancel_semigroup ℕ+ :=
-{ mul_right_cancel := λ a b c h, by {
-   replace h := congr_arg (coe : ℕ+ → ℕ) h,
-   exact eq ((nat.mul_left_inj b.pos).mp h)},
-  .. (pnat.comm_monoid) }
-
 instance : ordered_cancel_comm_monoid ℕ+ :=
 { mul_le_mul_left := by { intros, apply nat.mul_le_mul_left, assumption },
   le_of_mul_le_mul_left := by { intros a b c h, apply nat.le_of_mul_le_mul_left h a.property, },
-  .. (pnat.left_cancel_semigroup),
-  .. (pnat.right_cancel_semigroup),
-  .. (pnat.linear_order),
-  .. (pnat.comm_monoid)}
-
-instance : distrib ℕ+ :=
-{ left_distrib  := λ a b c, eq (mul_add a b c),
-  right_distrib := λ a b c, eq (add_mul a b c),
-  ..(pnat.add_comm_semigroup), ..(pnat.comm_monoid) }
+  mul_left_cancel := λ a b c h, by {
+   replace h := congr_arg (coe : ℕ+ → ℕ) h,
+   exact eq ((nat.mul_right_inj a.pos).mp h)},
+  .. pnat.comm_monoid,
+  .. pnat.linear_order }
+
+instance : distrib ℕ+ := coe_injective.distrib coe (λ _ _, rfl) (λ _ _, rfl)
 
 /-- Subtraction a - b is defined in the obvious way when
   a > b, and by a - b = 1 if a ≤ b.
diff --git a/src/data/real/nnreal.lean b/src/data/real/nnreal.lean
@@ -242,8 +242,6 @@ instance : semilattice_sup_bot ℝ≥0 :=
 instance : linear_ordered_semiring ℝ≥0 :=
 { add_left_cancel            := assume a b c h, nnreal.eq $
     @add_left_cancel ℝ _ a b c (nnreal.eq_iff.2 h),
-  add_right_cancel           := assume a b c h, nnreal.eq $
-    @add_right_cancel ℝ _ a b c (nnreal.eq_iff.2 h),
   le_of_add_le_add_left      := assume a b c, @le_of_add_le_add_left ℝ _ a b c,
   mul_lt_mul_of_pos_left     := assume a b c, @mul_lt_mul_of_pos_left ℝ _ a b c,
   mul_lt_mul_of_pos_right    := assume a b c, @mul_lt_mul_of_pos_right ℝ _ a b c,
diff --git a/src/order/filter/germ.lean b/src/order/filter/germ.lean
@@ -522,8 +522,7 @@ instance [ordered_cancel_comm_monoid β] : ordered_cancel_comm_monoid (germ l β
     H.mono $ λ x H, mul_le_mul_left' H _,
   le_of_mul_le_mul_left := λ f g h, induction_on₃ f g h $ λ f g h H,
     H.mono $ λ x, le_of_mul_le_mul_left',
-  .. germ.partial_order, .. germ.comm_monoid, .. germ.left_cancel_semigroup,
-  .. germ.right_cancel_semigroup }
+  .. germ.partial_order, .. germ.comm_monoid, .. germ.left_cancel_semigroup }
 
 @[to_additive]
 instance ordered_comm_group [ordered_comm_group β] : ordered_comm_group (germ l β) :=
