rw [rkPos_iff_empty_not_base, dual_base_iff, diff_empty, not_iff_comm, not_exists,
  ← ground_indep_iff_base, indep_iff_forall_subset_not_circuit]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ M✶.RkPos ↔ ∃ C, M.Circuit C
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ (∀ (x : Set α), ¬M.Circuit x) ↔ ∀ C ⊆ M.E, ¬M.Circuit C