rw [comapOn, base_restrict_iff', comap_basis'_iff]
α : Type u_1
β : Type u_2
f : α → β
E✝ I s : Set α
M : Matroid α
N : Matroid β
B E : Set α
⊢ (N.comapOn E f).Base B ↔ N.Basis' (f '' B) (f '' E) ∧ B ⊆ E ∧ InjOn f B
no goals