α : Type u_2
β : Type u_1
γ : Type ?u.96866
ι : Sort ?u.96869
κ : ι → Sort ?u.96874
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α ≃o β
s t : UpperSet α
a : α
b : β
⊢ b ∈ ↑(OrderIso.symm (map (OrderIso.symm f))) s ↔ ↑(OrderIso.symm f) b ∈ s
α : Type u_2
β : Type u_1
γ : Type ?u.96866
ι : Sort ?u.96869
κ : ι → Sort ?u.96874
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α ≃o β
s t : UpperSet α
a : α
b : β
⊢ b ∈ ↑(map f) s ↔ ↑(OrderIso.symm f) b ∈ s
rw [← f.symm_symm, ← symm_map, f.symm_symm]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.96866
ι : Sort ?u.96869
κ : ι → Sort ?u.96874
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α ≃o β
s t : UpperSet α
a : α
b : β
⊢ b ∈ ↑(OrderIso.symm (map (OrderIso.symm f))) s ↔ ↑(OrderIso.symm f) b ∈ s
rfl