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