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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : M.Parallel e f
hne : e ≠ f
⊢ (M ／ e).Loop f
Tactic:
rw [loop_iff_mem_cl_empty, contract_elem, contract_loops_eq, mem_diff]
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
hef : M.Parallel e f
hne : e ≠ f
⊢ f ∈ M.cl {e} ∧ f ∉ {e}

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