Theorem: Matroid.loop_iff_forall_mem_compl_base (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.Loop e ↔ ∀ (B : Set α), M.Base B → e ∈ M.E \ B
Tactic:
refine' ⟨fun h B hB ↦ mem_of_mem_of_subset h _, fun 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 : M.Loop e
B : Set α
hB : M.Base B
⊢ M.cl ∅ ⊆ M.E \ B

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 : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
⊢ M.Loop 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 : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
⊢ M.Loop e
Tactic:
have he : e ∈ M.E := M.exists_base.elim (fun B hB ↦ (h B hB).1)
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 : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
⊢ M.Loop 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 : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
⊢ M.Loop e
Tactic:
rw [← singleton_dep, ← not_indep_iff]
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 : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
⊢ ¬M.Indep {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 : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
⊢ ¬M.Indep {e}
Tactic:
intro hei
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 : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
hei : M.Indep {e}
⊢ False

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 : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
hei : M.Indep {e}
⊢ False
Tactic:
obtain ⟨B, hB, heB⟩ := hei.exists_base_superset
State after:
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
hei : M.Indep {e}
B : Set α
hB : M.Base B
heB : {e} ⊆ B
⊢ False

State before:
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
h : ∀ (B : Set α), M.Base B → e ∈ M.E \ B
he : e ∈ M.E
hei : M.Indep {e}
B : Set α
hB : M.Base B
heB : {e} ⊆ B
⊢ False
Tactic:
exact (h B hB).2 (singleton_subset_iff.mp heB)
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 : M.Loop e
B : Set α
hB : M.Base B
⊢ M.cl ∅ ⊆ M.E \ B
Tactic:
rw [subset_diff, and_iff_right (cl_subset_ground _ _), disjoint_iff_inter_eq_empty,
  hB.indep.cl_inter_eq_self_of_subset (empty_subset B)]
State after:
no goals