rw [(hb hB).1.erk_dual_restrict, union_diff_left,
  ← encard_diff_add_encard_inter (J \ (K \ I)) B, add_comm, inter_comm _ B,
  inter_diff_distrib_left, (hdj.mono_left hB.subset).inter_eq, diff_empty]
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
hb : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
B : Set α
hB : M.Basis B (M.cl I)
⊢ (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
no goals