refine eq_of_indep_iff_indep_forall truncateTo_ground_eq (fun I _ ↦ ?_)
α : Type u_1
M : Matroid α
E I B : Set α
k : ℕ∞
h_rk : M.erk ≤ k
⊢ M.truncateTo k = M
α : 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