no goals
α : Type u_1
β : Type ?u.197772
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a a₁ a₂ b b₁ b₂ c d : α
⊢ ∀ (x : α), x ∈ Ioc a b \ Ioi c ↔ x ∈ Ioc a (min b c)
simp (config := { contextual := true }) [iff_def]