Theorem: Matroid.Iso.preimage_subset_iff (Matroid/Equiv.lean)

State before:
α : 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
Tactic:
rw [← e.image_symm_eq_preimage, image_subset_iff, e.preimage_symm_eq_image]
State after:
no goals