rintro _ D hD rfl hss
case mpr.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 α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
⊢ ∀ ⦃I : Set β⦄ (x : Set α), M.Dep x → I = f '' x → I ⊆ f '' C₀ → I = f '' C₀
case mpr.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 α
h : M.Dep C₀
h' : ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C₀ → I = C₀
D : Set α
hD : M.Dep D
hss : f '' D ⊆ f '' C₀
⊢ f '' D = f '' C₀