no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
κ : ι → Sort ?u.32992
a a₁ a₂ : α
b b₁ b₂ : β
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
s : Set β
⊢ BddAbove (↑e ⁻¹' s) ↔ BddAbove s
rw [← e.bddAbove_image, e.image_preimage]