rwa [inter_eq_self_of_subset_left subset_union_right] at this
α : Type u_1
M✝ M' N : Matroid α
e f : α
I✝ J✝ R✝ B X Y Z K : Set α
M₀ M₁ M₂ M : Matroid α
C R : Set α
h : Disjoint C R
I : Set α
x✝ : I ⊆ (M ／ C ↾ R).E
J : Set α
hJ : (M ↾ (R ∪ C)).Basis' J C
this : M.Basis' J (C ∩ (R ∪ C))
⊢ M.Basis' J C
no goals