simp_rw [base_iff_maximal_indep, truncateTo_indep_iff, and_imp]
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ (M.truncateTo ↑k).Base B ↔ M.Indep B ∧ B.encard = ↑k
α : Type u_1
M : Matroid α
E I B : Set α
k✝ : ℕ∞
k : ℕ
h_rk : ↑k ≤ M.erk
⊢ ((M.Indep B ∧ B.encard ≤ ↑k) ∧ ∀ (I : Set α), M.Indep I → I.encard ≤ ↑k → B ⊆ I → B = I) ↔ M.Indep B ∧ B.encard = ↑k