refine' hH.ssuperset_eq_univ_of_flat (M.cl_flat _)
  ((ssubset_insert he.2).trans_subset (M.subset_cl _ _))
α : 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
he : e ∈ M.E \ H
⊢ M.cl (insert e H) = M.E
α : 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
he : e ∈ M.E \ H
⊢ insert e H ⊆ M.E