rw [Fintype.card_congr topEdgeSetEquiv, Sym2.card_subtype_not_diag]
V : Type u_1
V' : Type u_2
G : SimpleGraph V
K : Type u_3
K' : Type u_4
inst✝¹ : DecidableEq V
inst✝ : Fintype V
⊢ Fintype.card ↑(edgeSet ⊤) = Nat.choose (Fintype.card V) 2
no goals