exact (h.mapsTo.mono_left (show B ⊆ E by simpa)).image_subset
α : 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 α
hB : B ⊆ (N.comapOn E f)✶.E
⊢ f '' B ⊆ N.E
no goals