simp [hB, comapOn_base_iff_of_surjOn h.surjOn, h']
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
E : Set α
h : BijOn f E N.E
B : Set α
h' : B ⊆ E → InjOn f B
hB : B ⊆ E
⊢ (N.comapOn E f).Base B ↔ N.Base (f '' B)
no goals