Theorem: Matroid.Base.mem_coloop_iff_forall_not_mem_fundCct (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 α
hB : M.Base B
he : e ∈ B
⊢ M.Coloop e ↔ ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
Tactic:
refine ⟨fun h x hx heC ↦ (h.not_mem_circuit <| hB.fundCct_circuit hx) heC, 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 α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
⊢ 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 α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
h' : M.E \ {e} ⊆ M.cl (B \ {e})
⊢ M.Coloop e
Tactic:
rw [coloop_iff_not_mem_cl_compl (hB.subset_ground he)]
State after:
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
h' : M.E \ {e} ⊆ M.cl (B \ {e})
⊢ e ∉ M.cl (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 α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
h' : M.E \ {e} ⊆ M.cl (B \ {e})
⊢ e ∉ M.cl (M.E \ {e})
Tactic:
exact not_mem_subset (M.cl_subset_cl_of_subset_cl h') <| hB.indep.not_mem_cl_diff_of_mem he
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 α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
⊢ M.E \ {e} ⊆ M.cl (B \ {e})
Tactic:
rintro x ⟨hxE, hne : x ≠ e⟩
State after:
case intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.cl (B \ {e})

State before:
case intro
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
⊢ x ∈ M.cl (B \ {e})
Tactic:
obtain (hx | hx) := em (x ∈ B)
State after:
case intro.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∈ B
⊢ x ∈ M.cl (B \ {e})

case intro.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
⊢ x ∈ M.cl (B \ {e})

State before:
case intro.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
⊢ x ∈ M.cl (B \ {e})
Tactic:
have h_cct := (hB.fundCct_circuit ⟨hxE, hx⟩).mem_cl_diff_singleton_of_mem
  (M.mem_fundCct x B)
State after:
case intro.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ x ∈ M.cl (B \ {e})

State before:
case intro.inr
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ x ∈ M.cl (B \ {e})
Tactic:
refine (M.cl_subset_cl (subset_diff_singleton ?_ ?_)) h_cct
State after:
case intro.inr.refine_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ M.fundCct x B \ {x} ⊆ B

case intro.inr.refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ e ∉ M.fundCct x B \ {x}

State before:
case intro.inr.refine_2
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ e ∉ M.fundCct x B \ {x}
Tactic:
simp [hne.symm, h x ⟨hxE, hx⟩]
State after:
no goals

State before:
case intro.inl
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∈ B
⊢ x ∈ M.cl (B \ {e})
Tactic:
exact M.subset_cl (B \ {e}) (diff_subset.trans hB.subset_ground) ⟨hx, hne⟩
State after:
no goals

State before:
case intro.inr.refine_1
α : Type u_1
β : Type u_2
M N : Matroid α
e f : α
B L L' I X Y Z F C K : Set α
hB : M.Base B
he : e ∈ B
h : ∀ x ∈ M.E \ B, e ∉ M.fundCct x B
x : α
hxE : x ∈ M.E
hne : x ≠ e
hx : x ∉ B
h_cct : x ∈ M.cl (M.fundCct x B \ {x})
⊢ M.fundCct x B \ {x} ⊆ B
Tactic:
simpa using fundCct_subset_insert _ _
State after:
no goals