rw [Dep, comap_indep_iff, not_and, comap_ground_eq, Dep, image_subset_iff]
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
⊢ (N.comap f).Dep I ↔ N.Dep (f '' I) ∨ N.Indep (f '' I) ∧ ¬InjOn f I
α : Type u_1
β : Type u_2
f : α → β
E I s : Set α
M : Matroid α
N : Matroid β
⊢ (N.Indep (f '' I) → ¬InjOn f I) ∧ I ⊆ f ⁻¹' N.E ↔ ¬N.Indep (f '' I) ∧ I ⊆ f ⁻¹' N.E ∨ N.Indep (f '' I) ∧ ¬InjOn f I