rw [isoOfSwapParallel, isoOfMapParallelBijOn_apply_image]
α : Type u_1
M N : Matroid α
e f g : α
I X✝ P D : Set α
inst✝ : DecidableEq α
h_para : M.Parallel' e f
X : Set ↑M.E
⊢ ↑(⇑(isoOfSwapParallel h_para) '' X) = ⇑(Equiv.swap e f) '' ↑X
no goals