obtain ⟨I, hI⟩ := (M ↾ R).exists_basis (X ∩ R)
case h
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E
case h.intro
α : Type u_1
ι : Type u_2
M✝ : Matroid α
F I✝ J X✝ Y B C R✝ : Set α
e✝ f x y : α
M : Matroid α
X R : Set α
e : α
I : Set α
hI : (M ↾ R).Basis I (X ∩ R)
⊢ e ∈ (M ↾ R).cl (X ∩ R) ↔ e ∈ M.cl (X ∩ R) ∩ R ∪ R \ M.E