simp only [dual_ground, unifOn_ground_eq] at hBE
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 ⊆ (unifOn E ↑k)✶.E
⊢ (unifOn E ↑k)✶.Base B ↔ (unifOn E (E.encard - ↑k)).Base B
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