rw [encard_univ, PartENat.card_eq_coe_fintype_card, Fintype.card_fin,
  PartENat.withTopEquiv_natCast, ENat.some_eq_coe, eq_comm, Nat.cast_add]
case h.e'_2.h.e'_2
α : 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
⊢ univ.encard = ↑a + ↑b
no goals