Theorem: Matroid.isoOfSwapParallel_apply_image (Matroid/Parallel.lean)

State before:
α : 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
Tactic:
rw [isoOfSwapParallel, isoOfMapParallelBijOn_apply_image]
State after:
no goals