Update LeanCamCombi/ProbLYM.lean

Co-authored-by: Yaël Dillies <[email protected]>

Author: ctchou

LeanCamCombi/ProbLYM.lean

@@ -41,7 +41,7 @@ in mathlib because we need the special property `set_prefix_subset` below. -/
 def Numbering (α : Type*) [Fintype α] := α ≃ Fin (card α)
 
 @[reducible]
-def NumberingOn {α : Type*} (s : Finset α) := {x // x ∈ s} ≃ Fin s.card
+def NumberingOn {α : Type*} (s : Finset α) := Numbering s
 
 variable {α : Type*} [Fintype α] [DecidableEq α]