simp only [contract_cl_eq, singleton_union, diff_subset_iff, diff_union_self,
  cl_insert_cl_eq_cl_insert, union_diff_self, contract_nonloop_iff, cl_cl,
  union_eq_self_of_subset_left (M.cl_subset_cl (subset_insert _ X))]
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, (M ／ M.cl X).Nonloop e ∧ Y \ M.cl X ⊆ (M ／ M.cl X).cl {e}) ↔
    ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, e ∈ M.E \ M.cl X ∧ Y ⊆ M.cl (insert e X)) ↔ ∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)