rw [cl_covBy_iff]
α : 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 : α
⊢ M.cl X ⋖[M] M.cl Y ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y
α : 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 : α
⊢ (∃ e ∈ M.E \ M.cl X, M.cl Y = M.cl (insert e X)) ↔ ∃ e ∈ M.E, e ∈ Y ∧ e ∉ M.cl X ∧ M.cl (insert e X) = M.cl Y