no goals
α : Type u_1
β : Type ?u.192566
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
h : b₂ ≤ b₁
x : α
⊢ x ∈ Ioc a₁ b₁ ∩ Ioo a₂ b₂ ↔ x ∈ Ioo (max a₁ a₂) b₂
simp [and_assoc, @and_left_comm (x ≤ _),
  and_iff_right_iff_imp.2 fun h' => (le_of_lt h').trans h]