rw [dual_base_iff, unif_ground_eq, unif_base_iff (Nat.le_add_right _ _),
  unif_base_iff (Nat.le_add_left _ _),
  ← WithTop.add_right_cancel_iff (encard_ne_top_iff.2 B.toFinite),
  encard_diff_add_encard_of_subset (subset_univ _), Iff.comm,
  ← WithTop.add_left_cancel_iff (WithTop.coe_ne_top (a := a)), eq_comm]
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ (unif a (a + b))✶.Base B ↔ (unif b (a + b)).Base B
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
k : ℕ∞
a b a' b' : ℕ
B : Set (Fin (a + b))
x✝ : B ⊆ (unif a (a + b))✶.E
⊢ ↑a + ↑b = ↑a + B.encard ↔ univ.encard = ↑a + B.encard