simp [← hC hIC]
case intro
α : Type u_1
M : Matroid α
C✝ C' I✝ X K C₁ C₂ R : Set α
e✝ f x y : α
β : Type u_2
N : Matroid β
e : M ≂ N
C : Set ↑M.E
I : Set ↑N.E
hI : N.Dep ↑I
hIC : I ⊆ ⇑e '' C
hC : I ⊆ ⇑e '' C → ⇑e ⁻¹' I = C
⊢ ↑I = ↑(⇑e '' C)
no goals