simpa [union_eq_self_of_subset_right hIB]
α : 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
x✝ : Disjoint J I ∧ ∃ B, M.Base B ∧ J ⊆ B ∧ I ⊆ B
hdj : Disjoint J I
B : Set α
hB : M.Base B
hJB : J ⊆ B
hIB : I ⊆ B
⊢ M.Base (B \ I ∪ I)
no goals