simp [hJ.subset_ground]
case refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
I X : Set ↑M.E
hI : M.Indep ↑I
hIX : I ⊆ X
J : Set α
hJ : M.Indep J
hJX : J ⊆ ↑X
hIJ : I ⊆ Subtype.val ⁻¹' J
h : ⇑e '' I = ⇑e '' M.E ↓∩ J
⊢ ↑(⇑e.symm '' (⇑e '' M.E ↓∩ J)) = J
no goals