have hBYb : M.Base BY := by rw [← basis_ground_iff, ← hIJE.cl_eq]; exact hBY.basis_cl_right
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBY : M.Basis BY (BX ∩ X ∪ J)
hJBY : J ⊆ BY
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)
case intro.intro.intro.intro.intro.intro
α : Type u_1
M✝ : Matroid α
B B' I I' J✝ K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
J : Set α
hJ : M.Basis J (M.E \ X)
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hBX : M.Basis BX (BX ∩ X ∪ J)
hIBX : BX ∩ X ⊆ BX
hIJE : M.Spanning (BX ∩ X ∪ J)
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBY : M.Basis BY (BX ∩ X ∪ J)
hJBY : J ⊆ BY
hBYb : M.Base BY
⊢ M.conn X (M.E \ X) = M✶.conn X (M.E \ X)