rw [contract_ground] at he
case pos
α : 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
he : e ∈ (M ／ C).E
⊢ e ∈ M.cl (X ∪ C) \ C
case pos
α : 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
he : e ∈ M.E \ C
⊢ e ∈ M.cl (X ∪ C) \ C