feat(order/succ_pred/basic): Intervals and succ/pred (#13486)

Relate `order.succ`, `order.pred` and `set.Ixx`.

src/analysis/calculus/cont_diff.lean

@@ -2803,7 +2803,7 @@ begin
   rcases metric.mem_nhds_within_iff.mp hst with ⟨ε, ε0, hε⟩,
   replace hp : has_ftaylor_series_up_to_on 1 f p (metric.ball x ε ∩ insert x s) := hp.mono hε,
   clear hst hε t,
-  rw [← insert_eq_of_mem (metric.mem_ball_self ε0), ← insert_inter] at hp,
+  rw [← insert_eq_of_mem (metric.mem_ball_self ε0), ← insert_inter_distrib] at hp,
   rcases hp.exists_lipschitz_on_with ((convex_ball _ _).inter hs) with ⟨K, t, hst, hft⟩,
   rw [inter_comm, ← nhds_within_restrict' _ (metric.ball_mem_nhds _ ε0)] at hst,
   exact ⟨K, t, hst, hft⟩

src/data/set/basic.lean

@@ -691,9 +691,12 @@ theorem insert_nonempty (a : α) (s : set α) : (insert a s).nonempty := ⟨a, m
 
 instance (a : α) (s : set α) : nonempty (insert a s : set α) := (insert_nonempty a s).to_subtype
 
-lemma insert_inter (x : α) (s t : set α) : insert x (s ∩ t) = insert x s ∩ insert x t :=
+lemma insert_inter_distrib (a : α) (s t : set α) : insert a (s ∩ t) = insert a s ∩ insert a t :=
 ext $ λ y, or_and_distrib_left
 
+lemma insert_union_distrib (a : α) (s t : set α) : insert a (s ∪ t) = insert a s ∪ insert a t :=
+ext $ λ _, or_or_distrib_left _ _ _
+
 lemma insert_inj (ha : a ∉ s) : insert a s = insert b s ↔ a = b :=
 ⟨λ h, eq_of_not_mem_of_mem_insert (h.subst $ mem_insert a s) ha, congr_arg _⟩
 
@@ -1074,17 +1077,17 @@ begin
   exact h,
 end
 
-lemma insert_inter_of_mem {s₁ s₂ : set α} {a : α} (h : a ∈ s₂) :
-  insert a s₁ ∩ s₂ = insert a (s₁ ∩ s₂) :=
-by simp [set.insert_inter, h]
+lemma inter_insert_of_mem (h : a ∈ s) : s ∩ insert a t = insert a (s ∩ t) :=
+by rw [insert_inter_distrib, insert_eq_of_mem h]
 
-lemma insert_inter_of_not_mem {s₁ s₂ : set α} {a : α} (h : a ∉ s₂) :
-  insert a s₁ ∩ s₂ = s₁ ∩ s₂ :=
-begin
-  ext x,
-  simp only [mem_inter_iff, mem_insert_iff, mem_inter_eq, and.congr_left_iff, or_iff_right_iff_imp],
-  cc,
-end
+lemma insert_inter_of_mem (h : a ∈ t) : insert a s ∩ t = insert a (s ∩ t) :=
+by rw [insert_inter_distrib, insert_eq_of_mem h]
+
+lemma inter_insert_of_not_mem (h : a ∉ s) : s ∩ insert a t = s ∩ t :=
+ext $ λ x, and_congr_right $ λ hx, or_iff_right $ ne_of_mem_of_not_mem hx h
+
+lemma insert_inter_of_not_mem (h : a ∉ t) : insert a s ∩ t = s ∩ t :=
+ext $ λ x, and_congr_left $ λ hx, or_iff_right $ ne_of_mem_of_not_mem hx h
 
 @[simp] theorem union_diff_self {s t : set α} : s ∪ (t \ s) = s ∪ t :=
 sup_sdiff_self_right

src/data/set/intervals/basic.lean

@@ -349,6 +349,10 @@ lemma Ici_inter_Iic : Ici a ∩ Iic b = Icc a b := rfl
 lemma Ici_inter_Iio : Ici a ∩ Iio b = Ico a b := rfl
 lemma Ioi_inter_Iic : Ioi a ∩ Iic b = Ioc a b := rfl
 lemma Ioi_inter_Iio : Ioi a ∩ Iio b = Ioo a b := rfl
+lemma Iic_inter_Ici : Iic a ∩ Ici b = Icc b a := inter_comm _ _
+lemma Iio_inter_Ici : Iio a ∩ Ici b = Ico b a := inter_comm _ _
+lemma Iic_inter_Ioi : Iic a ∩ Ioi b = Ioc b a := inter_comm _ _
+lemma Iio_inter_Ioi : Iio a ∩ Ioi b = Ioo b a := inter_comm _ _
 
 lemma mem_Icc_of_Ioo (h : x ∈ Ioo a b) : x ∈ Icc a b := Ioo_subset_Icc_self h
 lemma mem_Ico_of_Ioo (h : x ∈ Ioo a b) : x ∈ Ico a b := Ioo_subset_Ico_self h
@@ -456,6 +460,23 @@ by rw [← Icc_diff_left, diff_union_self,
 lemma Ico_union_right (hab : a ≤ b) : Ico a b ∪ {b} = Icc a b :=
 by simpa only [dual_Ioc, dual_Icc] using Ioc_union_left hab.dual
 
+@[simp] lemma Ico_insert_right (h : a ≤ b) : insert b (Ico a b) = Icc a b :=
+by rw [insert_eq, union_comm, Ico_union_right h]
+
+@[simp] lemma Ioc_insert_left (h : a ≤ b) : insert a (Ioc a b) = Icc a b :=
+by rw [insert_eq, union_comm, Ioc_union_left h]
+
+@[simp] lemma Ioo_insert_left (h : a < b) : insert a (Ioo a b) = Ico a b :=
+by rw [insert_eq, union_comm, Ioo_union_left h]
+
+@[simp] lemma Ioo_insert_right (h : a < b) : insert b (Ioo a b) = Ioc a b :=
+by rw [insert_eq, union_comm, Ioo_union_right h]
+
+@[simp] lemma Iio_insert : insert a (Iio a) = Iic a := ext $ λ _, le_iff_eq_or_lt.symm
+
+@[simp] lemma Ioi_insert : insert a (Ioi a) = Ici a :=
+ext $ λ _, (or_congr_left' eq_comm).trans le_iff_eq_or_lt.symm
+
 lemma mem_Ici_Ioi_of_subset_of_subset {s : set α} (ho : Ioi a ⊆ s) (hc : s ⊆ Ici a) :
   s ∈ ({Ici a, Ioi a} : set (set α)) :=
 classical.by_cases

src/data/set/intervals/ord_connected.lean

@@ -49,9 +49,8 @@ begin
   rw ord_connected_iff,
   intros x hx y hy hxy,
   rcases eq_or_lt_of_le hxy with rfl|hxy', { simpa },
-  have := hs x hx y hy hxy',
-  rw [← union_diff_cancel Ioo_subset_Icc_self],
-  simp [*, insert_subset]
+  rw [←Ioc_insert_left hxy, ←Ioo_insert_right hxy'],
+  exact insert_subset.2 ⟨hx, insert_subset.2 ⟨hy, hs x hx y hy hxy'⟩⟩,
 end
 
 protected lemma Icc_subset (s : set α) [hs : ord_connected s] {x y} (hx : x ∈ s) (hy : y ∈ s) :

src/logic/basic.lean

@@ -442,6 +442,12 @@ by simp only [and.left_comm, and.comm]
 lemma and_and_and_comm (a b c d : Prop) : (a ∧ b) ∧ c ∧ d ↔ (a ∧ c) ∧ b ∧ d :=
 by rw [←and_assoc, @and.right_comm a, and_assoc]
 
+lemma and_and_distrib_left (a b c : Prop) : a ∧ (b ∧ c) ↔ (a ∧ b) ∧ (a ∧ c) :=
+by rw [and_and_and_comm, and_self]
+
+lemma and_and_distrib_right (a b c : Prop) : (a ∧ b) ∧ c ↔ (a ∧ c) ∧ (b ∧ c) :=
+by rw [and_and_and_comm, and_self]
+
 lemma and_rotate : a ∧ b ∧ c ↔ b ∧ c ∧ a := by simp only [and.left_comm, and.comm]
 lemma and.rotate : a ∧ b ∧ c → b ∧ c ∧ a := and_rotate.1
 
@@ -493,6 +499,12 @@ theorem or.right_comm : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b := by rw [or_assoc,
 lemma or_or_or_comm (a b c d : Prop) : (a ∨ b) ∨ c ∨ d ↔ (a ∨ c) ∨ b ∨ d :=
 by rw [←or_assoc, @or.right_comm a, or_assoc]
 
+lemma or_or_distrib_left (a b c : Prop) : a ∨ (b ∨ c) ↔ (a ∨ b) ∨ (a ∨ c) :=
+by rw [or_or_or_comm, or_self]
+
+lemma or_or_distrib_right (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ (b ∨ c) :=
+by rw [or_or_or_comm, or_self]
+
 lemma or_rotate : a ∨ b ∨ c ↔ b ∨ c ∨ a := by simp only [or.left_comm, or.comm]
 lemma or.rotate : a ∨ b ∨ c → b ∨ c ∨ a := or_rotate.1
 

src/order/succ_pred/basic.lean

@@ -182,6 +182,18 @@ set.ext $ λ x, lt_succ_iff_of_not_is_max ha
 lemma Ici_succ_of_not_is_max (ha : ¬ is_max a) : Ici (succ a) = Ioi a :=
 set.ext $ λ x, succ_le_iff_of_not_is_max ha
 
+lemma Ico_succ_right_of_not_is_max (hb : ¬ is_max b) : Ico a (succ b) = Icc a b :=
+by rw [←Ici_inter_Iio, Iio_succ_of_not_is_max hb, Ici_inter_Iic]
+
+lemma Ioo_succ_right_of_not_is_max (hb : ¬ is_max b) : Ioo a (succ b) = Ioc a b :=
+by rw [←Ioi_inter_Iio, Iio_succ_of_not_is_max hb, Ioi_inter_Iic]
+
+lemma Icc_succ_left_of_not_is_max (ha : ¬ is_max a) : Icc (succ a) b = Ioc a b :=
+by rw [←Ici_inter_Iic, Ici_succ_of_not_is_max ha, Ioi_inter_Iic]
+
+lemma Ico_succ_left_of_not_is_max (ha : ¬ is_max a) : Ico (succ a) b = Ioo a b :=
+by rw [←Ici_inter_Iio, Ici_succ_of_not_is_max ha, Ioi_inter_Iio]
+
 section no_max_order
 variables [no_max_order α]
 
@@ -202,8 +214,20 @@ lemma succ_strict_mono : strict_mono (succ : α → α) := λ a b, succ_lt_succ
 
 lemma covby_succ (a : α) : a ⋖ succ a := covby_succ_of_not_is_max $ not_is_max a
 
-lemma Iio_succ (a : α) : Iio (succ a) = Iic a := Iio_succ_of_not_is_max $ not_is_max a
-lemma Ici_succ (a : α) : Ici (succ a) = Ioi a := Ici_succ_of_not_is_max $ not_is_max a
+@[simp] lemma Iio_succ (a : α) : Iio (succ a) = Iic a := Iio_succ_of_not_is_max $ not_is_max _
+@[simp] lemma Ici_succ (a : α) : Ici (succ a) = Ioi a := Ici_succ_of_not_is_max $ not_is_max _
+
+lemma Ico_succ_right (a b : α) : Ico a (succ b) = Icc a b :=
+Ico_succ_right_of_not_is_max $ not_is_max _
+
+lemma Ioo_succ_right (a b : α) : Ioo a (succ b) = Ioc a b :=
+Ioo_succ_right_of_not_is_max $ not_is_max _
+
+lemma Icc_succ_left (a b : α) : Icc (succ a) b = Ioc a b :=
+Icc_succ_left_of_not_is_max $ not_is_max _
+
+lemma Ico_succ_left (a b : α) : Ico (succ a) b = Ioo a b :=
+Ico_succ_left_of_not_is_max $ not_is_max _
 
 end no_max_order
 end preorder
@@ -228,6 +252,24 @@ end
 lemma _root_.covby.succ_eq (h : a ⋖ b) : succ a = b :=
 (succ_le_of_lt h.lt).eq_of_not_lt $ λ h', h.2 (lt_succ_of_not_is_max h.lt.not_is_max) h'
 
+lemma le_succ_iff_eq_or_le : a ≤ succ b ↔ a = succ b ∨ a ≤ b :=
+begin
+  by_cases hb : is_max b,
+  { rw [hb.succ_eq, or_iff_right_of_imp le_of_eq] },
+  { rw [←lt_succ_iff_of_not_is_max hb, le_iff_eq_or_lt] }
+end
+
+lemma lt_succ_iff_eq_or_lt_of_not_is_max (hb : ¬ is_max b) : a < succ b ↔ a = b ∨ a < b :=
+(lt_succ_iff_of_not_is_max hb).trans le_iff_eq_or_lt
+
+lemma Iic_succ (a : α) : Iic (succ a) = insert (succ a) (Iic a) := ext $ λ _, le_succ_iff_eq_or_le
+
+lemma Icc_succ_right (h : a ≤ succ b) : Icc a (succ b) = insert (succ b) (Icc a b) :=
+by simp_rw [←Ici_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ici.2 h)]
+
+lemma Ioc_succ_right (h : a < succ b) : Ioc a (succ b) = insert (succ b) (Ioc a b) :=
+by simp_rw [←Ioi_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ioi.2 h)]
+
 section no_max_order
 variables [no_max_order α]
 
@@ -239,14 +281,20 @@ lemma succ_ne_succ_iff : succ a ≠ succ b ↔ a ≠ b := succ_injective.ne_iff
 
 alias succ_ne_succ_iff ↔ _ order.succ_ne_succ
 
-lemma lt_succ_iff_lt_or_eq : a < succ b ↔ a < b ∨ a = b := lt_succ_iff.trans le_iff_lt_or_eq
-
-lemma le_succ_iff_lt_or_eq : a ≤ succ b ↔ a ≤ b ∨ a = succ b :=
-by rw [←lt_succ_iff, ←lt_succ_iff, lt_succ_iff_lt_or_eq]
+lemma lt_succ_iff_eq_or_lt : a < succ b ↔ a = b ∨ a < b := lt_succ_iff.trans le_iff_eq_or_lt
 
 lemma succ_eq_iff_covby : succ a = b ↔ a ⋖ b :=
 ⟨by { rintro rfl, exact covby_succ _ }, covby.succ_eq⟩
 
+lemma Iio_succ_eq_insert (a : α) : Iio (succ a) = insert a (Iio a) :=
+ext $ λ _, lt_succ_iff_eq_or_lt
+
+lemma Ico_succ_right_eq_insert (h : a ≤ b) : Ico a (succ b) = insert b (Ico a b) :=
+by simp_rw [←Iio_inter_Ici, Iio_succ_eq_insert, insert_inter_of_mem (mem_Ici.2 h)]
+
+lemma Ioo_succ_right_eq_insert (h : a < b) : Ioo a (succ b) = insert b (Ioo a b) :=
+by simp_rw [←Iio_inter_Ioi, Iio_succ_eq_insert, insert_inter_of_mem (mem_Ioi.2 h)]
+
 end no_max_order
 
 section order_top
@@ -335,6 +383,18 @@ set.ext $ λ x, pred_lt_iff_of_not_is_min ha
 lemma Iic_pred_of_not_is_min (ha : ¬ is_min a) : Iic (pred a) = Iio a :=
 set.ext $ λ x, le_pred_iff_of_not_is_min ha
 
+lemma Ioc_pred_left_of_not_is_min (ha : ¬ is_min a) : Ioc (pred a) b = Icc a b :=
+by rw [←Ioi_inter_Iic, Ioi_pred_of_not_is_min ha, Ici_inter_Iic]
+
+lemma Ioo_pred_left_of_not_is_min (ha : ¬ is_min a) : Ioo (pred a) b = Ico a b :=
+by rw [←Ioi_inter_Iio, Ioi_pred_of_not_is_min ha, Ici_inter_Iio]
+
+lemma Icc_pred_right_of_not_is_min (ha : ¬ is_min b) : Icc a (pred b) = Ico a b :=
+by rw [←Ici_inter_Iic, Iic_pred_of_not_is_min ha, Ici_inter_Iio]
+
+lemma Ioc_pred_right_of_not_is_min (ha : ¬ is_min b) : Ioc a (pred b) = Ioo a b :=
+by rw [←Ioi_inter_Iic, Iic_pred_of_not_is_min ha, Ioi_inter_Iio]
+
 section no_min_order
 variables [no_min_order α]
 
@@ -355,8 +415,20 @@ lemma pred_strict_mono : strict_mono (pred : α → α) := λ a b, pred_lt_pred
 
 lemma pred_covby (a : α) : pred a ⋖ a := pred_covby_of_not_is_min $ not_is_min a
 
-lemma Ioi_pred (a : α) : Ioi (pred a) = Ici a := Ioi_pred_of_not_is_min $ not_is_min a
-lemma Iic_pred (a : α) : Iic (pred a) = Iio a := Iic_pred_of_not_is_min $ not_is_min a
+@[simp] lemma Ioi_pred (a : α) : Ioi (pred a) = Ici a := Ioi_pred_of_not_is_min $ not_is_min a
+@[simp] lemma Iic_pred (a : α) : Iic (pred a) = Iio a := Iic_pred_of_not_is_min $ not_is_min a
+
+lemma Ioc_pred_left (a b : α) : Ioc (pred a) b = Icc a b :=
+Ioc_pred_left_of_not_is_min $ not_is_min _
+
+lemma Ioo_pred_left (a b : α) : Ioo (pred a) b = Ico a b :=
+Ioo_pred_left_of_not_is_min $ not_is_min _
+
+lemma Icc_pred_right (a b : α) : Icc a (pred b) = Ico a b :=
+Icc_pred_right_of_not_is_min $ not_is_min _
+
+lemma Ioc_pred_right (a b : α) : Ioc a (pred b) = Ioo a b :=
+Ioc_pred_right_of_not_is_min $ not_is_min _
 
 end no_min_order
 end preorder
@@ -381,6 +453,24 @@ end
 lemma _root_.covby.pred_eq {a b : α} (h : a ⋖ b) : pred b = a :=
 (le_pred_of_lt h.lt).eq_of_not_gt $ λ h', h.2 h' $ pred_lt_of_not_is_min h.lt.not_is_min
 
+lemma pred_le_iff_eq_or_le : pred a ≤ b ↔ b = pred a ∨ a ≤ b :=
+begin
+  by_cases ha : is_min a,
+  { rw [ha.pred_eq, or_iff_right_of_imp ge_of_eq] },
+  { rw [←pred_lt_iff_of_not_is_min ha, le_iff_eq_or_lt, eq_comm] }
+end
+
+lemma pred_lt_iff_eq_or_lt_of_not_is_min (ha : ¬ is_min a) : pred a < b ↔ a = b ∨ a < b :=
+(pred_lt_iff_of_not_is_min ha).trans le_iff_eq_or_lt
+
+lemma Ici_pred (a : α) : Ici (pred a) = insert (pred a) (Ici a) := ext $ λ _, pred_le_iff_eq_or_le
+
+lemma Icc_pred_left (h : pred a ≤ b) : Icc (pred a) b = insert (pred a) (Icc a b) :=
+by simp_rw [←Ici_inter_Iic, Ici_pred, insert_inter_of_mem (mem_Iic.2 h)]
+
+lemma Ico_pred_left (h : pred a < b) : Ico (pred a) b = insert (pred a) (Ico a b) :=
+by simp_rw [←Ici_inter_Iio, Ici_pred, insert_inter_of_mem (mem_Iio.2 h)]
+
 section no_min_order
 variables [no_min_order α]
 
@@ -392,14 +482,20 @@ lemma pred_ne_pred_iff : pred a ≠ pred b ↔ a ≠ b := pred_injective.ne_iff
 
 alias pred_ne_pred_iff ↔ _ order.pred_ne_pred
 
-lemma pred_lt_iff_lt_or_eq : pred a < b ↔ a < b ∨ a = b := pred_lt_iff.trans le_iff_lt_or_eq
-
-lemma le_pred_iff_lt_or_eq : pred a ≤ b ↔ a ≤ b ∨ pred a = b :=
-by rw [←pred_lt_iff, ←pred_lt_iff, pred_lt_iff_lt_or_eq]
+lemma pred_lt_iff_eq_or_lt : pred a < b ↔ a = b ∨ a < b := pred_lt_iff.trans le_iff_eq_or_lt
 
 lemma pred_eq_iff_covby : pred b = a ↔ a ⋖ b :=
 ⟨by { rintro rfl, exact pred_covby _ }, covby.pred_eq⟩
 
+lemma Ioi_pred_eq_insert (a : α) : Ioi (pred a) = insert a (Ioi a) :=
+ext $ λ _, pred_lt_iff_eq_or_lt.trans $ or_congr_left' eq_comm
+
+lemma Ico_pred_right_eq_insert (h : a ≤ b) : Ioc (pred a) b = insert a (Ioc a b) :=
+by simp_rw [←Ioi_inter_Iic, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iic.2 h)]
+
+lemma Ioo_pred_right_eq_insert (h : a < b) : Ioo (pred a) b = insert a (Ioo a b) :=
+by simp_rw [←Ioi_inter_Iio, Ioi_pred_eq_insert, insert_inter_of_mem (mem_Iio.2 h)]
+
 end no_min_order
 
 section order_bot