Theorem: Matroid.erk_dual_restrict_eq_zero_iff (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
⊢ (M ↾ I)✶.erk = 0 ↔ M.Indep I
Tactic:
rw [← restrict_eq_freeOn_iff, erk_eq_zero_iff, dual_ground, restrict_ground_eq,
  eq_comm, eq_dual_comm, loopyOn_dual_eq]
State after:
no goals