Theorem: Matroid.loopyOn_dep_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 : Set α
⊢ (loopyOn E).Dep D ↔ D.Nonempty ∧ D ⊆ E
Tactic:
simp [Dep, nonempty_iff_ne_empty]
State after:
no goals