rwa [h, hf_im' _ hI₀.subset_ground, ← e.indep_image_iff,
  Subset.image_val_preimage_val_eq hI₀.subset_ground]
case refine_2.refine_2
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
inst✝ : Nonempty (α → β)
f : α → β := fun x => if hx : x ∈ M.E then ↑(e ⟨x, hx⟩) else Classical.arbitrary (α → β) x
hf_im' : ∀ X ⊆ M.E, f '' X = ↑(⇑e '' M.E ↓∩ X)
hf_im : ∀ (X : Set ↑M.E), f '' ↑X = ↑(⇑e '' X)
I : Set ↑N.E
x✝ : ∃ I₀, M.Indep I₀ ∧ ↑I = f '' I₀
I₀ : Set α
hI₀ : M.Indep I₀
h : ↑I = f '' I₀
⊢ N.Indep ↑I
no goals