rw [spanning_iff_er', erk_eq_er_ground, unifOn_ground_eq, unifOn_er_eq', unifOn_er_eq',
  le_min_iff, min_le_iff, min_le_iff, iff_true_intro (le_refl _), or_true, and_true, inter_self]
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
⊢ (unifOn E ↑k).Spanning X ↔ ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E
case intro
α : Type u_1
M : Matroid α
E I B X C : Set α
k✝ : ℕ∞
k : ℕ
⊢ (E.encard ≤ (X ∩ E).encard ∨ ↑k ≤ (X ∩ E).encard) ∧ X ⊆ E ↔ ↑k ≤ X.encard ∧ X ⊆ E ∨ X = E