rw [truncateTo_indep_iff] at h
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h : (M.truncateTo k).Indep I
⊢ M.Indep I
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h : M.Indep I ∧ I.encard ≤ k
⊢ M.Indep I