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

State before:
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
h : N.Base ↑(⇑e '' B)
⊢ M.Base ↑B
Tactic:
simpa using e.symm.base_image h
State after:
no goals