no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ preimage t ↑f (_ : InjOn (↑f) (↑f ⁻¹' ↑t))
classical rw [map_eq_image, image_subset_iff_subset_preimage]
no goals
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ preimage t ↑f (_ : InjOn (↑f) (↑f ⁻¹' ↑t))
rw [map_eq_image, image_subset_iff_subset_preimage]