rintro ⟨I, hI, rfl⟩
α : Type u_1
β : Type u_2
f✝ : α → β
E I s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
D : Set β
⊢ (∃ D₀, M.Dep D₀ ∧ D = ⇑f '' D₀) → M.Dep (⇑f.symm '' D)
case intro.intro
α : Type u_1
β : Type u_2
f✝ : α → β
E I✝ s : Set α
M : Matroid α
N : Matroid β
f : α ≃ β
I : Set α
hI : M.Dep I
⊢ M.Dep (⇑f.symm '' (⇑f '' I))