rw [← contract_loop_iff_mem_cl, ← contract_loop_iff_mem_cl, contract_contract, union_comm]
case neg
α : Type u_1
M✝ M' N : Matroid α
e✝ f : α
I J R B X✝ Y Z K C✝ C₁ C₂ : Set α
M : Matroid α
C X : Set α
e : α
heX : e ∉ X
⊢ e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C)
no goals