α : Type u_1
β : Type ?u.112442
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (↑toDual a) (↑toDual b) = Icc b a
α : Type u_1
β : Type ?u.112442
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (↑toDual a) (↑toDual b) = map (Equiv.toEmbedding toDual) (Icc b a)
refine' Eq.trans _ map_refl.symm
case a
α : Type u_1
β : Type ?u.112442
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Icc (↑toDual a) (↑toDual b) ↔ c ∈ Icc b a
α : Type u_1
β : Type ?u.112442
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (↑toDual a) (↑toDual b) = Icc b a
ext c
case a
α : Type u_1
β : Type ?u.112442
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ ↑toDual a ≤ c ∧ c ≤ ↑toDual b ↔ b ≤ c ∧ c ≤ a
case a
α : Type u_1
β : Type ?u.112442
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Icc (↑toDual a) (↑toDual b) ↔ c ∈ Icc b a
rw [mem_Icc, mem_Icc (α := α)]
no goals
case a
α : Type u_1
β : Type ?u.112442
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ ↑toDual a ≤ c ∧ c ≤ ↑toDual b ↔ b ≤ c ∧ c ≤ a
exact and_comm