Theorem: Matroid.coloop_iff_forall_mem_cl_iff_mem (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 ↔ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.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 α
⊢ (∀ ⦃B : Set α⦄, M.Base B → e ∈ B) ↔ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.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 α
⊢ (∀ ⦃B : Set α⦄, M.Base B → e ∈ B) ↔ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Tactic:
refine' ⟨fun h ↦ _, fun h B hB ↦ _⟩
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 : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
⊢ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E

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 : (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
B : Set α
hB : M.Base B
⊢ e ∈ B

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 : (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
B : Set α
hB : M.Base B
⊢ e ∈ B
Tactic:
rw [← h.1, hB.cl_eq]
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 : (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
B : Set α
hB : M.Base B
⊢ 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 : (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
B : Set α
hB : M.Base B
⊢ e ∈ M.E
Tactic:
exact h.2
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 : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
⊢ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Tactic:
have heE := M.exists_base.elim (fun _ hB ↦ hB.subset_ground (h hB))
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 : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
⊢ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E

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 : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
⊢ (∀ (X : Set α), e ∈ M.cl X ↔ e ∈ X) ∧ e ∈ M.E
Tactic:
refine' ⟨fun X ↦ ⟨fun heX ↦ _, fun heX ↦ M.mem_cl_of_mem' heX⟩, heE⟩
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 : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
⊢ e ∈ X

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 : ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
⊢ e ∈ X
Tactic:
obtain ⟨I, hI⟩ := M.exists_basis (X ∩ M.E)
State after:
case refine'_1.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 ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ e ∈ X

State before:
case refine'_1.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 ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
I : Set α
hI : M.Basis I (X ∩ M.E)
⊢ e ∈ X
Tactic:
obtain ⟨B, hB, hIB⟩ := hI.indep.exists_base_superset
State after:
case refine'_1.intro.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 ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
I : Set α
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X

State before:
case refine'_1.intro.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 ∈ B
heE : e ∈ M.E
X : Set α
heX : e ∈ M.cl X
I : Set α
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X
Tactic:
rw [← cl_inter_ground, ← hI.cl_eq_cl] at heX
State after:
case refine'_1.intro.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 ∈ B
heE : e ∈ M.E
X I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X

State before:
case refine'_1.intro.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 ∈ B
heE : e ∈ M.E
X I : Set α
heX : e ∈ M.cl I
hI : M.Basis I (X ∩ M.E)
B : Set α
hB : M.Base B
hIB : I ⊆ B
⊢ e ∈ X
Tactic:
exact (hI.subset ((hB.indep.cl_inter_eq_self_of_subset hIB).subset ⟨heX, h hB⟩)).1
State after:
no goals