rw [spanning_iff_cl, ← cl_insert_cl_eq_cl_insert, hI.cl_eq_cl, hH.flat.cl,
  hH.cl_eq_ground_of_ssuperset (ssubset_insert heH)]
case refine_2
α : Type u_1
M : Matroid α
I F X Y F' F₀ F₁ F₂ P L H H₁ H₂ H' B C K : Set α
e✝ f : α
hH : M.Hyperplane H
hI : M.Basis I H
e : α
he : e ∈ M.E
heH : e ∉ H
⊢ M.Spanning (insert e I)
no goals