case a.h
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.98275
κ : ι → Sort ?u.98280
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f✝ : α ≃o β
s t : UpperSet α
a : α
b : β
g : β ≃o γ
f : α ≃o β
x✝ : γ
⊢ x✝ ∈ ↑(↑(map g) (↑(map f) s)) ↔ x✝ ∈ ↑(↑(map (OrderIso.trans f g)) s)
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.98275
κ : ι → Sort ?u.98280
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f✝ : α ≃o β
s t : UpperSet α
a : α
b : β
g : β ≃o γ
f : α ≃o β
⊢ ↑(map g) (↑(map f) s) = ↑(map (OrderIso.trans f g)) s
ext
no goals
case a.h
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Sort ?u.98275
κ : ι → Sort ?u.98280
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f✝ : α ≃o β
s t : UpperSet α
a : α
b : β
g : β ≃o γ
f : α ≃o β
x✝ : γ
⊢ x✝ ∈ ↑(↑(map g) (↑(map f) s)) ↔ x✝ ∈ ↑(↑(map (OrderIso.trans f g)) s)
simp