feat: add missing Set.Ioo_inter_Iio etc (#11902)

add missing lemmas. I'm not sure if these should be @[simp], as e.g. Ico_inter_Ico isn't, but Ico_inter_Iio is

Author: sven-manthe

Mathlib/Data/Set/Intervals/Basic.lean

@@ -1817,6 +1817,20 @@ theorem Ioo_inter_Ioo : Ioo a₁ b₁ ∩ Ioo a₂ b₂ = Ioo (a₁ ⊔ a₂) (b
   simp only [Ioi_inter_Iio.symm, Ioi_inter_Ioi.symm, Iio_inter_Iio.symm]; ac_rfl
 #align set.Ioo_inter_Ioo Set.Ioo_inter_Ioo
 
+theorem Ioo_inter_Iio : Ioo a b ∩ Iio c = Ioo a (min b c) := by
+  ext
+  simp_rw [mem_inter_iff, mem_Ioo, mem_Iio, lt_min_iff, and_assoc]
+
+theorem Iio_inter_Ioo : Iio a ∩ Ioo b c = Ioo b (min a c) := by
+  rw [Set.inter_comm, Set.Ioo_inter_Iio, min_comm]
+
+theorem Ioo_inter_Ioi : Ioo a b ∩ Ioi c = Ioo (max a c) b := by
+  ext
+  simp_rw [mem_inter_iff, mem_Ioo, mem_Ioi, max_lt_iff, and_assoc, and_comm]
+
+theorem Ioi_inter_Ioo : Set.Ioi a ∩ Set.Ioo b c = Set.Ioo (max a b) c := by
+  rw [inter_comm, Ioo_inter_Ioi, max_comm]
+
 theorem Ioc_inter_Ioo_of_left_lt (h : b₁ < b₂) : Ioc a₁ b₁ ∩ Ioo a₂ b₂ = Ioc (max a₁ a₂) b₁ :=
   ext fun x => by
     simp [and_assoc, @and_left_comm (x ≤ _), and_iff_left_iff_imp.2 fun h' => lt_of_le_of_lt h' h]