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

State before:
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N✝ N : Matroid β
⊢ ∀ I ⊆ (N.comap id).E, (N.comap id).Indep I ↔ N.Indep I
Tactic:
simp [injective_id.injOn]
State after:
no goals