rw [erk_eq_er_ground, ← er_cl_eq _ X, h.cl_eq]
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.erk ≤ M.er X ∧ X ⊆ M.E
case refine'_1
α : Type u_1
ι : Type u_2
M N : Matroid α
I B X X' Y Y' Z R : Set α
n : ℕ∞
e f : α
inst✝ : M.FiniteRk
h : M.Spanning X
⊢ M.er M.E ≤ M.er M.E ∧ X ⊆ M.E