rw [hBYdual.basis'.conn_eq_of_disjoint hBXdual.basis' disjoint_sdiff_right,
  hI.basis'.conn_eq_of_disjoint hJ.basis' disjoint_sdiff_right, hBX.erk_dual_restrict,
  union_diff_distrib, diff_eq_empty.2 inter_subset_left, empty_union,
  Basis.erk_dual_restrict (hBYb.compl_base_dual.basis_ground.basis_subset _ _)]
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
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ 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
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ ((BY ∩ (M.E \ X)) \ BX).encard = ((X \ BY ∪ (M.E \ X) \ BX) \ (M.E \ BY)).encard

α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ M.E \ BY ⊆ X \ BY ∪ (M.E \ X) \ BX

α : Type u_1
M✝ : Matroid α
B B' I I' J K X✝¹ Y : Set α
M : Matroid α
X✝ X : Set α
hX : X ⊆ M.E
BX : Set α
hBXb : M.Base BX
hI : M.Basis (BX ∩ X) X
hIBX : BX ∩ X ⊆ BX
hBXdual : M✶.Basis ((M.E \ X) \ BX) (M.E \ X)
BY : Set α
hBYb : M.Base BY
hJ : M.Basis (BY ∩ (M.E \ X)) (M.E \ X)
hBX : M.Basis BX (BX ∩ X ∪ BY ∩ (M.E \ X))
hIJE : M.Spanning (BX ∩ X ∪ BY ∩ (M.E \ X))
hBY : M.Basis BY (BX ∩ X ∪ BY ∩ (M.E \ X))
hJBY : BY ∩ (M.E \ X) ⊆ BY
hBYdual : M✶.Basis (X \ BY) X
⊢ X \ BY ∪ (M.E \ X) \ BX ⊆ M✶.E