From 7229a2cabe94dd1bbcbb340c1192b12b319fa6e2 Mon Sep 17 00:00:00 2001
From: Michael Rothgang <rothgami@math.hu-berlin.de>
Date: Sat, 20 Jan 2024 21:07:49 +0100
Subject: [PATCH] ToMathlib/LocallyFinite: use Type* and comment lemmas

Three will stay for now (explain why); fourth has been PRed.
---
 .../ToMathlib/Topology/LocallyFinite.lean     | 20 ++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/SphereEversion/ToMathlib/Topology/LocallyFinite.lean b/SphereEversion/ToMathlib/Topology/LocallyFinite.lean
index 1efb3493..93461b9b 100644
--- a/SphereEversion/ToMathlib/Topology/LocallyFinite.lean
+++ b/SphereEversion/ToMathlib/Topology/LocallyFinite.lean
@@ -3,24 +3,29 @@ import Mathlib.Topology.LocallyFinite
 
 open Function Set
 
-theorem LocallyFinite.smul_left {ι : Type _} {α : Type _} [TopologicalSpace α] {M : Type _}
-    {R : Type _} [Zero R] [Zero M] [SMulWithZero R M]
+-- these two lemmas require additional imports compared to what's in mathlib
+-- `Algebra.SMulWithZero` is not required in `Topology.LocallyFinite` so far;
+-- so it remains to find a nice home for these lemmas...
+theorem LocallyFinite.smul_left {ι : Type*} {α : Type*} [TopologicalSpace α] {M : Type*}
+    {R : Type*} [Zero R] [Zero M] [SMulWithZero R M]
     {s : ι → α → R} (h : LocallyFinite fun i => support <| s i) (f : ι → α → M) :
     LocallyFinite fun i => support (s i • f i) :=
   h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, zero_smul]
 
-theorem LocallyFinite.smul_right {ι : Type _} {α : Type _} [TopologicalSpace α] {M : Type _}
-    {R : Type _} [Zero R] [Zero M] [SMulZeroClass R M]
+theorem LocallyFinite.smul_right {ι : Type*} {α : Type*} [TopologicalSpace α] {M : Type*}
+    {R : Type*} [Zero R] [Zero M] [SMulZeroClass R M]
     {f : ι → α → M} (h : LocallyFinite fun i => support <| f i) (s : ι → α → R) :
     LocallyFinite fun i => support <| s i • f i :=
   h.subset fun i x ↦ mt <| fun h ↦ by rw [Pi.smul_apply', h, smul_zero]
 
 section
 
-variable {ι X : Type _} [TopologicalSpace X]
+variable {ι X : Type*} [TopologicalSpace X]
 
+-- TODO: remove this; we don't want to have this lemma in mathlib.
+-- See https://github.com/leanprover-community/mathlib4/pull/9813#discussion_r1455617707.
 @[to_additive]
-theorem LocallyFinite.exists_finset_mulSupport_eq {M : Type _} [CommMonoid M] {ρ : ι → X → M}
+theorem LocallyFinite.exists_finset_mulSupport_eq {M : Type*} [CommMonoid M] {ρ : ι → X → M}
     (hρ : LocallyFinite fun i => mulSupport <| ρ i) (x₀ : X) :
     ∃ I : Finset ι, (mulSupport fun i => ρ i x₀) = I := by
   use (hρ.point_finite x₀).toFinset
@@ -33,7 +38,8 @@ open scoped Topology
 
 open Filter
 
-theorem LocallyFinite.eventually_subset {ι X : Type _} [TopologicalSpace X] {s : ι → Set X}
+-- submitted as PR #9813
+theorem LocallyFinite.eventually_subset {ι X : Type*} [TopologicalSpace X] {s : ι → Set X}
     (hs : LocallyFinite s) (hs' : ∀ i, IsClosed (s i)) (x : X) :
     ∀ᶠ y in 𝓝 x, {i | y ∈ s i} ⊆ {i | x ∈ s i} := by
   filter_upwards [hs.iInter_compl_mem_nhds hs' x] with y hy i hi