case a.h
α : Type u_1
β : Type u_2
γ : Type ?u.118391
ι : Sort ?u.118394
κ : ι → Sort ?u.118399
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
a✝ b : α
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑(↑(map f) (Iio a)) ↔ x✝ ∈ ↑(Iio (↑f a))
α : Type u_1
β : Type u_2
γ : Type ?u.118391
ι : Sort ?u.118394
κ : ι → Sort ?u.118399
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
a✝ b : α
f : α ≃o β
a : α
⊢ ↑(map f) (Iio a) = Iio (↑f a)
ext
no goals
case a.h
α : Type u_1
β : Type u_2
γ : Type ?u.118391
ι : Sort ?u.118394
κ : ι → Sort ?u.118399
inst✝¹ : Preorder α
inst✝ : Preorder β
s : LowerSet α
a✝ b : α
f : α ≃o β
a : α
x✝ : β
⊢ x✝ ∈ ↑(↑(map f) (Iio a)) ↔ x✝ ∈ ↑(Iio (↑f a))
simp