Theorem: Matroid.loopyOn_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 : α
E✝ D E : Set α
⊢ (loopyOn E).Circuit C ↔ ∃ e ∈ E, C = {e}
Tactic:
simp [← uniqueBaseOn_empty]
State after:
no goals