rw [hJ.contract_eq_contract_delete, delete_indep_iff, hJ.indep.contract_indep_iff,
  delete_indep_iff, ← contract_inter_ground_eq, hJ'.1.contract_eq_contract_delete,
  delete_indep_iff,  hJ'.1.indep.contract_indep_iff, disjoint_union_left, and_iff_right hI.2,
  and_iff_left (disjoint_of_subset_right diff_subset hI.1.2), and_iff_left hJ'.2.2,
  and_iff_left
  (disjoint_of_subset_right (diff_subset.trans inter_subset_left) hI.1.2)]
case intro
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C D : Set α
hCD : Disjoint C D
I : Set α
hI : (I ⊆ M.E ∧ Disjoint I C) ∧ Disjoint I D
J : Set α
hJ : (M ＼ D).Basis' J C
hJ' : M.Basis' J (C ∩ M.E) ∧ J ⊆ M.E ∧ Disjoint J D
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
no goals