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