refactor(algebra/order/monoid): Remove redundant field from `ordered_…

…cancel_comm_monoid` (#16445)

`mul_left_cancel : ∀ a b c, a + b = a + c → b = c` can be inferred from `le_of_mul_le_mul_left : ∀ a b c, a + b ≤ a + c → b ≤ c` and antisymmetry.

src/algebra/order/group.lean

@@ -54,8 +54,7 @@ instance units.ordered_comm_group [ordered_comm_monoid α] : ordered_comm_group
 instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u)
   [s : ordered_comm_group α] :
   ordered_cancel_comm_monoid α :=
-{ mul_left_cancel       := λ a b c, (mul_right_inj a).mp,
-  le_of_mul_le_mul_left := λ a b c, (mul_le_mul_iff_left a).mp,
+{ le_of_mul_le_mul_left := λ a b c, (mul_le_mul_iff_left a).mp,
   ..s }
 
 @[priority 100, to_additive] -- See note [lower instance priority]
@@ -872,7 +871,6 @@ variables [linear_ordered_comm_group α] {a b c : α}
 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,
   ..‹linear_ordered_comm_group α› }
 
 /-- Pullback a `linear_ordered_comm_group` under an injective map.

src/algebra/order/monoid.lean

@@ -564,24 +564,27 @@ end canonically_linear_ordered_monoid
 /-- An ordered cancellative additive commutative monoid
 is an additive commutative monoid with a partial order,
 in which addition is cancellative and monotone. -/
