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

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