Theorem: SimpleGraph.card_top_edgeSet (ExponentialRamsey/Prereq/Mathlib/Combinatorics/SimpleGraph/Basic.lean)

State before:
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
Tactic:
rw [Fintype.card_congr topEdgeSetEquiv, Sym2.card_subtype_not_diag]
State after:
no goals