-@[protect_proj, ancestor add_cancel_comm_monoid partial_order]
-class ordered_cancel_add_comm_monoid (α : Type u)
-      extends add_cancel_comm_monoid α, partial_order α :=
+@[protect_proj, ancestor add_comm_monoid partial_order]
+class ordered_cancel_add_comm_monoid (α : Type u) extends add_comm_monoid α, partial_order α :=
 (add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
 (le_of_add_le_add_left : ∀ a b c : α, a + b ≤ a + c → b ≤ c)
 
 /-- An ordered cancellative commutative monoid
 is a commutative monoid with a partial order,
 in which multiplication is cancellative and monotone. -/
-@[protect_proj, ancestor cancel_comm_monoid partial_order, to_additive]
-class ordered_cancel_comm_monoid (α : Type u)
-      extends cancel_comm_monoid α, partial_order α :=
+@[protect_proj, ancestor comm_monoid partial_order, to_additive]
+class ordered_cancel_comm_monoid (α : Type u) extends comm_monoid α, partial_order α :=
 (mul_le_mul_left       : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b)
 (le_of_mul_le_mul_left : ∀ a b c : α, a * b ≤ a * c → b ≤ c)
 
 section ordered_cancel_comm_monoid
 variables [ordered_cancel_comm_monoid α] {a b c d : α}
 
+@[priority 200, to_additive] -- see Note [lower instance priority]
+instance ordered_cancel_comm_monoid.to_contravariant_class_le_left :
+  contravariant_class α α (*) (≤) :=
+⟨ordered_cancel_comm_monoid.le_of_mul_le_mul_left⟩
+
 @[to_additive]
 lemma ordered_cancel_comm_monoid.lt_of_mul_lt_mul_left : ∀ a b c : α, a * b < a * c → b < c :=
 λ a b c h, lt_of_le_not_le
@@ -608,6 +611,12 @@ contravariant_swap_mul_lt_of_contravariant_mul_lt M
 instance ordered_cancel_comm_monoid.to_ordered_comm_monoid : ordered_comm_monoid α :=
 { ..‹ordered_cancel_comm_monoid α› }
 
+@[priority 100, to_additive] -- see Note [lower instance priority]
+instance ordered_cancel_comm_monoid.to_cancel_comm_monoid : cancel_comm_monoid α :=
+{ mul_left_cancel := λ a b c h,
+    (le_of_mul_le_mul_left' h.le).antisymm $ le_of_mul_le_mul_left' h.ge,
+  ..‹ordered_cancel_comm_monoid α› }
+
 /-- Pullback an `ordered_cancel_comm_monoid` under an injective map.
 See note [reducible non-instances]. -/
 @[reducible, to_additive function.injective.ordered_cancel_add_comm_monoid
@@ -619,7 +628,6 @@ def function.injective.ordered_cancel_comm_monoid {β : Type*}
   ordered_cancel_comm_monoid β :=
 { le_of_mul_le_mul_left := λ a b c (bc : f (a * b) ≤ f (a * c)),
     (mul_le_mul_iff_left (f a)).mp (by rwa [← mul, ← mul]),
-  ..hf.left_cancel_semigroup f mul,
   ..hf.ordered_comm_monoid f one mul npow }
 
 end ordered_cancel_comm_monoid
@@ -832,7 +840,7 @@ instance [ordered_comm_monoid α] [ordered_comm_monoid β] : ordered_comm_monoid
 instance [ordered_cancel_comm_monoid M] [ordered_cancel_comm_monoid N] :
   ordered_cancel_comm_monoid (M × N) :=
 { 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.cancel_comm_monoid, .. prod.ordered_comm_monoid }
+  .. prod.ordered_comm_monoid }
 
 @[to_additive] instance [has_le α] [has_le β] [has_mul α] [has_mul β] [has_exists_mul_of_le α]
   [has_exists_mul_of_le β] : has_exists_mul_of_le (α × β) :=
@@ -1342,12 +1350,10 @@ 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.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_left_cancel_semigroup,
   ..additive.ordered_add_comm_monoid }
 
 instance [linear_ordered_add_comm_monoid α] : linear_ordered_comm_monoid (multiplicative α) :=

src/algebra/order/positive/ring.lean

@@ -106,9 +106,7 @@ ordered cancellative commutative monoid. We don't have a typeclass for linear or
 semirings, so we assume `[linear_ordered_semiring R] [is_commutative R (*)] instead. -/
 instance [linear_ordered_semiring R] [is_commutative R (*)] [nontrivial R] :
   linear_ordered_cancel_comm_monoid {x : R // 0 < x} :=
-{ mul_left_cancel := λ a b c h, subtype.ext $ (strict_mono_mul_left_of_pos a.2).injective $
-    by convert congr_arg subtype.val h,
-  le_of_mul_le_mul_left := λ a b c h, subtype.coe_le_coe.1 $ (mul_le_mul_left a.2).1 h,
+{ le_of_mul_le_mul_left := λ a b c h, subtype.coe_le_coe.1 $ (mul_le_mul_left a.2).1 h,
   .. subtype.linear_order _,
   .. @positive.subtype.ordered_comm_monoid R
     { mul_comm := is_commutative.comm, .. ‹linear_ordered_semiring R› } _  }

src/algebra/order/ring.lean

@@ -852,13 +852,10 @@ end
 
 @[priority 100] -- see Note [lower instance priority]
 instance ordered_ring.to_ordered_semiring : ordered_semiring α :=
-{ mul_zero                   := mul_zero,
-  zero_mul                   := zero_mul,
-  add_left_cancel            := @add_left_cancel α _,
-  le_of_add_le_add_left      := @le_of_add_le_add_left α _ _ _,
+{ 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 α _,
-  ..‹ordered_ring α› }
+  ..‹ordered_ring α›, ..ring.to_semiring }
 
 -- See Note [decidable namespace]
 protected lemma decidable.mul_le_mul_of_nonpos_left [@decidable_rel α (≤)]
@@ -1024,14 +1021,7 @@ local attribute [instance] linear_ordered_ring.decidable_le linear_ordered_ring.
 
 @[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_ring.to_linear_ordered_semiring : linear_ordered_semiring α :=
-{ mul_zero                   := mul_zero,
-  zero_mul                   := zero_mul,
-  add_left_cancel            := @add_left_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 α _,
-  le_total                   := linear_ordered_ring.le_total,
-  ..‹linear_ordered_ring α› }
+{ ..‹linear_ordered_ring α›, ..ordered_ring.to_ordered_semiring }
 
 @[priority 100] -- see Note [lower instance priority]
 instance linear_ordered_ring.is_domain : is_domain α :=

src/algebra/punit_instances.lean

@@ -77,8 +77,7 @@ by refine
 intros; trivial
 
 instance : linear_ordered_cancel_add_comm_monoid punit :=
-{ add_left_cancel := λ _ _ _ _, subsingleton.elim _ _,
-  le_of_add_le_add_left := λ _ _ _ _, trivial,
+{ le_of_add_le_add_left := λ _ _ _ _, trivial,
   .. punit.canonically_ordered_add_monoid, ..punit.linear_order }
 
 instance : has_smul R punit :=

src/data/dfinsupp/order.lean

@@ -111,11 +111,6 @@ instance (α : ι → Type*) [Π i, ordered_cancel_add_comm_monoid (α i)] :
     rw [add_apply, add_apply] at H,
     exact le_of_add_le_add_left H,
   end,
-  add_left_cancel := λ f g h H, ext $ λ i, begin
-    refine add_left_cancel _,
-    exact f i,
-    rw [←add_apply, ←add_apply, H],
-  end,
   .. dfinsupp.ordered_add_comm_monoid α }
 
 instance [Π i, ordered_add_comm_monoid (α i)] [Π i, contravariant_class (α i) (α i) (+) (≤)] :

src/data/finsupp/order.lean

@@ -96,7 +96,6 @@ instance [ordered_add_comm_monoid α] : ordered_add_comm_monoid (ι →₀ α) :
 
 instance [ordered_cancel_add_comm_monoid α] : ordered_cancel_add_comm_monoid (ι →₀ α) :=
 { le_of_add_le_add_left := λ f g i h s, le_of_add_le_add_left (h s),
-  add_left_cancel := λ f g i h, ext $ λ s, add_left_cancel (ext_iff.1 h s),
   .. finsupp.ordered_add_comm_monoid }
 
 instance [ordered_add_comm_monoid α] [contravariant_class α α (+) (≤)] :

src/data/multiset/basic.lean

@@ -428,7 +428,6 @@ instance : ordered_cancel_add_comm_monoid (multiset α) :=
     congr_arg coe $ append_assoc l₁ l₂ l₃,
   zero_add              := λ s, quot.induction_on s $ λ l, rfl,
   add_zero              := λ s, quotient.induction_on s $ λ l, congr_arg coe $ append_nil l,
-  add_left_cancel       := λ a b c, add_left_cancel'',
   add_le_add_left       := λ s₁ s₂, add_le_add_left,
   le_of_add_le_add_left := λ s₁ s₂ s₃, le_of_add_le_add_left,
   ..@multiset.partial_order α }

src/data/nat/basic.lean

@@ -54,8 +54,7 @@ instance : comm_semiring ℕ :=
     by rw [nat.succ_eq_add_one, nat.add_comm, nat.right_distrib, nat.one_mul] }
 
 instance : linear_ordered_semiring nat :=
-{ add_left_cancel            := @nat.add_left_cancel,
-  lt                         := nat.lt,
+{ 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,
   zero_le_one                := nat.le_of_lt (nat.zero_lt_succ 0),
@@ -66,9 +65,7 @@ instance : linear_ordered_semiring nat :=
   ..nat.comm_semiring, ..nat.linear_order }
 
 -- all the fields are already included in the linear_ordered_semiring instance
-instance : linear_ordered_cancel_add_comm_monoid ℕ :=
-{ add_left_cancel := @nat.add_left_cancel,
-  ..nat.linear_ordered_semiring }
+instance : linear_ordered_cancel_add_comm_monoid ℕ := { ..nat.linear_ordered_semiring }
 
 instance : linear_ordered_comm_monoid_with_zero ℕ :=
 { mul_le_mul_left := λ a b h c, nat.mul_le_mul_left c h,

src/data/num/lemmas.lean

@@ -320,8 +320,7 @@ try { intros, refl }; try { transfer };
 simp [add_comm, mul_add, add_mul, mul_assoc, mul_comm, mul_left_comm]
 
 instance : ordered_cancel_add_comm_monoid num :=
-{ add_left_cancel            := by {intros a b c, transfer_rw, apply add_left_cancel},
-  lt                         := (<),
+{ lt                         := (<),
   lt_iff_le_not_le           := by {intros a b, transfer_rw, apply lt_iff_le_not_le},
   le                         := (≤),
   le_refl                    := by transfer,

src/number_theory/bertrand.lean

@@ -68,7 +68,7 @@ begin
       (convex_Ioi 0.5)).add ((strict_concave_on_sqrt_mul_log_Ioi.concave_on.comp_linear_map
       ((2 : ℝ) • linear_map.id)).subset
       (λ a ha, lt_of_eq_of_lt _ ((mul_lt_mul_left two_pos).mpr ha)) (convex_Ioi 0.5))).sub
-      ((convex_on_id (convex_Ioi 0.5)).smul (div_nonneg (log_nonneg _) _)); norm_num1 },
+      ((convex_on_id (convex_Ioi (0.5 : ℝ))).smul (div_nonneg (log_nonneg _) _)); norm_num1 },
   suffices : ∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0,
   { obtain ⟨x1, x2, h1, h2, h0, h3, h4⟩ := this,
     exact (h.right_le_of_le_left'' h1 ((h1.trans h2).trans_le h0) h2 h0 (h4.trans h3)).trans h4 },

src/order/filter/germ.lean

@@ -537,7 +537,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.partial_order, .. germ.comm_monoid }
 
 @[to_additive]
 instance ordered_comm_group [ordered_comm_group β] : ordered_comm_group (germ l β) :=

src/set_theory/ordinal/natural_ops.lean

@@ -261,7 +261,6 @@ instance add_contravariant_class_le :
 instance : ordered_cancel_add_comm_monoid nat_ordinal :=
 { add := (+),
   add_assoc := nadd_assoc,
-  add_left_cancel := λ a b c, add_left_cancel'',
   add_le_add_left := λ a b, add_le_add_left,
   le_of_add_le_add_left := λ a b c, le_of_add_le_add_left,
   zero := 0,