rw [loopEquiv_iff_union_eq_union, union_assoc, union_eq_self_of_subset_left hL]
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
hL : L ⊆ M.cl ∅
⊢ M.LoopEquiv X (X ∪ L)
no goals