no goals
α : Type u_1
β : Type ?u.196535
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₁ ≤ b₂
⊢ Ioo a₁ b₁ ∩ Ioc a₂ b₂ = Ioo (max a₁ a₂) b₁
rw [inter_comm, Ioc_inter_Ioo_of_right_le h, max_comm]