simp only [← i.indep_image_iff, restrict_ground_eq, comp_apply, Equiv.ofInjective_apply,
  restrict_indep_iff, image_subset_iff, Subtype.coe_preimage_self, subset_univ, and_true]
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤ir M
I : Set ↑N.E
⊢ N.Indep ↑I ↔ (M ↾ range (val ∘ ⇑i)).Indep ↑(⇑(Equiv.ofInjective (fun y => (val ∘ ⇑i) y) ⋯) '' 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 ↑(⇑i '' I) ↔ M.Indep ((fun a => ↑a) '' ((fun a => (Equiv.ofInjective (fun y => ↑(i y)) ⋯) a) '' I))