refine'
  h.eq_of_ssubset_of_subset (M.cl_flat _)
    ((ssubset_insert he.2).trans_subset (M.subset_cl _ _))
    (h.flat_right.cl_subset_of_subset (insert_subset he.1 h.ssubset.subset))
α : 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 : α
h : F₀ ⋖[M] F₁
he : e ∈ F₁ \ F₀
⊢ M.cl (insert e F₀) = F₁
α : 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 : α
h : F₀ ⋖[M] F₁
he : e ∈ F₁ \ F₀
⊢ insert e F₀ ⊆ M.E