chore(Topology): remove autoImplicit from most remaining files (#9865)

grunweg · grunweg · commit d1054e16d3bc · 2024-01-24T14:31:54.000Z
diff --git a/Mathlib/Topology/Algebra/Order/Compact.lean b/Mathlib/Topology/Algebra/Order/Compact.lean
@@ -27,9 +27,6 @@ We also prove that the image of a closed interval under a continuous map is a cl
 compact, extreme value theorem
 -/
 
-set_option autoImplicit true
-
-
 open Filter OrderDual TopologicalSpace Function Set
 
 open scoped Filter Topology
@@ -56,6 +53,8 @@ class CompactIccSpace (α : Type*) [TopologicalSpace α] [Preorder α] : Prop wh
 
 export CompactIccSpace (isCompact_Icc)
 
+variable {α : Type*}
+
 -- porting note: new lemma; TODO: make it the definition
 lemma CompactIccSpace.mk' [TopologicalSpace α] [Preorder α]
     (h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)) : CompactIccSpace α where
diff --git a/Mathlib/Topology/Algebra/Order/Rolle.lean b/Mathlib/Topology/Algebra/Order/Rolle.lean
@@ -14,7 +14,7 @@ import Mathlib.Topology.LocalExtr
 # Rolle's Theorem (topological part)
 
 In this file we prove the purely topological part of Rolle's Theorem:
-a function that is continuous on an interval $[a, b]$, $a<b$,
+a function that is continuous on an interval $[a, b]$, $a < b$,
 has a local extremum at a point $x ∈ (a, b)$ provided that $f(a)=f(b)$.
 We also prove several variations of this statement.
 
@@ -25,11 +25,9 @@ to prove several versions of Rolle's Theorem from calculus.
 local minimum, local maximum, extremum, Rolle's Theorem
 -/
 
-set_option autoImplicit true
-
 open Filter Set Topology
 
-variable
+variable {X Y : Type*}
   [ConditionallyCompleteLinearOrder X] [DenselyOrdered X] [TopologicalSpace X] [OrderTopology X]
   [LinearOrder Y] [TopologicalSpace Y] [OrderTopology Y]
   {f : X → Y} {a b : X} {l : Y}
diff --git a/Mathlib/Topology/Algebra/Star.lean b/Mathlib/Topology/Algebra/Star.lean
@@ -17,8 +17,6 @@ This file defines the `ContinuousStar` typeclass, along with instances on `Pi`,
 `MulOpposite`, and `Units`.
 -/
 
-set_option autoImplicit true
-
 open Filter Topology
 
 /-- Basic hypothesis to talk about a topological space with a continuous `star` operator. -/
@@ -31,7 +29,7 @@ export ContinuousStar (continuous_star)
 
 section Continuity
 
-variable [TopologicalSpace R] [Star R] [ContinuousStar R]
+variable {α R : Type*} [TopologicalSpace R] [Star R] [ContinuousStar R]
 
 theorem continuousOn_star {s : Set R} : ContinuousOn star s :=
   continuous_star.continuousOn
@@ -84,6 +82,8 @@ end Continuity
 
 section Instances
 
+variable {R S ι : Type*}
+
 instance [Star R] [Star S] [TopologicalSpace R] [TopologicalSpace S] [ContinuousStar R]
     [ContinuousStar S] : ContinuousStar (R × S) :=
   ⟨(continuous_star.comp continuous_fst).prod_mk (continuous_star.comp continuous_snd)⟩
diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean
@@ -29,9 +29,6 @@ equipped with the subspace topology.
 
 -/
 
