simp_rw [le_antisymm_iff, le_er_iff, er_le_iff, truncateTo_indep_iff]
α : Type u_1
M✝ : Matroid α
E I B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X : Set α
⊢ (M.truncateTo k).er X = min (M.er X) k
α : Type u_1
M✝ : Matroid α
E I B : Set α
k✝ : ℕ∞
M : Matroid α
k : ℕ∞
X : Set α
⊢ (∀ {I : Set α}, I ⊆ X → M.Indep I ∧ I.encard ≤ k → I.encard ≤ min (M.er X) k) ∧
    ∃ I ⊆ X, (M.Indep I ∧ I.encard ≤ k) ∧ I.encard = min (M.er X) k