Theorem: Matroid.Parallel'.loop_of_loop (Matroid/Parallel.lean)

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
⊢ M.Loop f
Tactic:
have h' := h.cl_eq_cl
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {e} = M.cl {f}
⊢ M.Loop f

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {e} = M.cl {f}
⊢ M.Loop f
Tactic:
rw [he.cl, eq_comm] at h'
State after:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {f} = M.cl ∅
⊢ M.Loop f

State before:
α : Type u_1
M N : Matroid α
e f g : α
I X P D : Set α
h : M.Parallel' e f
he : M.Loop e
h' : M.cl {f} = M.cl ∅
⊢ M.Loop f
Tactic:
rwa [loop_iff_cl_eq_cl_empty h.mem_ground_right]
State after:
no goals