case a.h
α : Type u_1
β : Type u_2
γ : Type ?u.111542
ι : Sort ?u.111545
κ : ι → Sort ?u.111550
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
a✝ b : α
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑(↑(map f) (Ici a)) ↔ x✝ ∈ ↑(Ici (↑f a))
α : Type u_1
β : Type u_2
γ : Type ?u.111542
ι : Sort ?u.111545
κ : ι → Sort ?u.111550
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
a✝ b : α
f : α ≃o β
a : α
⊢ ↑(map f) (Ici a) = Ici (↑f a)
ext
no goals
case a.h
α : Type u_1
β : Type u_2
γ : Type ?u.111542
ι : Sort ?u.111545
κ : ι → Sort ?u.111550
inst✝¹ : Preorder α
inst✝ : Preorder β
s : UpperSet α
a✝ b : α
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑(↑(map f) (Ici a)) ↔ x✝ ∈ ↑(Ici (↑f a))
simp