Theorem: Matroid.coloop_iff_diff_nonspanning (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 α
⊢ M.Coloop e ↔ ¬M.Spanning (M.E \ {e})
Tactic:
rw [coloop_iff_forall_mem_cl_iff_mem']
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ (∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E ↔ ¬M.Spanning (M.E \ {e})

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
⊢ (∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E ↔ ¬M.Spanning (M.E \ {e})
Tactic:
refine ⟨fun h hsp ↦ ?_, fun h ↦ ⟨fun X hX ↦ ⟨fun he ↦ ?_, fun he ↦ ?_⟩, by_contra fun h' ↦ h ?_⟩⟩
State after:
case refine_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : (∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
hsp : M.Spanning (M.E \ {e})
⊢ False

case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.Spanning (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
⊢ e ∈ X

case refine_3
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.Spanning (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ X
⊢ e ∈ M.cl X

case refine_4
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ¬M.Spanning (M.E \ {e})
h' : e ∉ M.E
⊢ M.Spanning (M.E \ {e})

State before:
case refine_4
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : ¬M.Spanning (M.E \ {e})
h' : e ∉ M.E
⊢ M.Spanning (M.E \ {e})
Tactic:
rw [spanning_iff_cl, diff_singleton_eq_self h', cl_ground]
State after:
no goals

State before:
case refine_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
h : (∀ X ⊆ M.E, e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
hsp : M.Spanning (M.E \ {e})
⊢ False
Tactic:
simpa [hsp.cl_eq.symm ▸ h.2] using h.1 (M.E \ {e})
State after:
no goals

State before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.Spanning (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
⊢ e ∈ X
Tactic:
rw [spanning_iff_ground_subset_cl] at h
State after:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
⊢ e ∈ X

State before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
⊢ e ∈ X
Tactic:
refine by_contra fun he' ↦ h ?_
State after:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl (M.E \ {e})

State before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl (M.E \ {e})
Tactic:
rw [← union_eq_self_of_subset_left (subset_diff_singleton hX he'), ← cl_union_cl_left_eq,
  ← insert_eq_of_mem he, ← union_singleton, union_assoc, union_diff_self, singleton_union,
  ← cl_ground]
State after:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.cl M.E ⊆ M.cl (M.cl X ∪ insert e (M.cl M.E))

State before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.cl M.E ⊆ M.cl (M.cl X ∪ insert e (M.cl M.E))
Tactic:
apply M.cl_subset_cl
State after:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl X ∪ insert e (M.cl M.E)

State before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl X ∪ insert e (M.cl M.E)
Tactic:
rw [cl_ground]
State after:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl X ∪ insert e M.E

State before:
case refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.E ⊆ M.cl (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ M.cl X
he' : e ∉ X
⊢ M.E ⊆ M.cl X ∪ insert e M.E
Tactic:
exact (subset_insert _ _).trans subset_union_right
State after:
no goals

State before:
case refine_3
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X✝ Y Z F C K : Set α
h : ¬M.Spanning (M.E \ {e})
X : Set α
hX : X ⊆ M.E
he : e ∈ X
⊢ e ∈ M.cl X
Tactic:
exact M.subset_cl X hX he
State after:
no goals