exact h _ hD rfl (image_subset f hDC)
case mp.intro.intro.intro
α : Type u_1
M : Matroid α
C✝ C' I X K C₁ C₂ R : Set α
e f✝ x y : α
β : Type u_2
f : α → β
hf : InjOn f M.E
C : Set α
hC : M.Dep C
h : ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C → I = f '' C
D : Set α
hD : M.Dep D
hDC : D ⊆ C
⊢ f '' D = f '' C
no goals