Theorem: Matroid.Indep.erk_dual_restrict_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 = 0
Tactic:
simp [hI.restrict_eq_freeOn]
State after:
no goals