rw [Dep, (hi.subset subset_union_left).contract_indep_iff, union_comm,
  and_iff_left hi] at h
α : 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✝
hi : M.Indep (C ∪ X)
⊢ False
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
h : ¬Disjoint X C ∧ X ⊆ (M ／ C).E
hC : autoParam (C ⊆ M.E) _auto✝
hi : M.Indep (C ∪ X)
⊢ False