exact ⟨Iso.mk (e.trans (Equiv.setCongr (by simp [hE, range_comp])))
  fun _ ↦ by simp [h, image_image, e], fun ⟨x,hx⟩ ↦ rfl⟩
case intro.intro.intro
α : Type u_1
β : Type u_2
β' : Type u_3
M : Matroid α
N : Matroid β
C D : Set α
i : N ≤i M
M₀ : Matroid α
hM₀ : M₀ ≤m M
hE : M₀.E = ↑(range ⇑i)
h : ∀ (I : Set ↑N.E), N.Indep ↑I ↔ M₀.Indep ↑(⇑i '' I)
e : ↑N.E ≃ ↑(range (val ∘ ⇑i)) := Equiv.ofInjective (val ∘ ⇑i) ⋯
⊢ ∃ e, ∀ (x : ↑N.E), inclusion ⋯ (e x) = i x
no goals