no goals
α : Type u_1
β : Type ?u.78623
inst✝ : DecidableEq α
s : Finset α
⊢ Finset.card (image Quotient.mk' (offDiag s)) = Nat.choose (Finset.card s) 2
rw [Nat.choose_two_right, mul_tsub, mul_one, ← offDiag_card,
  Nat.div_eq_of_eq_mul_right zero_lt_two (two_mul_card_image_offDiag s).symm]