Theorem: Matroid.parallelExtend_delete_eq (Matroid/Constructions/ParallelExtension.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
M M' : Matroid α
e✝ f x : α
I C : Set α
e : α
hf : f ∉ M.E
⊢ M.parallelExtend e f ＼ f = M
Tactic:
rwa [parallelExtend_delete_eq', deleteElem, delete_eq_self_iff, disjoint_singleton_left]
State after:
no goals