rw [ subset_antisymm_iff, insert_subset_iff, and_iff_left (M.cl_subset_cl (subset_insert _ _)),
  and_iff_left (M.mem_cl_of_mem' (mem_insert _ _)), ← union_singleton (s := M.cl X),
  ← diff_subset_iff, subset_singleton_iff]
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
he : M.Coloop e
⊢ M.cl (insert e X) = insert e (M.cl X)
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
he : M.Coloop e
⊢ ∀ y ∈ M.cl (insert e X) \ M.cl X, y = e