Theorem: Matroid.coloop_iff_forall_mem_compl_circuit (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 α
inst✝ : M✶.RkPos
⊢ M.Coloop e ↔ ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
Tactic:
refine ⟨fun h C hC ↦ ⟨h.mem_ground, h.not_mem_circuit hC⟩, 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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
⊢ M.Coloop 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 α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
⊢ M.Coloop e
Tactic:
rw [coloop_iff_forall_mem_base]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
⊢ ∀ ⦃B : Set α⦄, M.Base B → e ∈ B

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
⊢ ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
Tactic:
refine fun B hB ↦ by_contra fun heB ↦ ?_
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
⊢ False

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
⊢ False
Tactic:
have heE : e ∈ M.E := Exists.elim M.exists_circuit (fun C hC ↦ (h C hC).1)
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
heE : e ∈ M.E
⊢ False

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
heE : e ∈ M.E
⊢ False
Tactic:
rw [← hB.cl_eq] at heE
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
heE : e ∈ M.cl B
⊢ False

State before:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B✝ L L' I X Y Z F C K : Set α
inst✝ : M✶.RkPos
h : ∀ (C : Set α), M.Circuit C → e ∈ M.E \ C
B : Set α
hB : M.Base B
heB : e ∉ B
heE : e ∈ M.cl B
⊢ False
Tactic:
exact (h _ (hB.indep.fundCct_circuit ⟨heE, heB⟩)).2 (mem_fundCct _ _ _)
State after:
no goals