simp_rw [circuit_iff, dep_iff, and_congr_right_iff, ssubset_iff_subset_ne, and_imp]
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ M.Circuit C ↔ M.Dep C ∧ ∀ ⦃I : Set α⦄, I ⊂ C → M.Indep I
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
⊢ ¬M.Indep C →
    C ⊆ M.E → ((∀ ⦃I : Set α⦄, ¬M.Indep I → I ⊆ M.E → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, I ⊆ C → I ≠ C → M.Indep I)