Theorem: Matroid.Coindep.delete_erk_eq (Matroid/Minor/Rank.lean)

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : M.Coindep X
⊢ (M ＼ X).erk = M.erk
Tactic:
rw [coindep_iff_cl_compl_eq_ground] at hX
State after:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : M.cl (M.E \ X) = M.E
⊢ (M ＼ X).erk = M.erk

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
hX : M.cl (M.E \ X) = M.E
⊢ (M ＼ X).erk = M.erk
Tactic:
rw [erk_eq_er_ground, delete_ground, delete_er_eq', diff_diff, union_self, ← er_cl_eq, hX,
  erk_eq_er_ground]
State after:
no goals