no goals
α : Type u_1
β : Type ?u.197269
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ico a b \ Iio c = Ico (max a c) b
rw [diff_eq, compl_Iio, Ico_inter_Ici, sup_eq_max]