ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h :
  Disjoint (Ico (↑toDual a₂) (↑toDual a₁)) (Ico (↑toDual b₂) (↑toDual b₁)) ↔
    min (↑toDual a₁) (↑toDual b₁) ≤ max (↑toDual a₂) (↑toDual b₂)
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico
no goals
ι : Sort u
α : Type v
β : Type w
inst✝ : LinearOrder α
a₁ a₂ b₁ b₂ : α
h :
  Disjoint (Ico (↑toDual a₂) (↑toDual a₁)) (Ico (↑toDual b₂) (↑toDual b₁)) ↔
    min (↑toDual a₁) (↑toDual b₁) ≤ max (↑toDual a₂) (↑toDual b₂)
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
simpa only [dual_Ico] using h