feat(data/set/pointwise/interval): generalize some lemmas (#17837)

* Add `set.bij_on.inter_maps_to` and `set.maps_to.inter_bij_on`.
* Generalize `set.image_add_const_Ici` etc to `[ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α]`.
* Reorder, golf.

src/data/set/function.lean

@@ -630,6 +630,16 @@ lemma bij_on.mk (h₁ : maps_to f s t) (h₂ : inj_on f s) (h₃ : surj_on f s t
 lemma bij_on_empty (f : α → β) : bij_on f ∅ ∅ :=
 ⟨maps_to_empty f ∅, inj_on_empty f, surj_on_empty f ∅⟩
 
+lemma bij_on.inter_maps_to (h₁ : bij_on f s₁ t₁) (h₂ : maps_to f s₂ t₂) (h₃ : s₁ ∩ f ⁻¹' t₂ ⊆ s₂) :
+  bij_on f (s₁ ∩ s₂) (t₁ ∩ t₂) :=
+⟨h₁.maps_to.inter_inter h₂, h₁.inj_on.mono $ inter_subset_left _ _,
+  λ y hy, let ⟨x, hx, hxy⟩ := h₁.surj_on hy.1 in ⟨x, ⟨hx, h₃ ⟨hx, hxy.symm.rec_on hy.2⟩⟩, hxy⟩⟩
+
+lemma maps_to.inter_bij_on (h₁ : maps_to f s₁ t₁) (h₂ : bij_on f s₂ t₂)
+  (h₃ : s₂ ∩ f ⁻¹' t₁ ⊆ s₁) :
+  bij_on f (s₁ ∩ s₂) (t₁ ∩ t₂) :=
+inter_comm s₂ s₁ ▸ inter_comm t₂ t₁ ▸ h₂.inter_maps_to h₁ h₃
+
 lemma bij_on.inter (h₁ : bij_on f s₁ t₁) (h₂ : bij_on f s₂ t₂) (h : inj_on f (s₁ ∪ s₂)) :
   bij_on f (s₁ ∩ s₂) (t₁ ∩ t₂) :=
 ⟨h₁.maps_to.inter_inter h₂.maps_to, h₁.inj_on.mono $ inter_subset_left _ _,
@@ -660,8 +670,7 @@ theorem bij_on.comp (hg : bij_on g t p) (hf : bij_on f s t) : bij_on (g ∘ f) s
 bij_on.mk (hg.maps_to.comp hf.maps_to) (hg.inj_on.comp hf.inj_on hf.maps_to)
   (hg.surj_on.comp hf.surj_on)
 
-theorem bij_on.bijective (h : bij_on f s t) :
-  bijective (t.cod_restrict (s.restrict f) $ λ x, h.maps_to x.val_prop) :=
+theorem bij_on.bijective (h : bij_on f s t) : bijective (h.maps_to.restrict f s t) :=
 ⟨λ x y h', subtype.ext $ h.inj_on x.2 y.2 $ subtype.ext_iff.1 h',
   λ ⟨y, hy⟩, let ⟨x, hx, hxy⟩ := h.surj_on hy in ⟨⟨x, hx⟩, subtype.eq hxy⟩⟩
 

src/data/set/pointwise/interval.lean

@@ -33,64 +33,96 @@ The lemmas in this section state that addition maps intervals bijectively. The t
 TODO : move as much as possible in this file to the setting of this weaker typeclass.
 -/
 
-variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] (a b d : α)
+variables [ordered_cancel_add_comm_monoid α] [has_exists_add_of_le α] (a b c d : α)
 
-lemma Icc_add_bij : bij_on (+d) (Icc a b) (Icc (a + d) (b + d)) :=
+lemma Ici_add_bij : bij_on (+d) (Ici a) (Ici (a + 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,
+  refine ⟨λ x h, add_le_add_right (mem_Ici.mp h) _, (add_left_injective d).inj_on _, λ _ 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 Ioo_add_bij : bij_on (+d) (Ioo a b) (Ioo (a + d) (b + d)) :=
+lemma Ioi_add_bij : bij_on (+d) (Ioi a) (Ioi (a + 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,
+  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
 
-lemma Ioc_add_bij : bij_on (+d) (Ioc a b) (Ioc (a + d) (b + d)) :=
+lemma Icc_add_bij : bij_on (+d) (Icc a b) (Icc (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⟩,
+  rw [← Ici_inter_Iic, ← Ici_inter_Iic],
+  exact (Ici_add_bij a d).inter_maps_to (λ x hx, add_le_add_right hx _)
+    (λ x hx, le_of_add_le_add_right hx.2)
 end
 
-lemma Ico_add_bij : bij_on (+d) (Ico a b) (Ico (a + d) (b + d)) :=
+lemma Ioo_add_bij : bij_on (+d) (Ioo a b) (Ioo (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⟩,
+  rw [← Ioi_inter_Iio, ← Ioi_inter_Iio],
+  exact (Ioi_add_bij a d).inter_maps_to (λ x hx, add_lt_add_right hx _)
+    (λ x hx, lt_of_add_lt_add_right hx.2)
 end
 
-lemma Ici_add_bij : bij_on (+d) (Ici a) (Ici (a + d)) :=
+lemma Ioc_add_bij : bij_on (+d) (Ioc a b) (Ioc (a + d) (b + 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⟩,
+  rw [← Ioi_inter_Iic, ← Ioi_inter_Iic],
+  exact (Ioi_add_bij a d).inter_maps_to (λ x hx, add_le_add_right hx _)
+    (λ x hx, le_of_add_le_add_right hx.2)
 end
 
-lemma Ioi_add_bij : bij_on (+d) (Ioi a) (Ioi (a + d)) :=
+lemma Ico_add_bij : bij_on (+d) (Ico a b) (Ico (a + d) (b + 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⟩,
+  rw [← Ici_inter_Iio, ← Ici_inter_Iio],
+  exact (Ici_add_bij a d).inter_maps_to (λ x hx, add_lt_add_right hx _)
+    (λ x hx, lt_of_add_lt_add_right hx.2)
 end
 
+/-!
+### Images under `x ↦ x + a`
+-/
+
+@[simp] lemma image_add_const_Ici : (λ x, x + a) '' Ici b = Ici (b + a) :=
+(Ici_add_bij _ _).image_eq
+
+@[simp] lemma image_add_const_Ioi : (λ x, x + a) '' Ioi b = Ioi (b + a) :=
+(Ioi_add_bij _ _).image_eq
+
+@[simp] lemma image_add_const_Icc : (λ x, x + a) '' Icc b c = Icc (b + a) (c + a) :=
+(Icc_add_bij _ _ _).image_eq
+
+@[simp] lemma image_add_const_Ico : (λ x, x + a) '' Ico b c = Ico (b + a) (c + a) :=
+(Ico_add_bij _ _ _).image_eq
+
+@[simp] lemma image_add_const_Ioc : (λ x, x + a) '' Ioc b c = Ioc (b + a) (c + a) :=
+(Ioc_add_bij _ _ _).image_eq
+
+@[simp] lemma image_add_const_Ioo : (λ x, x + a) '' Ioo b c = Ioo (b + a) (c + a) :=
+(Ioo_add_bij _ _ _).image_eq
+
+/-!
+### Images under `x ↦ a + x`
+-/
+
+@[simp] lemma image_const_add_Ici : (λ x, a + x) '' Ici b = Ici (a + b) :=
+by simp only [add_comm a, image_add_const_Ici]
+
+@[simp] lemma image_const_add_Ioi : (λ x, a + x) '' Ioi b = Ioi (a + b) :=
+by simp only [add_comm a, image_add_const_Ioi]
+
+@[simp] lemma image_const_add_Icc : (λ x, a + x) '' Icc b c = Icc (a + b) (a + c) :=
+by simp only [add_comm a, image_add_const_Icc]
+
+@[simp] lemma image_const_add_Ico : (λ x, a + x) '' Ico b c = Ico (a + b) (a + c) :=
+by simp only [add_comm a, image_add_const_Ico]
+
+@[simp] lemma image_const_add_Ioc : (λ x, a + x) '' Ioc b c = Ioc (a + b) (a + c) :=
+by simp only [add_comm a, image_add_const_Ioc]
+
+@[simp] lemma image_const_add_Ioo : (λ x, a + x) '' Ioo b c = Ioo (a + b) (a + c) :=
+by simp only [add_comm a, image_add_const_Ioo]
+
 end has_exists_add_of_le
 
 section ordered_add_comm_group
@@ -233,50 +265,18 @@ by simp [← Ioi_inter_Iio, inter_comm]
 ### Images under `x ↦ a + x`
 -/
 
-@[simp] lemma image_const_add_Ici : (λ x, a + x) '' Ici b = Ici (a + b) :=
-by simp [add_comm]
-
 @[simp] lemma image_const_add_Iic : (λ x, a + x) '' Iic b = Iic (a + b) :=
 by simp [add_comm]
 
 @[simp] lemma image_const_add_Iio : (λ x, a + x) '' Iio b = Iio (a + b) :=
 by simp [add_comm]
 
-@[simp] lemma image_const_add_Ioi : (λ x, a + x) '' Ioi b = Ioi (a + b) :=
-by simp [add_comm]
-
-@[simp] lemma image_const_add_Icc : (λ x, a + x) '' Icc b c = Icc (a + b) (a + c) :=
-by simp [add_comm]
-
-@[simp] lemma image_const_add_Ico : (λ x, a + x) '' Ico b c = Ico (a + b) (a + c) :=
-by simp [add_comm]
-
-@[simp] lemma image_const_add_Ioc : (λ x, a + x) '' Ioc b c = Ioc (a + b) (a + c) :=
-by simp [add_comm]
-
-@[simp] lemma image_const_add_Ioo : (λ x, a + x) '' Ioo b c = Ioo (a + b) (a + c) :=
-by simp [add_comm]
-
 /-!
 ### Images under `x ↦ x + a`
 -/
 
-@[simp] lemma image_add_const_Ici : (λ x, x + a) '' Ici b = Ici (b + a) := by simp
 @[simp] lemma image_add_const_Iic : (λ x, x + a) '' Iic b = Iic (b + a) := by simp
 @[simp] lemma image_add_const_Iio : (λ x, x + a) '' Iio b = Iio (b + a) := by simp
-@[simp] lemma image_add_const_Ioi : (λ x, x + a) '' Ioi b = Ioi (b + a) := by simp
-
-@[simp] lemma image_add_const_Icc : (λ x, x + a) '' Icc b c = Icc (b + a) (c + a) :=
-by simp
-
-@[simp] lemma image_add_const_Ico : (λ x, x + a) '' Ico b c = Ico (b + a) (c + a) :=
-by simp
-
-@[simp] lemma image_add_const_Ioc : (λ x, x + a) '' Ioc b c = Ioc (b + a) (c + a) :=
-by simp
-
-@[simp] lemma image_add_const_Ioo : (λ x, x + a) '' Ioo b c = Ioo (b + a) (c + a) :=
-by simp
 
 /-!
 ### Images under `x ↦ -x`
@@ -345,16 +345,10 @@ by simp [sub_eq_neg_add]
 -/
 
 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
+image_add_const_Iic a b ▸ ((add_left_injective _).inj_on _).bij_on_image
 
 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
+image_add_const_Iio a b ▸ ((add_left_injective _).inj_on _).bij_on_image
 
 end ordered_add_comm_group