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

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
⊢ M.Parallel e f ↔ e ∈ M.cl {f}
Tactic:
refine ⟨Parallel.mem_cl, fun h ↦ ?_⟩
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
h : e ∈ M.cl {f}
⊢ M.Parallel e f

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
h : e ∈ M.cl {f}
⊢ M.Parallel e f
Tactic:
rw [cl_eq_parallel_class_union_loops, mem_union,  mem_setOf_eq, parallel_comm] at h
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
h : M.Parallel e f ∨ e ∈ M.cl ∅
⊢ M.Parallel e f

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
he : M.Nonloop e
h : M.Parallel e f ∨ e ∈ M.cl ∅
⊢ M.Parallel e f
Tactic:
exact h.elim id (fun h' ↦ (he.not_loop h').elim)
State after:
no goals