rw [← restrict_compl, basis'_restrict_iff, subset_diff, diff_eq, inter_comm M.E, ← inter_assoc,
  ← diff_eq, sdiff_eq_left.2 hCD] at hJ'
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 hJ' : (M ＼ D).Basis' J C
⊢ (M ／ C).Indep I ↔ (M ＼ D ／ C).Indep I
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