Theorem: Matroid.Coloop.insert_indep_of_indep (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 : Set α
he : M.Coloop e
hI : M.Indep I
⊢ M.Indep (insert e I)
Tactic:
refine (em (e ∈ I)).elim (fun h ↦ by rwa [insert_eq_of_mem h]) fun h ↦ ?_
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I)

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ M.Indep (insert e I)
Tactic:
rw [← hI.not_mem_cl_iff_of_not_mem h]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ e ∉ M.cl I

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∉ I
⊢ e ∉ M.cl I
Tactic:
exact he.not_mem_cl_of_not_mem h
State after:
no goals

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
he : M.Coloop e
hI : M.Indep I
h : e ∈ I
⊢ M.Indep (insert e I)
Tactic:
rwa [insert_eq_of_mem h]
State after:
no goals