no goals
α : Type u_1
β : Type ?u.210763
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b \ Iic c = Ioc (max a c) b
rw [diff_eq, compl_Iic, Ioc_inter_Ioi, sup_eq_max]