refactor(algebra/order/monoid): Split field of canonically_ordered_... (#14556)

Replace
```
(le_iff_exists_add : ∀ a b : α, a ≤ b ↔ ∃ c, b = a + c)
```
by
```
(exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ c, b = a + c)
(le_self_add : ∀ a b : α, a ≤ a + b)
```
This makes our life easier because
* We can use existing `has_exists_add_of_le` instances to complete the `exists_add_of_le` field, and detect the missing ones.
* No need to substitute `b = a + c` every time.

Author: YaelDillies

counterexamples/canonically_ordered_comm_semiring_two_mul.lean

@@ -209,37 +209,24 @@ begin
     exact nat.succ_pos _ }
 end
 
-instance order_bot : order_bot L :=
-{ bot := 0,
-  bot_le := bot_le,
-  ..(infer_instance : partial_order L) }
+instance order_bot : order_bot L := ⟨0, bot_le⟩
 
-lemma le_iff_exists_add : ∀ (a b : L), a ≤ b ↔ ∃ (c : L), b = a + c :=
+lemma exists_add_of_le : ∀ a b : L, a ≤ b → ∃ c, b = a + c :=
 begin
-  rintros ⟨⟨an, a2⟩, ha⟩ ⟨⟨bn, b2⟩, hb⟩,
-  rw subtype.mk_le_mk,
-  refine ⟨λ h, _, λ h, _⟩,
-  { rcases h with ⟨rfl, rfl⟩ | h,
-    { exact ⟨(0 : L), (add_zero _).symm⟩ },
-    { refine ⟨⟨⟨bn - an, b2 + a2⟩, _⟩, _⟩,
-      { rw [ne.def, prod.mk.inj_iff, not_and_distrib],
-        exact or.inl (ne_of_gt (tsub_pos_of_lt h)) },
-      { congr,
-        { exact (add_tsub_cancel_of_le h.le).symm },
-        { change b2 = a2 + (b2 + a2),
-          rw [add_comm b2, ← add_assoc, add_self_zmod_2, zero_add] } } } },
-  { rcases h with ⟨⟨⟨c, c2⟩, hc⟩, abc⟩,
-    injection abc with abc,
-    rw [prod.mk_add_mk, prod.mk.inj_iff] at abc,
-    rcases abc with ⟨rfl, rfl⟩,
-    cases c,
-    { refine or.inl _,
-      rw [ne.def, prod.mk.inj_iff, eq_self_iff_true, true_and] at hc,
-      rcases mem_zmod_2 c2 with rfl | rfl,
-      { rw [add_zero, add_zero] },
-      { exact (hc rfl).elim } },
-    { refine or.inr _,
-      exact (lt_add_iff_pos_right _).mpr c.succ_pos } }
+  rintro a ⟨b, _⟩ (⟨rfl, rfl⟩ | h),
+  { exact ⟨0, (add_zero _).symm⟩ },
+  { exact ⟨⟨b - a.1, λ H, (tsub_pos_of_lt h).ne' (prod.mk.inj_iff.1 H).1⟩,
+      subtype.ext $ prod.ext (add_tsub_cancel_of_le h.le).symm (add_sub_cancel'_right _ _).symm⟩ }
+end
+
+lemma le_self_add : ∀ a b : L, a ≤ a + b :=
+begin
+  rintro a ⟨⟨bn, b2⟩, hb⟩,
+  obtain rfl | h := nat.eq_zero_or_pos bn,
+  { obtain rfl | rfl := mem_zmod_2 b2,
+    { exact or.inl (prod.ext (add_zero _).symm (add_zero _).symm) },
+    { exact (hb rfl).elim } },
+  { exact or.inr ((lt_add_iff_pos_right _).mpr h) }
 end
 
 lemma eq_zero_or_eq_zero_of_mul_eq_zero : ∀ (a b : L), a * b = 0 → a = 0 ∨ b = 0 :=
@@ -260,7 +247,8 @@ begin
 end
 
 instance can : canonically_ordered_comm_semiring L :=
-{ le_iff_exists_add := le_iff_exists_add,
+{ exists_add_of_le := exists_add_of_le,
+  le_self_add := le_self_add,
   eq_zero_or_eq_zero_of_mul_eq_zero := eq_zero_or_eq_zero_of_mul_eq_zero,
   ..(infer_instance : order_bot L),
   ..(infer_instance : ordered_comm_semiring L) }

src/algebra/associated.lean

@@ -847,7 +847,8 @@ instance : cancel_comm_monoid_with_zero (associates α) :=
   .. (infer_instance : comm_monoid_with_zero (associates α)) }
 
 instance : canonically_ordered_monoid (associates α) :=
-{ le_iff_exists_mul := λ a b, iff.rfl,
+{ exists_mul_of_le := λ a b, id,
+  le_self_mul := λ a b, ⟨b, rfl⟩,
   ..associates.cancel_comm_monoid_with_zero,
   ..associates.bounded_order,
   ..associates.ordered_comm_monoid}

src/algebra/lie/subalgebra.lean

@@ -381,7 +381,8 @@ instance : add_comm_monoid (lie_subalgebra R L) :=
 /-- This is not an instance, as it would stop `⊥` being the simp-normal form (via `bot_eq_zero`). -/
 def canonically_ordered_add_monoid : canonically_ordered_add_monoid (lie_subalgebra R L) :=
 { add_le_add_left := λ a b, sup_le_sup_left,
-  le_iff_exists_add := λ a b, le_iff_exists_sup,
+  exists_add_of_le := λ a b h, ⟨b, (sup_eq_right.2 h).symm⟩,
+  le_self_add := λ a b, le_sup_left,
   ..lie_subalgebra.add_comm_monoid,
   ..lie_subalgebra.complete_lattice }
 

src/algebra/module/submodule/pointwise.lean

@@ -148,7 +148,8 @@ def canonically_ordered_add_monoid : canonically_ordered_add_monoid (submodule R
   bot := ⊥,
   add := (+),
   add_le_add_left := λ a b, sup_le_sup_left,
-  le_iff_exists_add := λ a b, le_iff_exists_sup,
+  exists_add_of_le := λ a b h, ⟨b, (sup_eq_right.2 h).symm⟩,
+  le_self_add := λ a b, le_sup_left,
   ..submodule.pointwise_add_comm_monoid,
   ..submodule.complete_lattice }
 

src/algebra/order/monoid.lean

@@ -275,7 +275,7 @@ lemma lt_of_mul_lt_mul_left {α : Type u} [has_mul α] [partial_order α]
   ∀ (a b c : with_zero α), a * b < a * c → b < c :=
 begin
   rintro (_ | a) (_ | b) (_ | c) h;
-  try { exact false.elim (lt_irrefl none h) },
+  try { exact false.elim (lt_irrefl _ h) },
   { exact with_zero.zero_lt_coe c },
   { exact false.elim (not_le_of_lt h (with_zero.zero_le _)) },
   { simp_rw [some_eq_coe] at h ⊢,
@@ -340,7 +340,8 @@ end with_zero
 @[protect_proj, ancestor ordered_add_comm_monoid has_bot]
 class canonically_ordered_add_monoid (α : Type*) extends ordered_add_comm_monoid α, has_bot α :=
 (bot_le : ∀ x : α, ⊥ ≤ x)
-(le_iff_exists_add : ∀ a b : α, a ≤ b ↔ ∃ c, b = a + c)
+(exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ c, b = a + c)
+(le_self_add : ∀ a b : α, a ≤ a + b)
 
 @[priority 100]  -- see Note [lower instance priority]
 instance canonically_ordered_add_monoid.to_order_bot (α : Type u)
@@ -359,32 +360,36 @@ instance canonically_ordered_add_monoid.to_order_bot (α : Type u)
 @[protect_proj, ancestor ordered_comm_monoid has_bot, to_additive]
 class canonically_ordered_monoid (α : Type*) extends ordered_comm_monoid α, has_bot α :=
 (bot_le : ∀ x : α, ⊥ ≤ x)
-(le_iff_exists_mul : ∀ a b : α, a ≤ b ↔ ∃ c, b = a * c)
+(exists_mul_of_le : ∀ {a b : α}, a ≤ b → ∃ c, b = a * c)
+(le_self_mul : ∀ a b : α, a ≤ a * b)
 
 @[priority 100, to_additive]  -- see Note [lower instance priority]
 instance canonically_ordered_monoid.to_order_bot (α : Type u)
   [h : canonically_ordered_monoid α] : order_bot α :=
 { ..h }
 
+@[priority 100, to_additive]  -- see Note [lower instance priority]
+instance canonically_ordered_monoid.has_exists_mul_of_le (α : Type u)
+  [h : canonically_ordered_monoid α] : has_exists_mul_of_le α :=
+{ ..h }
+
 section canonically_ordered_monoid
 
 variables [canonically_ordered_monoid α] {a b c d : α}
 
-@[to_additive]
-lemma le_iff_exists_mul : a ≤ b ↔ ∃c, b = a * c :=
-canonically_ordered_monoid.le_iff_exists_mul a b
+@[to_additive] lemma le_self_mul : a ≤ a * c := canonically_ordered_monoid.le_self_mul _ _
+@[to_additive] lemma le_mul_self : a ≤ b * a := by { rw mul_comm, exact le_self_mul }
 
-@[to_additive]
-lemma le_iff_exists_mul' : a ≤ b ↔ ∃c, b = c * a :=
-by simpa only [mul_comm _ a] using le_iff_exists_mul
+@[to_additive] lemma self_le_mul_right (a b : α) : a ≤ a * b := le_self_mul
+@[to_additive] lemma self_le_mul_left (a b : α) : a ≤ b * a := le_mul_self
 
 @[to_additive]
-lemma self_le_mul_right (a b : α) : a ≤ a * b :=
-le_iff_exists_mul.mpr ⟨b, rfl⟩
+lemma le_iff_exists_mul : a ≤ b ↔ ∃ c, b = a * c :=
+⟨exists_mul_of_le, by { rintro ⟨c, rfl⟩, exact le_self_mul }⟩
 
 @[to_additive]
-lemma self_le_mul_left (a b : α) : a ≤ b * a :=
-by { rw [mul_comm], exact self_le_mul_right a b }
+lemma le_iff_exists_mul' : a ≤ b ↔ ∃ c, b = c * a :=
+by simpa only [mul_comm _ a] using le_iff_exists_mul
 
 @[simp, to_additive zero_le] lemma one_le (a : α) : 1 ≤ a :=
 le_iff_exists_mul.mpr ⟨a, (one_mul _).symm⟩
@@ -418,16 +423,10 @@ end
 calc a = 1 * a : by simp
   ... ≤ b * c : mul_le_mul' (one_le _) h
 
-@[to_additive] lemma le_mul_self : a ≤ b * a :=
-le_mul_left (le_refl a)
-
 @[to_additive] lemma le_mul_right (h : a ≤ b) : a ≤ b * c :=
 calc a = a * 1 : by simp
   ... ≤ b * c : mul_le_mul' h (one_le _)
 
-@[to_additive] lemma le_self_mul : a ≤ a * c :=
-le_mul_right (le_refl a)
-
 @[to_additive]
 lemma lt_iff_exists_mul [covariant_class α α (*) (<)] : a < b ↔ ∃ c > 1, b = a * c :=
 begin
@@ -439,35 +438,31 @@ begin
   { rw [← (self_le_mul_right a c).lt_iff_ne], apply lt_mul_of_one_lt_right' }
 end
 
+instance with_zero.has_exists_add_of_le {α} [has_add α] [preorder α] [has_exists_add_of_le α] :
+  has_exists_add_of_le (with_zero α) :=
+⟨λ a b, begin
+  apply with_zero.cases_on a,
+  { exact λ _, ⟨b, (zero_add b).symm⟩ },
+  apply with_zero.cases_on b,
+  { exact λ b' h, (with_bot.not_coe_le_bot _ h).elim },
+  rintro a' b' h,
+  obtain ⟨c, rfl⟩ := exists_add_of_le (with_zero.coe_le_coe.1 h),
+  exact ⟨c, rfl⟩,
+end⟩
+
 -- This instance looks absurd: a monoid already has a zero
 /-- Adding a new zero to a canonically ordered additive monoid produces another one. -/
 instance with_zero.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :
   canonically_ordered_add_monoid (with_zero α) :=
-{ le_iff_exists_add := λ a b, begin
+{ le_self_add := λ a b, begin
     apply with_zero.cases_on a,
-    { exact iff_of_true bot_le ⟨b, (zero_add b).symm⟩ },
+    { exact bot_le },
     apply with_zero.cases_on b,
-    { intro b',
-      refine iff_of_false (mt (le_antisymm bot_le) (by simp)) (not_exists.mpr (λ c, _)),
-      apply with_zero.cases_on c;
-      simp [←with_zero.coe_add] },
-    { simp only [le_iff_exists_add, with_zero.coe_le_coe],
-      intros,
-      split; rintro ⟨c, h⟩,
-      { exact ⟨c, congr_arg coe h⟩ },
-      { induction c using with_zero.cases_on,
-        { refine ⟨0, _⟩,
-          simpa using h },
-        { refine ⟨c, _⟩,
-          simpa [←with_zero.coe_add] using h } } }
+    { exact λ b', le_rfl },
+    { exact λ a' b', with_zero.coe_le_coe.2 le_self_add }
   end,
   .. with_zero.order_bot,
-  .. with_zero.ordered_add_comm_monoid zero_le }
-
-@[priority 100, to_additive]
-instance canonically_ordered_monoid.has_exists_mul_of_le (α : Type u)
-  [canonically_ordered_monoid α] : has_exists_mul_of_le α :=
-{ exists_mul_of_le := λ a b hab, le_iff_exists_mul.mp hab }
+  .. with_zero.ordered_add_comm_monoid zero_le, ..with_zero.has_exists_add_of_le }
 
 end canonically_ordered_monoid
 
@@ -817,9 +812,8 @@ instance [ordered_cancel_comm_monoid M] [ordered_cancel_comm_monoid N] :
 
 @[to_additive] instance [canonically_ordered_monoid α] [canonically_ordered_monoid β] :
   canonically_ordered_monoid (α × β) :=
-{ le_iff_exists_mul := λ a b,
-    ⟨exists_mul_of_le, by { rintro ⟨c, rfl⟩, exact ⟨le_self_mul, le_self_mul⟩ }⟩,
-  .. prod.ordered_comm_monoid, .. prod.order_bot _ _ }
+{ le_self_mul := λ a b, ⟨le_self_mul, le_self_mul⟩,
+  ..prod.ordered_comm_monoid, ..prod.order_bot _ _, ..prod.has_exists_mul_of_le }
 
 end prod
 
@@ -1050,23 +1044,25 @@ instance [linear_ordered_add_comm_monoid α] :
   ..with_top.ordered_add_comm_monoid,
   ..option.nontrivial }
 
-instance [canonically_ordered_add_monoid α] : canonically_ordered_add_monoid (with_top α) :=
-{ le_iff_exists_add := assume a b,
-  match a, b with
+instance [has_le α] [has_add α] [has_exists_add_of_le α] : has_exists_add_of_le (with_top α) :=
+⟨λ a b, match a, b with
   | ⊤, ⊤ := by simp
-  | (a : α), ⊤ := by { simp only [true_iff, le_top], refine ⟨⊤, _⟩, refl }
-  | (a : α), (b : α) := begin
-      rw [with_top.coe_le_coe, le_iff_exists_add],
-      split,
-      { rintro ⟨c, rfl⟩,
-        refine ⟨c, _⟩, norm_cast },
-      { intro h,
-        exact match b, h with _, ⟨some c, rfl⟩ := ⟨_, rfl⟩ end }
+  | (a : α), ⊤ := λ _, ⟨⊤, rfl⟩
+  | (a : α), (b : α) := λ h, begin
+      obtain ⟨c, rfl⟩ := exists_add_of_le (with_top.coe_le_coe.1 h),
+      exact ⟨c, rfl⟩
     end
-  | ⊤, (b : α) := by simp
+  | ⊤, (b : α) := λ h, (not_top_le_coe _ h).elim
+end⟩
+
+instance [canonically_ordered_add_monoid α] : canonically_ordered_add_monoid (with_top α) :=
+{ le_self_add := λ a b, match a, b with
+  | ⊤, ⊤ := le_rfl
+  | (a : α), ⊤ := le_top
+  | (a : α), (b : α) := with_top.coe_le_coe.2 le_self_add
+  | ⊤, (b : α) := le_rfl
   end,
-  .. with_top.order_bot,
-  .. with_top.ordered_add_comm_monoid }
+  ..with_top.order_bot, ..with_top.ordered_add_comm_monoid, ..with_top.has_exists_add_of_le }
 
 instance [canonically_linear_ordered_add_monoid α] :
   canonically_linear_ordered_add_monoid (with_top α) :=
@@ -1287,12 +1283,13 @@ instance [has_mul α] [has_le α] [has_exists_mul_of_le α] : has_exists_add_of_
 ⟨@exists_mul_of_le α _ _ _⟩
 
 instance [canonically_ordered_add_monoid α] : canonically_ordered_monoid (multiplicative α) :=
-{ le_iff_exists_mul := @le_iff_exists_add α _,
-  ..multiplicative.ordered_comm_monoid, ..multiplicative.order_bot }
+{ le_self_mul := @le_self_add α _,
+  ..multiplicative.ordered_comm_monoid, ..multiplicative.order_bot,
+  ..multiplicative.has_exists_mul_of_le }
 
 instance [canonically_ordered_monoid α] : canonically_ordered_add_monoid (additive α) :=
-{ le_iff_exists_add := @le_iff_exists_mul α _,
-  ..additive.ordered_add_comm_monoid, ..additive.order_bot }
+{ le_self_add := @le_self_mul α _,
+  ..additive.ordered_add_comm_monoid, ..additive.order_bot, ..additive.has_exists_add_of_le }
 
 instance [canonically_linear_ordered_add_monoid α] :
   canonically_linear_ordered_monoid (multiplicative α) :=

src/algebra/order/nonneg.lean

@@ -251,8 +251,9 @@ rfl
 
 instance canonically_ordered_add_monoid [ordered_ring α] :
   canonically_ordered_add_monoid {x : α // 0 ≤ x} :=
-{ le_iff_exists_add     := λ ⟨a, ha⟩ ⟨b, hb⟩,
-    by simpa only [mk_add_mk, subtype.exists, subtype.mk_eq_mk] using le_iff_exists_nonneg_add a b,
+{ le_self_add := λ a b, le_add_of_nonneg_right b.2,
+  exists_add_of_le := λ a b h,
+    ⟨⟨b - a, sub_nonneg_of_le h⟩, subtype.ext (add_sub_cancel'_right _ _).symm⟩,
   ..nonneg.ordered_add_comm_monoid,
   ..nonneg.order_bot }
 

src/algebra/order/pi.lean

@@ -38,8 +38,8 @@ instance ordered_comm_monoid {ι : Type*} {Z : ι → Type*} [∀ i, ordered_com
   a canonically ordered additive monoid."]
 instance {ι : Type*} {Z : ι → Type*} [∀ i, canonically_ordered_monoid (Z i)] :
   canonically_ordered_monoid (Π i, Z i) :=
-{ le_iff_exists_mul := λ f g, ⟨exists_mul_of_le, by { rintro ⟨h, rfl⟩, exact λ i, le_self_mul }⟩,
-  ..pi.order_bot, ..pi.ordered_comm_monoid }
+{ le_self_mul := λ f g i, le_self_mul,
+  ..pi.order_bot, ..pi.ordered_comm_monoid, ..pi.has_exists_mul_of_le }
 
 @[to_additive]
 instance ordered_cancel_comm_monoid [∀ i, ordered_cancel_comm_monoid $ f i] :

src/algebra/punit_instances.lean

@@ -99,7 +99,7 @@ intros; trivial <|> simp only [eq_iff_true_of_subsingleton]
 
 instance : canonically_ordered_add_monoid punit :=
 by refine
-{ le_iff_exists_add := λ _ _, iff_of_true _ ⟨star, subsingleton.elim _ _⟩,
+{ exists_add_of_le := λ _ _ _, ⟨star, subsingleton.elim _ _⟩,
   .. punit.comm_ring, .. punit.complete_boolean_algebra, .. };
 intros; trivial
 

src/data/dfinsupp/order.lean

@@ -177,15 +177,9 @@ instance : has_ordered_sub (Π₀ i, α i) :=
 ⟨λ n m k, forall_congr $ λ i, by { rw [add_apply, tsub_apply], exact tsub_le_iff_right }⟩
 
 instance : canonically_ordered_add_monoid (Π₀ i, α i) :=
-{ le_iff_exists_add := λ f g, begin
-      refine ⟨λ h, ⟨g - f, _⟩, _⟩,
-      { ext i,
-        rw [add_apply, tsub_apply],
-        exact (add_tsub_cancel_of_le $ h i).symm },
-      { rintro ⟨g, rfl⟩ i,
-        rw add_apply,
-        exact self_le_add_right (f i) (g i) }
-    end,
+{ exists_add_of_le := λ f g h, ⟨g - f,
+    by { ext i, rw [add_apply, tsub_apply], exact (add_tsub_cancel_of_le $ h i).symm }⟩,
+  le_self_add := λ f g i, by { rw add_apply, exact le_self_add },
  .. dfinsupp.order_bot α,
  .. dfinsupp.ordered_add_comm_monoid α }
 

src/data/finsupp/order.lean

@@ -136,13 +136,8 @@ instance tsub : has_sub (ι →₀ α) := ⟨zip_with (λ m n, m - n) (tsub_self
 instance : has_ordered_sub (ι →₀ α) := ⟨λ n m k, forall_congr $ λ x, tsub_le_iff_right⟩
 
 instance : canonically_ordered_add_monoid (ι →₀ α) :=
-{ le_iff_exists_add := λ f g, begin
-      refine ⟨λ h, ⟨g - f, _⟩, _⟩,
-      { ext x,
-        exact (add_tsub_cancel_of_le $ h x).symm },
-      { rintro ⟨g, rfl⟩ x,
-        exact self_le_add_right (f x) (g x) }
-    end,
+{ exists_add_of_le := λ f g h, ⟨g - f, ext $ λ x, (add_tsub_cancel_of_le $ h x).symm⟩,
+  le_self_add := λ f g x, le_self_add,
  .. finsupp.order_bot,
  .. finsupp.ordered_add_comm_monoid }