refine ⟨C, ⟨hC, fun D hD hDC ↦ ?_⟩, rfl⟩
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
⊢ ∃ C₀, (M.Dep C₀ ∧ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀) ∧ f '' C = f '' C₀
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
⊢ D = C