rw [← relRank_cl_left, relRank_eq_er_diff_contract, er_eq_one_iff
  (show Y \ (M.cl X) ⊆ (M ／ (M.cl X)).E from diff_subset_diff_left hY)]
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.relRank X Y = 1 ↔ ∃ 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, (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)