rw [truncateTo_indep_iff, and_iff_left_iff_imp]
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ (M.truncateTo k).Indep I ↔ M.Indep I
α : Type u_1
M : Matroid α
E I✝ B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
I : Set α
x✝ : I ⊆ (M.truncateTo k).E
⊢ M.Indep I → I.encard ≤ k