rw [← ENat.some_eq_coe, unifOn_spanning_iff' (WithTop.coe_lt_top k).ne, and_iff_left hX,
  or_iff_left_iff_imp]
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hX : X ⊆ E
⊢ (unifOn E ↑k).Spanning X ↔ ↑k ≤ X.encard
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
hk : ↑k ≤ E.encard
hX : X ⊆ E
⊢ X = E → ↑k ≤ X.encard