α : Type u_1
β : Type ?u.212353
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc b a = Ioc (min a b) (max b a)
α : Type u_1
β : Type ?u.212353
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc b a = Ioc (min a b) (max a b)
rw [max_comm]
no goals
α : Type u_1
β : Type ?u.212353
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ Ioc a b ∪ Ioc b a = Ioc (min a b) (max b a)
apply Ioc_union_Ioc <;> rw [max_comm] <;> exact min_le_max