Theorem: Matroid.Indep.delete_erk_dual_eq (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hI : M.Indep I
⊢ (M ／ I)✶.erk = M✶.erk
Tactic:
rw [← hI.coindep.delete_erk_eq, contract_dual_eq_dual_delete]
State after:
no goals