Theorem: Matroid.Basis.erk_dual_restrict (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hB : M.Basis I X
⊢ (M ↾ X)✶.erk = (X \ I).encard
Tactic:
rw [← Base.encard_compl_eq hB.restrict_base, restrict_ground_eq]
State after:
no goals