Theorem: Matroid.Iso.dep_image_iff (Matroid/Equiv.lean)

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
D : Set ↑M.E
⊢ M.Dep ↑D ↔ N.Dep ↑(⇑e '' D)
Tactic:
rw [← not_indep_iff, e.indep_image_iff, not_indep_iff]
State after:
no goals