have hIE : insert e I ⊆ (N.comap f).E := by
    simp_rw [comap_ground_eq, ← image_subset_iff]
    exact (image_subset _ (insert_subset heX h.2.1)).trans h.1.subset_ground
case refine_2.refine_2
α : 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
⊢ (N.comap f).Dep (insert e I)
case refine_2.refine_2
α : 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
hIE : insert e I ⊆ (N.comap f).E
⊢ (N.comap f).Dep (insert e I)