Theorem: Matroid.Cocircuit.delete_cocircuit (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ D : Set α
hK : M.Cocircuit K
hD : D ⊂ K
⊢ (M ＼ D).Cocircuit (K \ D)
Tactic:
rw [cocircuit_def, delete_dual_eq_dual_contract]
State after:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ D : Set α
hK : M.Cocircuit K
hD : D ⊂ K
⊢ (M✶ ／ D).Circuit (K \ D)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y Z K C C₁ C₂ D : Set α
hK : M.Cocircuit K
hD : D ⊂ K
⊢ (M✶ ／ D).Circuit (K \ D)
Tactic:
exact hK.circuit.contract_circuit hD
State after:
no goals