chore(Archive/Wiedijk100Theorems/BirthdayProblem): cleanup (leanprover-community#37679)

We remove some redundant instances, and a redundant `open scoped`.

Author: vihdzp

Archive/Wiedijk100Theorems/BirthdayProblem.lean

@@ -17,11 +17,9 @@ in terms of injective functions. The general result about `Fintype.card (α ↪
 uses is `Fintype.card_embedding_eq`.
 -/
 
-
 namespace Theorems100
 
 local notation "|" x "|" => Finset.card x
-
 local notation "‖" x "‖" => Fintype.card x
 
 /-- **Birthday Problem**: set cardinality interpretation. -/
@@ -30,38 +28,23 @@ theorem birthday :
   simp only [Fintype.card_fin, Fintype.card_embedding_eq, Fintype.card_fun]
   decide
 
-section MeasureTheory
-
 open MeasureTheory ProbabilityTheory
 
-open scoped ProbabilityTheory ENNReal
-
 variable {n m : ℕ}
 
-/- In order for Lean to understand that we can take probabilities in `Fin 23 → Fin 365`, we must
-tell Lean that there is a `MeasurableSpace` structure on the space. Note that this instance
-is only for `Fin m` - Lean automatically figures out that the function space `Fin n → Fin m`
-is _also_ measurable, by using `MeasurableSpace.pi`, and furthermore that all sets are measurable,
-from `MeasurableSingletonClass.pi`. -/
-instance : MeasurableSpace (Fin m) :=
-  ⊤
-
-instance : MeasurableSingletonClass (Fin m) :=
-  ⟨fun _ => trivial⟩
-
 /- We then endow the space with a canonical measure, which is called ℙ.
 We define this to be the conditional counting measure. -/
 noncomputable instance measureSpace : MeasureSpace (Fin n → Fin m) :=
   ⟨uniformOn Set.univ⟩
 
-theorem FinFin.measure_apply {s : Set <| Fin n → Fin m} :
+theorem Fin.measure_apply {s : Set <| Fin n → Fin m} :
     ℙ s = |s.toFinite.toFinset| / ‖Fin n → Fin m‖ := by
   rw [volume, measureSpace, uniformOn_univ, Measure.count_apply_finite]
 
 /-- **Birthday Problem**: first probabilistic interpretation. -/
 theorem birthday_measure :
-    ℙ ({f | (Function.Injective f)} : Set ((Fin 23) → (Fin 365))) < 1 / 2 := by
-  rw [FinFin.measure_apply]
+    ℙ ({f | f.Injective} : Set (Fin 23 → Fin 365)) < 1 / 2 := by
+  rw [Fin.measure_apply]
   generalize_proofs hfin
   have : |hfin.toFinset| = 42200819302092359872395663074908957253749760700776448000000 := by
     trans ‖Fin 23 ↪ Fin 365‖
@@ -76,6 +59,4 @@ theorem birthday_measure :
     simp only [Fintype.card_pi, Fintype.card_fin, Finset.prod_const, Finset.card_univ]
     norm_num
 
-end MeasureTheory
-
 end Theorems100