rw [nonloop_iff_mem_compl_loops, contract_ground, contract_loops_eq]
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
⊢ (M ／ C).Nonloop e ↔ e ∈ M.E \ M.cl C
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ : Set α
⊢ e ∈ (M.E \ C) \ (M.cl C \ C) ↔ e ∈ M.E \ M.cl C