refine' fun _ _ ↦
  ⟨fun h ↦ h.base_of_base_subset hB₀ (subset_diff.mpr ⟨hB₀.subset_ground, _⟩), fun hB ↦
    hB.basis_of_subset diff_subset (diff_subset_diff_right subset_union_right)⟩
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
⊢ Disjoint B I → B ⊆ M.E → (M✶.Basis (M.E \ (B ∪ I)) (M.E \ I) ↔ M✶.Base (M.E \ (B ∪ I)))
case intro.intro
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
hIE : I ⊆ M.E
B₀ : Set α
hB₀ : M✶.Base B₀
hfk : B₀ ⊆ M✶.E \ I
x✝¹ : Disjoint B I
x✝ : B ⊆ M.E
h : M✶.Basis (M.E \ (B ∪ I)) (M.E \ I)
⊢ Disjoint B₀ I