no goals
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ s ⊆ ↑e.symm '' t ↔ ↑e.symm.symm '' s ⊆ t
rw [e.symm.subset_image]
no goals
α✝ : Sort u
β✝ : Sort v
γ : Sort w
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ ↑e.symm.symm '' s ⊆ t ↔ ↑e '' s ⊆ t
rw [e.symm_symm]