Update LeanCamCombi/ProbLYM.lean

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

Author: ctchou

LeanCamCombi/ProbLYM.lean

@@ -52,7 +52,7 @@ omit [Fintype α] in
 theorem card_numberingOn (s : Finset α) : card (NumberingOn s) = s.card.factorial := by
   simp only [NumberingOn]
   have h1 : card {x // x ∈ s} = card (Fin s.card) := by simp
-  have h2 : {x // x ∈ s} ≃ (Fin s.card) := by exact Fintype.equivOfCardEq h1
+  have h2 : {x // x ∈ s} ≃ Fin s.card := by exact Fintype.equivOfCardEq h1
   simp [Fintype.card_equiv h2]
 
 /-- `IsPrefix s f` means that the elements of `s` precede the elements of `sᶜ`