chore(Topology): remove autoImplicit in some files (#9689)

... where this is easy to do.

Co-authored-by: grunweg <grunweg@posteo.de>

Author: grunweg

Mathlib/Topology/Bases.lean

@@ -52,9 +52,6 @@ More fine grained instances for `FirstCountableTopology`,
 `TopologicalSpace.SeparableSpace`, and more.
 -/
 
-set_option autoImplicit true
-
-
 open Set Filter Function Topology
 
 noncomputable section
@@ -63,7 +60,7 @@ namespace TopologicalSpace
 
 universe u
 
-variable {α : Type u} [t : TopologicalSpace α] {B : Set (Set α)} {s : Set α}
+variable {α : Type u} {β : Type*} [t : TopologicalSpace α] {B : Set (Set α)} {s : Set α}
 
 /-- A topological basis is one that satisfies the necessary conditions so that
   it suffices to take unions of the basis sets to get a topology (without taking

Mathlib/Topology/EMetricSpace/Lipschitz.lean

@@ -41,8 +41,6 @@ coercions both to `ℝ` and `ℝ≥0∞`. Constructors whose names end with `'`
 argument, and return `LipschitzWith (Real.toNNReal K) f`.
 -/
 
-set_option autoImplicit true
-
 universe u v w x
 
 open Filter Function Set Topology NNReal ENNReal Bornology
@@ -313,8 +311,8 @@ protected theorem continuousOn (hf : LipschitzOnWith K f s) : ContinuousOn f s :
   hf.uniformContinuousOn.continuousOn
 #align lipschitz_on_with.continuous_on LipschitzOnWith.continuousOn
 
-theorem edist_le_mul_of_le (h : LipschitzOnWith K f s) (hx : x ∈ s) (hy : y ∈ s)
-    (hr : edist x y ≤ r) :
+theorem edist_le_mul_of_le (h : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s)
+    {r : ℝ≥0∞} (hr : edist x y ≤ r) :
     edist (f x) (f y) ≤ K * r :=
   (h hx hy).trans <| ENNReal.mul_left_mono hr
 

Mathlib/Topology/FiberBundle/Trivialization.lean

@@ -48,9 +48,6 @@ Indeed, since trivializations only have meaning on their base sets (taking junk
 type of linear trivializations is not even particularly well-behaved.
 -/
 
-set_option autoImplicit true
-
-
 open TopologicalSpace Filter Set Bundle Function
 
 open scoped Topology Classical Bundle
@@ -458,7 +455,7 @@ theorem image_preimage_eq_prod_univ {s : Set B} (hb : s ⊆ e.baseSet) :
     ⟨e.invFun p, mem_preimage.mpr ((e.proj_symm_apply hp').symm ▸ hp.1), e.apply_symm_apply hp'⟩
 #align trivialization.image_preimage_eq_prod_univ Trivialization.image_preimage_eq_prod_univ
 
-theorem tendsto_nhds_iff {l : Filter α} {f : α → Z} {z : Z} (hz : z ∈ e.source) :
+theorem tendsto_nhds_iff {α : Type*} {l : Filter α} {f : α → Z} {z : Z} (hz : z ∈ e.source) :
     Tendsto f l (𝓝 z) ↔
       Tendsto (proj ∘ f) l (𝓝 (proj z)) ∧ Tendsto (fun x ↦ (e (f x)).2) l (𝓝 (e z).2) := by
   rw [e.nhds_eq_comap_inf_principal hz, tendsto_inf, tendsto_comap_iff, Prod.tendsto_iff, coe_coe,

Mathlib/Topology/Instances/ENNReal.lean

@@ -1647,7 +1647,7 @@ end truncateToReal
 
 section LimsupLiminf
 
-set_option autoImplicit true
+variable {ι : Type*}
 
 lemma limsup_sub_const (F : Filter ι) [NeBot F] (f : ι → ℝ≥0∞) (c : ℝ≥0∞) :
     Filter.limsup (fun i ↦ f i - c) F = Filter.limsup f F - c :=

Mathlib/Topology/MetricSpace/Gluing.lean

@@ -48,9 +48,6 @@ isometrically and in a way compatible with `f n`.
 
 -/
 
-set_option autoImplicit true
-
-
 noncomputable section
 
 universe u v w
@@ -628,6 +625,7 @@ def InductiveLimit (I : ∀ n, Isometry (f n)) : Type _ :=
   @UniformSpace.SeparationQuotient _ (inductivePremetric I).toUniformSpace
 #align metric.inductive_limit Metric.InductiveLimit
 
+set_option autoImplicit true in
 instance : MetricSpace (InductiveLimit (f := f) I) :=
   inferInstanceAs <| MetricSpace <|
     @UniformSpace.SeparationQuotient _ (inductivePremetric I).toUniformSpace

Mathlib/Topology/MetricSpace/Kuratowski.lean

@@ -16,9 +16,6 @@ Any partially defined Lipschitz map into `ℓ^∞` can be extended to the whole
 
 -/
 
-set_option autoImplicit true
-
-
 noncomputable section
 
 set_option linter.uppercaseLean3 false
@@ -140,19 +137,19 @@ Theorem 2.2 of [Assaf Naor, *Metric Embeddings and Lipschitz Extensions*][Naor-2
 The same result for the case of a finite type `ι` is implemented in
 `LipschitzOnWith.extend_pi`.
 -/
-theorem LipschitzOnWith.extend_lp_infty [PseudoMetricSpace α] {s : Set α} {f : α → ℓ^∞(ι)}
-    {K : ℝ≥0} (hfl : LipschitzOnWith K f s): ∃ g : α → ℓ^∞(ι), LipschitzWith K g ∧ EqOn f g s := by
+theorem LipschitzOnWith.extend_lp_infty [PseudoMetricSpace α] {s : Set α} {ι : Type*}
+    {f : α → ℓ^∞(ι)} {K : ℝ≥0} (hfl : LipschitzOnWith K f s) :
+    ∃ g : α → ℓ^∞(ι), LipschitzWith K g ∧ EqOn f g s := by
   -- Construct the coordinate-wise extensions
   rw [LipschitzOnWith.coordinate] at hfl
-  have : ∀ i : ι, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
-  · intro i
-    exact LipschitzOnWith.extend_real (hfl i) -- use the nonlinear Hahn-Banach theorem here!
+  have (i: ι) : ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s :=
+    LipschitzOnWith.extend_real (hfl i) -- use the nonlinear Hahn-Banach theorem here!
   choose g hgl hgeq using this
   rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
   · exact ⟨0, LipschitzWith.const' 0, by simp⟩
   · -- Show that the extensions are uniformly bounded
-    have hf_extb : ∀ a : α, Memℓp (swap g a) ∞
-    · apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
+    have hf_extb : ∀ a : α, Memℓp (swap g a) ∞ := by
+      apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
       use ‖f a₀‖
       rintro - ⟨i, rfl⟩
       simp_rw [← hgeq i ha₀_in_s]

Mathlib/Topology/MetricSpace/Lipschitz.lean

@@ -32,8 +32,6 @@ coercions both to `ℝ` and `ℝ≥0∞`. Constructors whose names end with `'`
 argument, and return `LipschitzWith (Real.toNNReal K) f`.
 -/
 
-set_option autoImplicit true
-
 universe u v w x
 
 open Filter Function Set Topology NNReal ENNReal Bornology

Mathlib/Topology/Order/Lattice.lean

@@ -24,8 +24,6 @@ class `TopologicalLattice` as a topological space and lattice `L` extending `Con
 topological, lattice
 -/
 
-set_option autoImplicit true
-
 open Filter
 
 open Topology
@@ -79,7 +77,7 @@ instance (priority := 100) LinearOrder.topologicalLattice {L : Type*} [Topologic
   continuous_sup := continuous_max
 #align linear_order.topological_lattice LinearOrder.topologicalLattice
 
-variable [TopologicalSpace L] [TopologicalSpace X]
+variable {L X : Type*} [TopologicalSpace L] [TopologicalSpace X]
 
 @[continuity]
 theorem continuous_inf [Inf L] [ContinuousInf L] : Continuous fun p : L × L => p.1 ⊓ p.2 :=
@@ -133,7 +131,7 @@ end SupInf
 
 open Finset
 
-variable {ι : Type*} {s : Finset ι} {f : ι → α → L} {g : ι → L}
+variable {ι α : Type*} {s : Finset ι} {f : ι → α → L} {l : Filter α} {g : ι → L}
 
 lemma finset_sup'_nhds [SemilatticeSup L] [ContinuousSup L]
     (hne : s.Nonempty) (hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))) :

Mathlib/Topology/VectorBundle/Basic.lean

@@ -54,8 +54,6 @@ notes" section of `Mathlib.Topology.FiberBundle.Basic`.
 Vector bundle
 -/
 
-set_option autoImplicit true
-
 noncomputable section
 
 open Bundle Set Classical
@@ -680,7 +678,7 @@ def localTriv (i : ι) : Trivialization F (π F Z.Fiber) :=
 
 -- porting note: moved from below to fix the next instance
 @[simp, mfld_simps]
-theorem localTriv_apply (p : Z.TotalSpace) :
+theorem localTriv_apply {i : ι} (p : Z.TotalSpace) :
     (Z.localTriv i) p = ⟨p.1, Z.coordChange (Z.indexAt p.1) i p.1 p.2⟩ :=
   rfl
 #align vector_bundle_core.local_triv_apply VectorBundleCore.localTriv_apply