feat(data/set/intervals/image_preimage, algebra/ordered_monoid): new typeclass for interval bijection lemmas (#6629)

This commit introduces a ``has_exists_add_of_le`` typeclass extending ``ordered_add_comm_monoid``; is the assumption needed so that additively translating an interval gives a bijection. We then prove this fact for all flavours of interval. 

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Correct.20setting.20for.20positive.20shifts.20of.20intervals

Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: apnelson1

src/algebra/ordered_group.lean

@@ -15,7 +15,6 @@ This file develops the basics of ordered groups.
 Unfortunately, the number of `'` appended to lemmas in this file
 may differ between the multiplicative and the additive version of a lemma.
 The reason is that we did not want to change existing names in the library.
-
 -/
 
 set_option old_structure_cmd true
@@ -71,12 +70,19 @@ begin simp [inv_mul_cancel_left] at this, assumption end
 
 @[priority 100, to_additive]    -- see Note [lower instance priority]
 instance ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u)
-  [s : ordered_comm_group α] : ordered_cancel_comm_monoid α :=
+  [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 }
 
+@[priority 100, to_additive]
+instance ordered_comm_group.has_exists_mul_of_le (α : Type u)
+  [ordered_comm_group α] :
+  has_exists_mul_of_le α :=
+⟨λ a b hab, ⟨b * a⁻¹, (mul_inv_cancel_comm_assoc a b).symm⟩⟩
+
 @[to_additive neg_le_neg]
 lemma inv_le_inv' (h : a ≤ b) : b⁻¹ ≤ a⁻¹ :=
 have 1 ≤ a⁻¹ * b,           from mul_left_inv a ▸ mul_le_mul_left' h _,

src/algebra/ordered_monoid.lean

@@ -19,7 +19,6 @@ This file develops the basics of ordered monoids.
 Unfortunately, the number of `'` appended to lemmas in this file
 may differ between the multiplicative and the additive version of a lemma.
 The reason is that we did not want to change existing names in the library.
-
 -/
 
 set_option old_structure_cmd true
@@ -42,13 +41,32 @@ class ordered_comm_monoid (α : Type*) extends comm_monoid α, partial_order α
   * `a ≤ b → c + a ≤ c + b` (addition is monotone)
   * `a + b < a + c → b < c`.
 -/
+
 @[protect_proj, ancestor add_comm_monoid partial_order]
 class ordered_add_comm_monoid (α : Type*) extends add_comm_monoid α, partial_order α :=
 (add_le_add_left       : ∀ a b : α, a ≤ b → ∀ c : α, c + a ≤ c + b)
 (lt_of_add_lt_add_left : ∀ a b c : α, a + b < a + c → b < c)
 
 attribute [to_additive] ordered_comm_monoid
 
+/-- An `ordered_comm_monoid` with one-sided 'division' in the sense that
+if `a ≤ b`, there is some `c` for which `a * c = b`. This is a weaker version
+of the condition on canonical orderings defined by `canonically_ordered_monoid`. -/
+class has_exists_mul_of_le (α : Type u) [ordered_comm_monoid α] : Prop :=
+(exists_mul_of_le : ∀ {a b : α}, a ≤ b → ∃ (c : α), b = a * c)
+
+export has_exists_mul_of_le (exists_mul_of_le)
+
+/-- An `ordered_add_comm_monoid` with one-sided 'subtraction' in the sense that
+if `a ≤ b`, then there is some `c` for which `a + c = b`. This is a weaker version
+of the condition on canonical orderings defined by `canonically_ordered_add_monoid`. -/
+class has_exists_add_of_le (α : Type u) [ordered_add_comm_monoid α] : Prop :=
+(exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ (c : α), b = a + c)
+
+export has_exists_add_of_le (exists_add_of_le)
+
+attribute [to_additive] has_exists_mul_of_le
+
 /-- A linearly ordered additive commutative monoid. -/
 @[protect_proj, ancestor linear_order ordered_add_comm_monoid]
 class linear_ordered_add_comm_monoid (α : Type*)
@@ -795,6 +813,11 @@ instance with_top.canonically_ordered_add_monoid {α : Type u} [canonically_orde
   .. with_top.order_bot,
   .. with_top.ordered_add_comm_monoid }
 
+@[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 }
+
 end canonically_ordered_monoid
 
 /-- A canonically linear-ordered additive monoid is a canonically ordered additive monoid

src/data/set/intervals/image_preimage.lean

@@ -14,12 +14,82 @@ In this file we prove a bunch of trivial lemmas like “if we add `a` to all poi
 then we get `[a + b, a + c]`”. For the functions `x ↦ x ± a`, `x ↦ a ± x`, and `x ↦ -x` we prove
 lemmas about preimages and images of all intervals. We also prove a few lemmas about images under
 `x ↦ a * x`, `x ↦ x * a` and `x ↦ x⁻¹`.
-
 -/
 
 universe u
 
 namespace set
