rw [← e.image_symm_eq_preimage, image_subset_iff, e.preimage_symm_eq_image]
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
X : Set ↑N.E
Y : Set ↑M.E
⊢ ⇑e ⁻¹' X ⊆ Y ↔ X ⊆ ⇑e '' Y
no goals