exact union_subset (hB.subset_ground.trans (contract_ground_subset_ground _ _)) hI.subset_ground
case refine'_2
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hI : M.Indep I
hB : (M ／ I).Basis J X
hi : Disjoint J I ∧ M.Indep (J ∪ I)
⊢ X ∪ I ⊆ M.E
no goals