refine' hi.2.basis_of_maximal_subset (union_subset_union_left _ hB.subset) _ _
α : 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)
⊢ M.Basis (J ∪ I) (X ∪ I)
case refine'_1
α : 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)
⊢ ∀ ⦃J_1 : Set α⦄, M.Indep J_1 → J ∪ I ⊆ J_1 → J_1 ⊆ X ∪ I → J_1 ⊆ J ∪ I

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