suffices h' : e ∈ (M ／ C).cl X \ X ↔ e ∈ M.cl (X ∪ C) \ (X ∪ C) by
  rwa [mem_diff, and_iff_left heX, mem_diff, mem_union, or_iff_right heX, ← mem_diff] at h'
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 ↔ e ∈ M.cl (X ∪ C) \ C
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)