obtain ⟨I₀, hI₀, hI₀ss⟩ := exists_subset_encard_eq (min_le_of_left_le (b := k) hI.encard.symm.le)
case intro.refine_2
α : Type u_1
M✝ : Matroid α
E I✝ B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X I : Set α
hI : M.Basis' I X
⊢ ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k
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