chore: forward-port leanprover-community/mathlib#18876 (#3753)

Mathlib/Data/Set/Intervals/Basic.lean

@@ -715,6 +715,40 @@ theorem Iic_inter_Ioc_of_le (h : a ≤ c) : Iic a ∩ Ioc b c = Ioc b a :=
   ext fun _ => ⟨fun H => ⟨H.2.1, H.1⟩, fun H => ⟨H.2, H.1, H.2.trans h⟩⟩
 #align set.Iic_inter_Ioc_of_le Set.Iic_inter_Ioc_of_le
 
+theorem not_mem_Icc_of_lt (ha : c < a) : c ∉ Icc a b := fun h => ha.not_le h.1
+#align set.not_mem_Icc_of_lt Set.not_mem_Icc_of_lt
+
+theorem not_mem_Icc_of_gt (hb : b < c) : c ∉ Icc a b := fun h => hb.not_le h.2
+#align set.not_mem_Icc_of_gt Set.not_mem_Icc_of_gt
+
+theorem not_mem_Ico_of_lt (ha : c < a) : c ∉ Ico a b := fun h => ha.not_le h.1
+#align set.not_mem_Ico_of_lt Set.not_mem_Ico_of_lt
+
+theorem not_mem_Ioc_of_gt (hb : b < c) : c ∉ Ioc a b := fun h => hb.not_le h.2
+#align set.not_mem_Ioc_of_gt Set.not_mem_Ioc_of_gt
+
+-- Porting note: `simp` can prove this
+-- @[simp]
+theorem not_mem_Ioi_self : a ∉ Ioi a := lt_irrefl _
+#align set.not_mem_Ioi_self Set.not_mem_Ioi_self
+
+-- Porting note: `simp` can prove this
+-- @[simp]
+theorem not_mem_Iio_self : b ∉ Iio b := lt_irrefl _
+#align set.not_mem_Iio_self Set.not_mem_Iio_self
+
+theorem not_mem_Ioc_of_le (ha : c ≤ a) : c ∉ Ioc a b := fun h => lt_irrefl _ <| h.1.trans_le ha
+#align set.not_mem_Ioc_of_le Set.not_mem_Ioc_of_le
+
+theorem not_mem_Ico_of_ge (hb : b ≤ c) : c ∉ Ico a b := fun h => lt_irrefl _ <| h.2.trans_le hb
+#align set.not_mem_Ico_of_ge Set.not_mem_Ico_of_ge
+
+theorem not_mem_Ioo_of_le (ha : c ≤ a) : c ∉ Ioo a b := fun h => lt_irrefl _ <| h.1.trans_le ha
+#align set.not_mem_Ioo_of_le Set.not_mem_Ioo_of_le
+
+theorem not_mem_Ioo_of_ge (hb : b ≤ c) : c ∉ Ioo a b := fun h => lt_irrefl _ <| h.2.trans_le hb
+#align set.not_mem_Ioo_of_ge Set.not_mem_Ioo_of_ge
+
 end Preorder
 
 section PartialOrder
@@ -1014,22 +1048,6 @@ theorem not_mem_Iic : c ∉ Iic b ↔ b < c :=
   not_le
 #align set.not_mem_Iic Set.not_mem_Iic
 
-theorem not_mem_Icc_of_lt (ha : c < a) : c ∉ Icc a b :=
-  not_mem_subset Icc_subset_Ici_self <| not_mem_Ici.mpr ha
-#align set.not_mem_Icc_of_lt Set.not_mem_Icc_of_lt
-
-theorem not_mem_Icc_of_gt (hb : b < c) : c ∉ Icc a b :=
-  not_mem_subset Icc_subset_Iic_self <| not_mem_Iic.mpr hb
-#align set.not_mem_Icc_of_gt Set.not_mem_Icc_of_gt
-
-theorem not_mem_Ico_of_lt (ha : c < a) : c ∉ Ico a b :=
-  not_mem_subset Ico_subset_Ici_self <| not_mem_Ici.mpr ha
-#align set.not_mem_Ico_of_lt Set.not_mem_Ico_of_lt
-
-theorem not_mem_Ioc_of_gt (hb : b < c) : c ∉ Ioc a b :=
-  not_mem_subset Ioc_subset_Iic_self <| not_mem_Iic.mpr hb
-#align set.not_mem_Ioc_of_gt Set.not_mem_Ioc_of_gt
-
 theorem not_mem_Ioi : c ∉ Ioi a ↔ c ≤ a :=
   not_lt
 #align set.not_mem_Ioi Set.not_mem_Ioi
@@ -1038,34 +1056,6 @@ theorem not_mem_Iio : c ∉ Iio b ↔ b ≤ c :=
   not_lt
 #align set.not_mem_Iio Set.not_mem_Iio
 
--- Porting note: `simp` can prove this
--- @[simp]
-theorem not_mem_Ioi_self : a ∉ Ioi a :=
-  lt_irrefl _
-#align set.not_mem_Ioi_self Set.not_mem_Ioi_self
-
--- Porting note: `simp` can prove this
--- @[simp]
-theorem not_mem_Iio_self : b ∉ Iio b :=
-  lt_irrefl _
-#align set.not_mem_Iio_self Set.not_mem_Iio_self
-
-theorem not_mem_Ioc_of_le (ha : c ≤ a) : c ∉ Ioc a b :=
-  not_mem_subset Ioc_subset_Ioi_self <| not_mem_Ioi.mpr ha
-#align set.not_mem_Ioc_of_le Set.not_mem_Ioc_of_le
-
-theorem not_mem_Ico_of_ge (hb : b ≤ c) : c ∉ Ico a b :=
-  not_mem_subset Ico_subset_Iio_self <| not_mem_Iio.mpr hb
-#align set.not_mem_Ico_of_ge Set.not_mem_Ico_of_ge
-
-theorem not_mem_Ioo_of_le (ha : c ≤ a) : c ∉ Ioo a b :=
-  not_mem_subset Ioo_subset_Ioi_self <| not_mem_Ioi.mpr ha
-#align set.not_mem_Ioo_of_le Set.not_mem_Ioo_of_le
-
-theorem not_mem_Ioo_of_ge (hb : b ≤ c) : c ∉ Ioo a b :=
-  not_mem_subset Ioo_subset_Iio_self <| not_mem_Iio.mpr hb
-#align set.not_mem_Ioo_of_ge Set.not_mem_Ioo_of_ge
-
 @[simp]
 theorem compl_Iic : Iic aᶜ = Ioi a :=
   ext fun _ => not_le