rw [relRank_eq_relRank_union, relRank, ← er_cl_eq, contract_cl_eq, union_assoc, union_self,
  ← hI.cl_eq_cl, ← relRank_eq_er_diff_contract, relRank_cl_right,
  relRank_eq_er_diff_contract, Indep.er]
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ M.relRank C X = (I \ C).encard
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Basis' I (X ∪ C)
hIC : M.Basis' (I ∩ C) C
⊢ (M ／ C).Indep (I \ C)