exact ⟨_, hI₀.trans hI.subset, ⟨hI.indep.subset hI₀, hI₀ss.trans_le (min_le_right _ _)⟩, hI₀ss⟩
case intro.refine_2.intro.intro
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
I₀ : Set α
hI₀ : I₀ ⊆ I
hI₀ss : I₀.encard = min (M.er X) k
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
no goals