simp_rw [← dual_loop_iff_coloop, loop_iff_forall_mem_compl_base, dual_base_iff',
  dual_ground, mem_diff]
α : 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
α : 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