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

State before:
α : Type u_1
M : Matroid α
C C' I X K C₁ C₂ R : Set α
e f x y : α
B : Set α
hC : M.Circuit C
⊢ M✶.Cocircuit C
Tactic:
rwa [cocircuit_def, dual_dual]
State after:
no goals