no goals
α : Type u_1
β : Type ?u.211189
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc a c = Ioc a (max b c)
rw [Ioc_union_Ioc, min_self] <;> exact (min_le_left _ _).trans (le_max_left _ _)