chore: remove autoImplicit in Util (#14694)

All of them were easy to remove. Also remove on occurrence in Init/Logic which was not needed.

Author: grunweg

Mathlib/Init/Logic.lean

@@ -25,8 +25,6 @@ Contributions assisting with this are appreciated.
 These will be deleted soon so will not significantly delay deleting otherwise empty `Init` files.
 -/
 
-set_option autoImplicit true
-
 universe u v
 variable {α : Sort u}
 

Mathlib/Util/AtomM.lean

@@ -12,8 +12,6 @@ This monad is used by tactics like `ring` and `abel` to keep uninterpreted atoms
 order, and also to allow unifying atoms up to a specified transparency mode.
 -/
 
-set_option autoImplicit true
-
 namespace Mathlib.Tactic
 open Lean Meta
 
@@ -35,7 +33,7 @@ structure AtomM.State :=
 abbrev AtomM := ReaderT AtomM.Context <| StateRefT AtomM.State MetaM
 
 /-- Run a computation in the `AtomM` monad. -/
-def AtomM.run (red : TransparencyMode) (m : AtomM α)
+def AtomM.run {α : Type} (red : TransparencyMode) (m : AtomM α)
     (evalAtom : Expr → MetaM Simp.Result := fun e ↦ pure { expr := e }) :
     MetaM α :=
   (m { red, evalAtom }).run' {}

Mathlib/Util/Export.lean

@@ -12,8 +12,6 @@ A rudimentary export format, adapted from
 with support for lean 4 kernel primitives.
 -/
 
-set_option autoImplicit true
-
 open Lean (HashMap HashSet)
 
 namespace Lean
@@ -196,7 +194,7 @@ where
 
 end
 
-def runExportM (m : ExportM α) : CoreM α := m.run' default
+def runExportM {α : Type} (m : ExportM α) : CoreM α := m.run' default
 
 -- #eval runExportM (exportDef `Lean.Expr)
 end Export

Mathlib/Util/MemoFix.lean

@@ -10,8 +10,7 @@ import Lean.Data.HashMap
 
 -/
 
-set_option autoImplicit true
-
+universe u v
 open ShareCommon
 
 private unsafe abbrev ObjectMap := @Lean.HashMap Object Object ⟨Object.ptrEq⟩ ⟨Object.hash⟩

Mathlib/Util/Qq.lean

@@ -11,7 +11,6 @@ import Qq
 This file contains some additional functions for using the quote4 library more conveniently.
 -/
 
-set_option autoImplicit true
 open Lean Elab Tactic Meta
 
 namespace Qq
@@ -26,6 +25,6 @@ def inferTypeQ' (e : Expr) : MetaM ((u : Level) × (α : Q(Type $u)) × Q($α))
   let some v := (← instantiateLevelMVars u).dec | throwError "not a Type{indentExpr e}"
   pure ⟨v, α, e⟩
 
-theorem QuotedDefEq.rfl : @QuotedDefEq u α a a := ⟨⟩
+theorem QuotedDefEq.rfl {u : Level} {α : Q(Sort u)} {a : Q(«$α»)} : @QuotedDefEq u α a a := ⟨⟩
 
 end Qq

Mathlib/Util/Superscript.lean

@@ -24,10 +24,12 @@ However, note that Unicode has a rather restricted character set for superscript
 parser for complex expressions.
 -/
 
-set_option autoImplicit true
+universe u
 
 namespace Mathlib.Tactic
+
 open Lean Parser PrettyPrinter
+
 namespace Superscript
 
 instance : Hashable Char := ⟨fun c => hash c.1⟩

Mathlib/Util/Tactic.lean

@@ -11,13 +11,11 @@ import Lean.MetavarContext
 [TODO] Ideally we would find good homes for everything in this file, eventually removing it.
 -/
 
-set_option autoImplicit true
-
 namespace Mathlib.Tactic
 
 open Lean Meta Tactic
 
-variable [Monad m]
+variable {m : Type → Type} [Monad m]
 
 /--
 `modifyMetavarDecl mvarId f` updates the `MetavarDecl` for `mvarId` with `f`.

Mathlib/Util/WithWeakNamespace.lean

@@ -12,8 +12,6 @@ import Lean
 Changes the current namespace without causing scoped things to go out of scope.
 -/
 
-set_option autoImplicit true
-
 namespace Lean.Elab.Command
 
 /-- Adds the name to the namespace, `_root_`-aware.
@@ -29,7 +27,7 @@ def resolveNamespace (ns : Name) : Name → Name
   | Name.anonymous => ns
 
 /-- Changes the current namespace without causing scoped things to go out of scope -/
-def withWeakNamespace (ns : Name) (m : CommandElabM α) : CommandElabM α := do
+def withWeakNamespace {α : Type} (ns : Name) (m : CommandElabM α) : CommandElabM α := do
   let old ← getCurrNamespace
   let ns := resolveNamespace old ns
   modify fun s ↦ { s with env := s.env.registerNamespace ns }