simp_rw [(M.cl_flat X).covBy_iff_eq_cl_insert, cl_insert_cl_eq_cl_insert]
α : 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] F ↔ ∃ e ∈ M.E \ M.cl X, F = M.cl (insert e X)
no goals