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