Theorem: Matroid.circuit_iff (Matroid/Circuit.lean)

State before:
α : 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 α⦄, M.Dep I → I ⊆ C → I = C
Tactic:
simp [Circuit, mem_minimals_setOf_iff, and_congr_right_iff, eq_comm (b := C)]
State after:
no goals