rwa [hI.indep.insert_indep_iff_of_not_mem (not_mem_subset hI.subset heH), hI.cl_eq_cl,
  hH.flat.cl, mem_diff, and_iff_left heH]
case refine_1
α : 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.Indep (insert e I)
no goals