rw [skew_iff_cl_skew, conn_cl_cl, ← hI.cl_eq_cl, ← hJ.cl_eq_cl, ← skew_iff_cl_skew,
  ← conn_cl_cl, hI.indep.conn_eq hJ.indep, add_eq_zero_iff, encard_eq_zero,
  ← disjoint_iff_inter_eq_empty, erk_dual_restrict_eq_zero_iff,
  hI.indep.skew_iff_disjoint_union_indep hJ.indep]
case intro.intro
α : Type u_1
M✝ : Matroid α
B B' I✝ I' J✝ K X Y : Set α
M : Matroid α
hX : autoParam (X ⊆ M.E) _auto✝
hY : autoParam (Y ⊆ M.E) _auto✝
I : Set α
hI : M.Basis I X
J : Set α
hJ : M.Basis J Y
⊢ M.conn X Y = 0 ↔ M.Skew X Y
no goals