refine' ⟨Indep.basis_cl (hI.subset _), Indep.basis_cl (hI.subset (subset_insert _ _))⟩
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ M.Basis (insert a X) (M.cl (insert a X)) ∧ M.Basis (insert b X) (M.cl (insert b X))
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert a (insert b X)