Theorem: Matroid.Parallel.dep_of_ne (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hne : e ≠ f
⊢ M.Dep {e, f}
Tactic:
rw [pair_comm, ← h.nonloop_left.indep.mem_cl_iff_of_not_mem hne.symm]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hne : e ≠ f
⊢ f ∈ M.cl {e}

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel e f
hne : e ≠ f
⊢ f ∈ M.cl {e}
Tactic:
exact h.symm.mem_cl
State after:
no goals