Theorem: Matroid.comapOn_base_iff (Matroid/Map.lean)

State before:
α : 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
Tactic:
rw [comapOn, base_restrict_iff', comap_basis'_iff]
State after:
no goals