rw [circuit_iff_forall_ssubset, and_congr_right_iff]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Circuit C ↔ M.Dep C ∧ ∀ e ∈ C, M.Indep (C \ {e})
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Dep C → ((∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I) ↔ ∀ e ∈ C, M.Indep (C \ {e}))