rw [← (hind I).contract_er_dual_eq,  ← (hind I').contract_er_dual_eq,
  restrict_contract_eq_contract_restrict _ (hb hI.basis_cl).2,
  restrict_contract_eq_contract_restrict _ (hb hI'b).2,
  union_diff_distrib, sdiff_eq_left.2 disjoint_sdiff_right,
  union_diff_distrib, sdiff_eq_left.2 (hdj.mono_left hI'b.subset), hb' hI.basis_cl, hb' hI'b]
case intro.intro
α : 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
hb' : ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (B ∩ J).encard + (M ／ (K \ I) ↾ (B ∪ J \ (K \ I)))✶.erk = (J \ (K \ I)).encard
hind : ∀ (Y : Set α), (M ↾ (Y ∪ J)).Indep (K \ I)
hI'b : M.Basis I' (M.cl I)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
no goals