use fun h => ⟨⟨B, hB, h.finite_of_indep_subset hB.indep hB.subset_ground⟩⟩
case intro
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.rFin M.E ↔ M.FiniteRk
case mpr
α : Type u_1
ι : Type u_2
M N : Matroid α
I B✝ X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
B : Set α
hB : M.Base B
⊢ M.FiniteRk → M.rFin M.E