rw [Equiv.swap_image_eq_self (by simp [hfI, heI])]
case neg
α : Type u_1
M N : Matroid α
e f g : α
I✝ X P D : Set α
h : M.Parallel' e f
inst✝ : DecidableEq α
hrw : ⇑(Equiv.swap e f) '' M.E = M.E
I : Set α
heI : e ∉ I
hfI : f ∉ I
⊢ M.Indep ((fun a => (Equiv.swap e f) a) '' I) ↔ M.Indep I
no goals