have hK' : (M ／ I).Indep (K \ I) := hK.diff_indep_contract_of_subset hJIK.2
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)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
⊢ K ⊆ J ∪ 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)
K : Set α
hK : M.Indep K
hJIK : J ⊆ K ∧ I ⊆ K
hKXI : K ⊆ X ∪ I
hK' : (M ／ I).Indep (K \ I)
⊢ K ⊆ J ∪ I