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

State before:
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅
Tactic:
by_cases he : M.Nonloop e
State after:
case pos
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : M.Nonloop e
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅

case neg
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : ¬M.Nonloop e
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅

State before:
case neg
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : ¬M.Nonloop e
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅
Tactic:
rw [not_nonloop_iff_cl.1 he, diff_self, eq_empty_iff_forall_not_mem]
State after:
case neg
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : ¬M.Nonloop e
⊢ ∀ (x : α), x ∉ {f | M.Parallel e f}

State before:
case neg
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : ¬M.Nonloop e
⊢ ∀ (x : α), x ∉ {f | M.Parallel e f}
Tactic:
exact fun f hf ↦ he (Parallel.nonloop_left hf)
State after:
no goals

State before:
case pos
α : Type u_1
M✝ N : Matroid α
e✝ f g : α
I X P D : Set α
M : Matroid α
e : α
he : M.Nonloop e
⊢ {f | M.Parallel e f} = M.cl {e} \ M.cl ∅
Tactic:
rw [Parallel, parallelClasses, Partition.rel_congr,
  Partition.setOf_rel_eq_partOf, (M.cl_flat ∅).partOf_covByPartition_eq,
  cl_insert_cl_eq_cl_insert, insert_emptyc_eq]
State after:
no goals