Theorem: Matroid.coloop_iff_forall_mem_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.Coloop e ↔ ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
Tactic:
simp_rw [← dual_loop_iff_coloop, loop_iff_forall_mem_compl_base, dual_base_iff',
  dual_ground, mem_diff]
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 (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B) ↔ ∀ ⦃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 α
⊢ (∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B) ↔ ∀ ⦃B : Set α⦄, M.Base B → e ∈ B
Tactic:
refine' ⟨fun h B hB ↦ _, fun h B ⟨hB, _⟩ ↦ ⟨hB.subset_ground (h hB), (h hB).2⟩⟩
State after:
α : 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 (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : 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 α
h : ∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : M.Base B
⊢ e ∈ B
Tactic:
rw [← diff_diff_cancel_left hB.subset_ground]
State after:
α : 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 (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : M.Base B
⊢ e ∈ M.E \ (M.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 α
h : ∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : M.Base B
⊢ e ∈ M.E \ (M.E \ B)
Tactic:
exact h (M.E \ B) ⟨(by rwa [diff_diff_cancel_left hB.subset_ground]), diff_subset⟩
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 α
h : ∀ (B : Set α), M.Base (M.E \ B) ∧ B ⊆ M.E → e ∈ M.E ∧ e ∉ B
B : Set α
hB : M.Base B
⊢ M.Base (M.E \ (M.E \ B))
Tactic:
rwa [diff_diff_cancel_left hB.subset_ground]
State after:
no goals