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

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
X : Set ↑M.E
⊢ ⇑e ⁻¹' (⇑e '' X) = X
Tactic:
rw [← e.image_symm_eq_preimage, e.symm_image_image]
State after:
no goals