Theorem: Matroid.cl_insert_coloop_eq (Matroid/Loop.lean)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
he : M.Coloop e
⊢ M.cl (insert e X) = insert e (M.cl X)
Tactic:
rw [ subset_antisymm_iff, insert_subset_iff, and_iff_left (M.cl_subset_cl (subset_insert _ _)),
  and_iff_left (M.mem_cl_of_mem' (mem_insert _ _)), ← union_singleton (s := M.cl X),
  ← diff_subset_iff, subset_singleton_iff]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
he : M.Coloop e
⊢ ∀ y ∈ M.cl (insert e X) \ M.cl X, y = e

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K X : Set α
he : M.Coloop e
⊢ ∀ y ∈ M.cl (insert e X) \ M.cl X, y = e
Tactic:
refine fun f hf ↦ (he.mem_of_mem_cl (cl_exchange hf).1).elim Eq.symm (fun heX ↦ False.elim ?_)
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f✝ : α
B L L' I X✝ Y Z F C K X : Set α
he : M.Coloop e
f : α
hf : f ∈ M.cl (insert e X) \ M.cl X
heX : e ∈ X
⊢ False

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f✝ : α
B L L' I X✝ Y Z F C K X : Set α
he : M.Coloop e
f : α
hf : f ∈ M.cl (insert e X) \ M.cl X
heX : e ∈ X
⊢ False
Tactic:
simp [insert_eq_of_mem heX] at hf
State after:
no goals