rw [← uniqueBaseOn_inter_ground_eq I E, ← cl_inter_ground _ X, uniqueBaseOn_ground,
  ← hb.cl_eq_cl, hb.indep.mem_cl_iff, dep_iff, uniqueBaseOn_indep_iff', insert_subset_iff,
  uniqueBaseOn_ground, inter_assoc, inter_self,  and_iff_left inter_subset_right,
  ← inter_inter_distrib_right, inter_assoc, inter_union_distrib_right, inter_comm I,
  inter_union_diff, insert_subset_iff, inter_comm X, inter_assoc,
  and_iff_left inter_subset_left, mem_inter_iff]
case h
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ e ∈ (uniqueBaseOn I E).cl X ↔ e ∈ X ∩ I ∩ E ∪ E \ I
case h
α : Type u_1
ι : Type u_2
M : Matroid α
F I✝ J X✝ Y B C R : Set α
e✝ f x y : α
I E X : Set α
hb : (uniqueBaseOn (I ∩ E) E).Basis (X ∩ E ∩ (I ∩ E)) (X ∩ E)
e : α
⊢ ¬(e ∈ E ∧ e ∈ I) ∧ e ∈ E ∨ e ∈ E ∩ (I ∩ X) ↔ e ∈ (X ∪ E \ I) ∩ E