+
+section has_exists_add_of_le
+/-!
+The lemmas in this section state that addition maps intervals bijectively. The typeclass
+`has_exists_add_of_le` is defined specifically to make them work when combined with
+`ordered_cancel_add_comm_monoid`; the lemmas below therefore apply to all
+`ordered_add_comm_group`, but also to `ℕ` and `ℝ≥0`, which are not groups.
+
+TODO : move as much as possible in this file to the setting of this weaker typeclass.
+-/
+
+variables {α : Type u} [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] (a b d : α)
+
+lemma Icc_add_bij : bij_on (+d) (Icc a b) (Icc (a + d) (b + d)) :=
+begin
+  refine ⟨λ _ h, ⟨add_le_add_right h.1 _, add_le_add_right h.2 _⟩,
+          λ _ _ _ _ h, add_right_cancel h,
+          λ _ h, _⟩,
+  obtain ⟨c, rfl⟩ := exists_add_of_le h.1,
+  rw [mem_Icc, add_right_comm, add_le_add_iff_right, add_le_add_iff_right] at h,
+  exact ⟨a + c, h, by rw add_right_comm⟩,
+end
+
+lemma Ioo_add_bij : bij_on (+d) (Ioo a b) (Ioo (a + d) (b + d)) :=
+begin
+  refine ⟨λ _ h, ⟨add_lt_add_right h.1 _, add_lt_add_right h.2 _⟩,
+          λ _ _ _ _ h, add_right_cancel h,
+          λ _ h, _⟩,
+  obtain ⟨c, rfl⟩ := exists_add_of_le h.1.le,
+  rw [mem_Ioo, add_right_comm, add_lt_add_iff_right, add_lt_add_iff_right] at h,
+  exact ⟨a + c, h, by rw add_right_comm⟩,
+end
+
+lemma Ioc_add_bij : bij_on (+d) (Ioc a b) (Ioc (a + d) (b + d)) :=
+begin
+  refine ⟨λ _ h, ⟨add_lt_add_right h.1 _, add_le_add_right h.2 _⟩,
+          λ _ _ _ _ h, add_right_cancel h,
+          λ _ h, _⟩,
+  obtain ⟨c, rfl⟩ := exists_add_of_le h.1.le,
+  rw [mem_Ioc, add_right_comm, add_lt_add_iff_right, add_le_add_iff_right] at h,
+  exact ⟨a + c, h, by rw add_right_comm⟩,
+end
+
+lemma Ico_add_bij : bij_on (+d) (Ico a b) (Ico (a + d) (b + d)) :=
+begin
+  refine ⟨λ _ h, ⟨add_le_add_right h.1 _, add_lt_add_right h.2 _⟩,
+          λ _ _ _ _ h, add_right_cancel h,
+          λ _ h, _⟩,
+  obtain ⟨c, rfl⟩ := exists_add_of_le h.1,
+  rw [mem_Ico, add_right_comm, add_le_add_iff_right, add_lt_add_iff_right] at h,
+  exact ⟨a + c, h, by rw add_right_comm⟩,
+end
+
+lemma Ici_add_bij : bij_on (+d) (Ici a) (Ici (a + d)) :=
+begin
+  refine ⟨λ x h, add_le_add_right (mem_Ici.mp h) _, λ _ _ _ _ h, add_right_cancel h, λ _ h, _⟩,
+  obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ici.mp h),
+  rw [mem_Ici, add_right_comm, add_le_add_iff_right] at h,
+  exact ⟨a + c, h, by rw add_right_comm⟩,
+end
+
+lemma Ioi_add_bij : bij_on (+d) (Ioi a) (Ioi (a + d)) :=
+begin
+  refine ⟨λ x h, add_lt_add_right (mem_Ioi.mp h) _, λ _ _ _ _ h, add_right_cancel h, λ _ h, _⟩,
+  obtain ⟨c, rfl⟩ := exists_add_of_le (mem_Ioi.mp h).le,
+  rw [mem_Ioi, add_right_comm, add_lt_add_iff_right] at h,
+  exact ⟨a + c, h, by rw add_right_comm⟩,
+end
+
+end has_exists_add_of_le
+
 section ordered_add_comm_group
 
 variables {G : Type u} [ordered_add_comm_group G] (a b c : G)
@@ -268,6 +338,22 @@ by simp [sub_eq_neg_add]
 @[simp] lemma image_sub_const_Ioo : (λ x, x - a) '' Ioo b c = Ioo (b - a) (c - a) :=
 by simp [sub_eq_neg_add]
 
+/-!
+### Bijections
+-/
+
+lemma Iic_add_bij : bij_on (+a) (Iic b) (Iic (b + a)) :=
+begin
+  refine ⟨λ x h, add_le_add_right (mem_Iic.mp h) _, λ _ _ _ _ h, add_right_cancel h, λ _ h, _⟩,
+  simpa [add_comm a] using h,
+end
+
+lemma Iio_add_bij : bij_on (+a) (Iio b) (Iio (b + a)) :=
+begin
+  refine ⟨λ x h, add_lt_add_right (mem_Iio.mp h) _, λ _ _ _ _ h, add_right_cancel h, λ _ h, _⟩,
+  simpa [add_comm a] using h,
+end
+
 end ordered_add_comm_group
 
 /-!