Theorem: Matroid.Nonloop.parallel_iff_dep (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
hf : M.Nonloop f
hef : e ≠ f
⊢ M.Parallel e f ↔ M.Dep {e, f}
Tactic:
rw [← hf.indep.mem_cl_iff_of_not_mem hef, he.parallel_iff_mem_cl]
State after:
no goals