replace hB := hB.eq_of_subset_indep (e.symm.image_indep hI)
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
hB : M.Base ↑B
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
⊢ ↑(⇑e '' B) = ↑I
case intro
α : Type u_1
β : Type u_2
M : Matroid α
N : Matroid β
e : M ≂ N
B : Set ↑M.E
I : Set ↑N.E
hI : N.Indep ↑I
h' : ↑(⇑e '' B) ⊆ ↑I
hB : ↑B ⊆ ↑(⇑e.symm '' I) → ↑B = ↑(⇑e.symm '' I)
⊢ ↑(⇑e '' B) = ↑I