Use Numbering to define NumberingOn

Author: ctchou

LeanCamCombi/ProbLYM.lean

@@ -43,7 +43,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 α]
 
@@ -52,10 +52,7 @@ theorem card_Numbering : card (Numbering α) = (card α).factorial := by
 
 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
-  simp [Fintype.card_equiv h2]
+  simp only [NumberingOn, card_Numbering, card_coe]
 
 /-- `IsPrefix s f` means that the elements of `s` precede the elements of `sᶜ`
 in the numbering `f`. -/
@@ -68,7 +65,8 @@ theorem subset_IsPrefix_IsPrefix {s1 s2 : Finset α} {f : Numbering α}
   intro a h_as1
   exact (h_s2 a).mpr (lt_of_lt_of_le ((h_s1 a).mp h_as1) h_card)
 
-def equiv_IsPrefix_NumberingOn2 (s : Finset α) : {f // IsPrefix s f} ≃ NumberingOn s × NumberingOn sᶜ where
+def equiv_IsPrefix_NumberingOn2' (s : Finset α) :
+    {f // IsPrefix s f} ≃ ({x // x ∈ s} ≃ Fin s.card) × ({x // x ∈ sᶜ} ≃ Fin sᶜ.card) where
   toFun := fun ⟨f, hf⟩ ↦
     ({
       toFun := fun ⟨x, hx⟩ ↦ ⟨f x, by rwa [← hf x]⟩
@@ -141,6 +139,11 @@ def equiv_IsPrefix_NumberingOn2 (s : Finset α) : {f // IsPrefix s f} ≃ Number
       rw [Finset.mem_compl] at hx
       simp [hx]
 
+def equiv_IsPrefix_NumberingOn2 (s : Finset α) :
+    {f // IsPrefix s f} ≃ NumberingOn s × NumberingOn sᶜ := by
+  simp only [NumberingOn, Numbering, card_coe]
+  exact equiv_IsPrefix_NumberingOn2' s
+
 instance (s : Finset α) :
     DecidablePred fun f ↦ (IsPrefix s f) := by
   intro f ; exact Classical.propDecidable ((fun f ↦ IsPrefix s f) f)