simp_rw [circuit_iff, delete_dep_iff, and_imp]
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ (M ＼ D).Circuit C ↔ M.Circuit C ∧ Disjoint C D
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ ((M.Dep C ∧ Disjoint C D) ∧ ∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔
    (M.Dep C ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C) ∧ Disjoint C D