rw [dual_base_iff', unifOn_base_iff' ((tsub_le_self.trans_lt hE.encard_lt_top).ne) (by simp) hBE,
  unifOn_ground_eq, and_iff_left hBE, unifOn_base_iff hlt.le diff_subset,
  ← WithTop.add_right_cancel_iff (hE.subset hBE).encard_lt_top.ne,
  encard_diff_add_encard_of_subset hBE, Iff.comm, eq_comm, add_comm,
  ← WithTop.add_right_cancel_iff (hlt.trans_le le_top).ne, tsub_add_cancel_of_le hlt.le]
case inr.intro.inr
α : Type u_1
M : Matroid α
E I B✝ X C : Set α
hE : E.Finite
k : ℕ
hlt : ↑k < E.encard
B : Set α
hBE : B ⊆ E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B
no goals