rw [Dep, and_iff_left (union_subset hC (h.subset_ground.trans diff_subset))]
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
⊢ M.Dep (C ∪ X)
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : (M ／ C).Dep X
hC : autoParam (C ⊆ M.E) _auto✝
⊢ ¬M.Indep (C ∪ X)