simp only [image_image]
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ↑(⇑i '' I) ↔ M.Indep ((fun a => ↑a) '' ((fun a => (Equiv.ofInjective (fun y => ↑(i y)) ⋯) a) '' I))
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ M.Indep ((fun x => ↑(i x)) '' I) ↔ M.Indep ((fun x => ↑((Equiv.ofInjective (fun y => ↑(i y)) ⋯) x)) '' I)