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

State before:
α : Type u_1
M N : Matroid α
I J C D X Y Z : Set α
e f : α
⊢ (M ＼ D).rFin X ↔ M.rFin (X \ D)
Tactic:
rw [← er_lt_top_iff, delete_er_eq', er_lt_top_iff]
State after:
no goals