simp_rw [comap_ground_eq, ← image_subset_iff]
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ insert e I ⊆ (N.comap f).E
α : Type u_1
β : Type u_2
f : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
I X : Set α
h : N.Basis (f '' I) (f '' X) ∧ I ⊆ X ∧ InjOn f I
e : α
x✝ : e ∈ X \ I
heX : e ∈ X
heI : e ∉ I
⊢ f '' insert e I ⊆ N.E