rw [le_iff_eq_or_lt, lt_iff_not_le, ENat.one_le_iff_ne_zero, not_not, relRank_eq_one_iff,
  relRank_eq_zero_iff]
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ M.relRank X Y ≤ 1 ↔ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hYne : Y.Nonempty
hY : autoParam (Y ⊆ M.E) _auto✝
⊢ (∃ e ∈ Y \ M.cl X, Y ⊆ M.cl (insert e X)) ∨ Y ⊆ M.cl X ↔ ∃ e ∈ Y, Y ⊆ M.cl (insert e X)