rw [← hI.cl_eq_cl, ← M.cl_inter_ground (X ∩ R), ← hI'.cl_eq_cl, mem_union, mem_inter_iff,
  hI'.indep.mem_cl_iff, hI.indep.mem_cl_iff, restrict_dep_iff, insert_subset_iff,
  dep_iff, insert_subset_iff, and_iff_left hI'.indep.subset_ground, mem_diff,
  and_iff_left (show I ⊆ R from hI.indep.subset_ground)]
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)
hI' : M.Basis I (X ∩ R ∩ M.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)
hI' : M.Basis I (X ∩ R ∩ M.E)
⊢ ¬M.Indep (insert e I) ∧ e ∈ R ∨ e ∈ I ↔ (¬M.Indep (insert e I) ∧ e ∈ M.E ∨ e ∈ I) ∧ e ∈ R ∨ e ∈ R ∧ e ∉ M.E