rw [(M.empty_indep.basis_self.basis').conn_eq hI, empty_inter, encard_empty,
  erk_dual_restrict_eq_zero_iff.2 (by simpa using hI.indep), zero_add]
case intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J K X✝ Y : Set α
M : Matroid α
X I : Set α
hI : M.Basis' I X
⊢ M.conn ∅ X = 0
no goals