-set_option autoImplicit true
-
-
 open Set Filter Function Topology Filter
 
 variable {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
@@ -753,7 +750,7 @@ theorem ContinuousWithinAt.mono_of_mem {f : α → β} {s t : Set α} {x : α}
   h.mono_left (nhdsWithin_le_of_mem hs)
 #align continuous_within_at.mono_of_mem ContinuousWithinAt.mono_of_mem
 
-theorem continuousWithinAt_congr_nhds {f : α → β} (h : 𝓝[s] x = 𝓝[t] x) :
+theorem continuousWithinAt_congr_nhds {f : α → β} {s t : Set α} {x : α} (h : 𝓝[s] x = 𝓝[t] x) :
     ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x := by
   simp only [ContinuousWithinAt, h]
 
diff --git a/Mathlib/Topology/CountableSeparatingOn.lean b/Mathlib/Topology/CountableSeparatingOn.lean
@@ -13,7 +13,7 @@ In this file we show that a T₀ topological space with second countable
 topology has a countable family of open (or closed) sets separating the points.
 -/
 
-set_option autoImplicit true
+variable {X : Type*}
 
 open Set TopologicalSpace
 
diff --git a/Mathlib/Topology/ExtremallyDisconnected.lean b/Mathlib/Topology/ExtremallyDisconnected.lean
@@ -30,8 +30,6 @@ compact Hausdorff spaces.
 [Gleason, *Projective topological spaces*][gleason1958]
 -/
 
-set_option autoImplicit true
-
 noncomputable section
 
 open Classical Function Set
@@ -286,7 +284,7 @@ end
 
 -- Note: It might be possible to use Gleason for this instead
 /-- The sigma-type of extremally disconnected spaces is extremally disconnected. -/
-instance instExtremallyDisconnected {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
+instance instExtremallyDisconnected {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
     [h₀ : ∀ i, ExtremallyDisconnected (π i)] : ExtremallyDisconnected (Σ i, π i) := by
   constructor
   intro s hs
diff --git a/Mathlib/Topology/Homotopy/Basic.lean b/Mathlib/Topology/Homotopy/Basic.lean
@@ -54,14 +54,11 @@ and for `ContinuousMap.homotopic` and `ContinuousMap.homotopic_rel`, we also def
 - [HOL-Analysis formalisation](https://isabelle.in.tum.de/library/HOL/HOL-Analysis/Homotopy.html)
 -/
 
-set_option autoImplicit true
-
-
 noncomputable section
 
 universe u v w x
 
-variable {F : Type*} {X : Type u} {Y : Type v} {Z : Type w} {Z' : Type x}
+variable {F : Type*} {X : Type u} {Y : Type v} {Z : Type w} {Z' : Type x} {ι : Type*}
 
 variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace Z']
 
diff --git a/Mathlib/Topology/LocallyConstant/Algebra.lean b/Mathlib/Topology/LocallyConstant/Algebra.lean
@@ -17,8 +17,6 @@ on the type of locally constant functions.
 
 -/
 
-set_option autoImplicit true
-
 namespace LocallyConstant
 
 variable {X Y : Type*} [TopologicalSpace X]
@@ -153,6 +151,8 @@ instance [SemigroupWithZero Y] : SemigroupWithZero (LocallyConstant X Y) :=
 instance [CommSemigroup Y] : CommSemigroup (LocallyConstant X Y) :=
   Function.Injective.commSemigroup DFunLike.coe DFunLike.coe_injective' fun _ _ => rfl
 
+variable {α R : Type*}
+
 @[to_additive]
 instance smul [SMul α Y] : SMul α (LocallyConstant X Y) where
   smul n f := f.map (n • ·)
@@ -341,7 +341,7 @@ end Eval
 
 section Comap
 
-variable [TopologicalSpace Y]
+variable [TopologicalSpace Y] {Z : Type*}
 
 /-- `LocallyConstant.comap` as a `MulHom`. -/
 @[to_additive (attr := simps) "`LocallyConstant.comap` as an `AddHom`."]
diff --git a/Mathlib/Topology/Order.lean b/Mathlib/Topology/Order.lean
@@ -45,9 +45,6 @@ of sets in `α` (with the reversed inclusion ordering).
 finer, coarser, induced topology, coinduced topology
 -/
 
-set_option autoImplicit true
-
-
 open Function Set Filter Topology
 
 universe u v w
@@ -240,7 +237,7 @@ end TopologicalSpace
 
 section Lattice
 
-variable {t t₁ t₂ : TopologicalSpace α} {s : Set α}
+variable {α : Type*} {t t₁ t₂ : TopologicalSpace α} {s : Set α}
 
 theorem IsOpen.mono (hs : IsOpen[t₂] s) (h : t₁ ≤ t₂) : IsOpen[t₁] s := h s hs
 #align is_open.mono IsOpen.mono
@@ -282,7 +279,7 @@ theorem discreteTopology_bot (α : Type*) : @DiscreteTopology α ⊥ :=
 
 section DiscreteTopology
 
-variable [TopologicalSpace α] [DiscreteTopology α]
+variable [TopologicalSpace α] [DiscreteTopology α] {β : Type*}
 
 @[simp]
 theorem isOpen_discrete (s : Set α) : IsOpen s := (@DiscreteTopology.eq_bot α _).symm ▸ trivial
@@ -296,7 +293,7 @@ theorem isOpen_discrete (s : Set α) : IsOpen s := (@DiscreteTopology.eq_bot α
 @[simp] theorem dense_discrete {s : Set α} : Dense s ↔ s = univ := by simp [dense_iff_closure_eq]
 
 @[simp]
-theorem denseRange_discrete {f : ι → α} : DenseRange f ↔ Surjective f := by
+theorem denseRange_discrete {ι : Type*} {f : ι → α} : DenseRange f ↔ Surjective f := by
   rw [DenseRange, dense_discrete, range_iff_surjective]
 
 @[nontriviality, continuity]
diff --git a/Mathlib/Topology/ProperMap.lean b/Mathlib/Topology/ProperMap.lean
@@ -67,15 +67,13 @@ so don't hesitate to have a look!
 * [Stacks: Characterizing proper maps](https://stacks.math.columbia.edu/tag/005M)
 -/
 
-set_option autoImplicit true
-
 open Filter Topology Function Set
 open Prod (fst snd)
 
+variable {X Y Z W ι : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
+  [TopologicalSpace W] {f : X → Y}
 
-
-variable [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] [TopologicalSpace W]
-  {f : X → Y}
+universe u v
 
 /-- A map `f : X → Y` between two topological spaces is said to be **proper** if it is continuous
 and, for all `ℱ : Filter X`, any cluster point of `map f ℱ` is the image by `f` of a cluster point
diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean
@@ -115,12 +115,9 @@ The formalization uses the books:
 But it makes a more systematic use of the filter library.
 -/
 
-set_option autoImplicit true
-
-
 open Set Filter Topology
 
-universe ua ub uc ud
+universe u v ua ub uc ud
 
 /-!
 ### Relations, seen as `Set (α × α)`
