case h.h.a.h
α : Type u_1
β : Type ?u.97471
γ : Type ?u.97474
ι : Sort ?u.97477
κ : ι → Sort ?u.97482
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α ≃o β
s t : UpperSet α
a : α
b : β
x✝¹ : UpperSet α
x✝ : α
⊢ x✝ ∈ ↑(↑(map (OrderIso.refl α)) x✝¹) ↔ x✝ ∈ ↑(↑(OrderIso.refl (UpperSet α)) x✝¹)
α : Type u_1
β : Type ?u.97471
γ : Type ?u.97474
ι : Sort ?u.97477
κ : ι → Sort ?u.97482
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α ≃o β
s t : UpperSet α
a : α
b : β
⊢ map (OrderIso.refl α) = OrderIso.refl (UpperSet α)
ext
no goals
case h.h.a.h
α : Type u_1
β : Type ?u.97471
γ : Type ?u.97474
ι : Sort ?u.97477
κ : ι → Sort ?u.97482
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α ≃o β
s t : UpperSet α
a : α
b : β
x✝¹ : UpperSet α
x✝ : α
⊢ x✝ ∈ ↑(↑(map (OrderIso.refl α)) x✝¹) ↔ x✝ ∈ ↑(↑(OrderIso.refl (UpperSet α)) x✝¹)
simp