α : Type u_1
β : Type ?u.113413
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc (↑toDual a) (↑toDual b) = Ico b a
α : Type u_1
β : Type ?u.113413
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc (↑toDual a) (↑toDual b) = map (Equiv.toEmbedding toDual) (Ico b a)
refine' Eq.trans _ map_refl.symm
case a
α : Type u_1
β : Type ?u.113413
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Ioc (↑toDual a) (↑toDual b) ↔ c ∈ Ico b a
α : Type u_1
β : Type ?u.113413
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc (↑toDual a) (↑toDual b) = Ico b a
ext c
case a
α : Type u_1
β : Type ?u.113413
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.113413
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Ioc (↑toDual a) (↑toDual b) ↔ c ∈ Ico b a
rw [mem_Ioc, mem_Ico (α := α)]
no goals
case a
α : Type u_1
β : Type ?u.113413
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