Theorem: Matroid.Nonloop.cl_eq_of_mem_cl (Matroid/Loop.lean)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Nonloop e
hef : e ∈ M.cl {f}
⊢ M.cl {e} = M.cl {f}
Tactic:
rw [← cl_cl _ {f}, ← insert_eq_of_mem hef, cl_insert_cl_eq_cl_insert,
  ← cl_cl _ {e}, ← insert_eq_of_mem (he.mem_cl_singleton hef), cl_insert_cl_eq_cl_insert,
  pair_comm]
State after:
no goals