chore(Tactic): reduce use of autoImplicit, part 3 (#14770)

Author: grunweg

Mathlib/Tactic/Basic.lean

@@ -11,8 +11,6 @@ import Mathlib.Tactic.Lemma
 import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.Linter.OldObtain
 
-set_option autoImplicit true
-
 namespace Mathlib.Tactic
 open Lean Parser.Tactic Elab Command Elab.Tactic Meta
 
@@ -30,7 +28,7 @@ Recall that variables linked this way should be considered to be semantically id
 
 The effect of this is, for example, the unused variable linter will see that variables
 from the first array are used if corresponding variables in the second array are used. -/
-def pushFVarAliasInfo [Monad m] [MonadInfoTree m]
+def pushFVarAliasInfo {m : Type → Type} [Monad m] [MonadInfoTree m]
     (oldFVars newFVars : Array FVarId) (newLCtx : LocalContext) : m Unit := do
   for old in oldFVars, new in newFVars do
     if old != new then

Mathlib/Tactic/CategoryTheory/BicategoryCoherence.lean

@@ -24,9 +24,6 @@ tactic is given in `Mathlib.Tactic.CategoryTheory.Coherence` at the same time as
 tactic for monoidal categories.
 -/
 
-set_option autoImplicit true
-
-
 noncomputable section
 
 universe w v u
@@ -246,7 +243,7 @@ theorem bicategoricalComp_refl {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) :
 open Lean Elab Tactic Meta
 
 /-- Helper function for throwing exceptions. -/
-def exception (g : MVarId) (msg : MessageData) : MetaM α :=
+def exception {α : Type} (g : MVarId) (msg : MessageData) : MetaM α :=
   throwTacticEx `bicategorical_coherence g msg
 
 /-- Helper function for throwing exceptions with respect to the main goal. -/

Mathlib/Tactic/CategoryTheory/Coherence.lean

@@ -25,8 +25,6 @@ are equal.
 
 -/
 
-set_option autoImplicit true
-
 -- Porting note: restore when ported
 -- import Mathlib.CategoryTheory.Bicategory.CoherenceTactic
 
@@ -103,7 +101,8 @@ end lifting
 open Lean Meta Elab Tactic
 
 /-- Helper function for throwing exceptions. -/
-def exception (g : MVarId) (msg : MessageData) : MetaM α := throwTacticEx `monoidal_coherence g msg
+def exception {α : Type} (g : MVarId) (msg : MessageData) : MetaM α :=
+  throwTacticEx `monoidal_coherence g msg
 
 /-- Helper function for throwing exceptions with respect to the main goal. -/
 def exception' (msg : MessageData) : TacticM Unit := do

Mathlib/Tactic/CategoryTheory/Elementwise.lean

@@ -32,8 +32,6 @@ This closely follows the implementation of the `@[reassoc]` attribute, due to Si
 reimplemented by Scott Morrison in Lean 4.
 -/
 
-set_option autoImplicit true
-
 open Lean Meta Elab Tactic
 open Mathlib.Tactic
 
@@ -42,14 +40,16 @@ open CategoryTheory
 
 section theorems
 
+universe u
+
 theorem forall_congr_forget_Type (α : Type u) (p : α → Prop) :
     (∀ (x : (forget (Type u)).obj α), p x) ↔ ∀ (x : α), p x := Iff.rfl
 
 attribute [local instance] ConcreteCategory.instFunLike ConcreteCategory.hasCoeToSort
 
 theorem forget_hom_Type (α β : Type u) (f : α ⟶ β) : DFunLike.coe f = f := rfl
 
-theorem hom_elementwise [Category C] [ConcreteCategory C]
+theorem hom_elementwise {C : Type*} [Category C] [ConcreteCategory C]
     {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x := by rw [h]
 
 end theorems

Mathlib/Tactic/FieldSimp.lean

@@ -18,8 +18,6 @@ import Qq
 Tactic to clear denominators in algebraic expressions, based on `simp` with a specific simpset.
 -/
 
-set_option autoImplicit true
-
 namespace Mathlib.Tactic.FieldSimp
 
 open Lean Elab.Tactic Parser.Tactic Lean.Meta
@@ -28,7 +26,8 @@ open Qq
 initialize registerTraceClass `Tactic.field_simp
 
 /-- Constructs a trace message for the `discharge` function. -/
-private def dischargerTraceMessage (prop: Expr) : Except ε (Option Expr) → SimpM MessageData
+private def dischargerTraceMessage {ε : Type*} (prop: Expr) :
+    Except ε (Option Expr) → SimpM MessageData
 | .error _ | .ok none => return m!"{crossEmoji} discharge {prop}"
 | .ok (some _) => return m!"{checkEmoji} discharge {prop}"
 

Mathlib/Tactic/IntervalCases.lean

@@ -22,11 +22,6 @@ where the hypotheses should be of the form `hl : a ≤ n` and `hu : n < b`. In t
 `interval_cases` calls `fin_cases` on the resulting hypothesis `h : n ∈ Set.Ico a b`.
 -/
 
-set_option autoImplicit true
-
--- In this file we would like to be able to use multi-character auto-implicits.
-set_option relaxedAutoImplicit true
-
 namespace Mathlib.Tactic
 
 open Lean Meta Elab Tactic Term Qq Int
@@ -123,6 +118,8 @@ structure Methods where
   /-- Construct the canonical numeral for integer `z`, or fail if `z` is out of range. -/
   mkNumeral : Int → MetaM Expr
 
+variable {α : Type*} {a b a' b' : α}
+
 theorem of_not_lt_left [LinearOrder α] (h : ¬(a:α) < b) (eq : a = a') : b ≤ a' := eq ▸ not_lt.1 h
 theorem of_not_lt_right [LinearOrder α] (h : ¬(a:α) < b) (eq : b = b') : b' ≤ a := eq ▸ not_lt.1 h
 theorem of_not_le_left [LE α] (h : ¬(a:α) ≤ b) (eq : a = a') : ¬a' ≤ b := eq ▸ h
@@ -159,7 +156,8 @@ def Methods.getBound (m : Methods) (e : Expr) (pf : Expr) (lb : Bool) :
   let .true ← withNewMCtxDepth <| withReducible <| isDefEq e e' | failure
   pure c
 
-theorem le_of_not_le_of_le [LinearOrder α] (h1 : ¬hi ≤ n) (h2 : hi ≤ lo) : (n:α) ≤ lo :=
+theorem le_of_not_le_of_le {hi n lo : α} [LinearOrder α] (h1 : ¬hi ≤ n) (h2 : hi ≤ lo) :
+    (n:α) ≤ lo :=
   le_trans (le_of_not_le h1) h2
 
 /--

Mathlib/Tactic/LinearCombination.lean

@@ -30,12 +30,12 @@ Lastly, calls a normalization tactic on this target.
 
 -/
 
-set_option autoImplicit true
-
 namespace Mathlib.Tactic.LinearCombination
 open Lean hiding Rat
 open Elab Meta Term
 
+variable {α : Type*} {a a' a₁ a₂ b b' b₁ b₂ c : α}
+
 theorem pf_add_c [Add α] (p : a = b) (c : α) : a + c = b + c := p ▸ rfl
 theorem c_add_pf [Add α] (p : b = c) (a : α) : a + b = a + c := p ▸ rfl
 theorem add_pf [Add α] (p₁ : (a₁:α) = b₁) (p₂ : a₂ = b₂) : a₁ + a₂ = b₁ + b₂ := p₁ ▸ p₂ ▸ rfl

Mathlib/Tactic/ModCases.lean

@@ -11,8 +11,6 @@ The `mod_cases` tactic does case disjunction on `e % n`, where `e : ℤ` or `e :
 to yield `n` new subgoals corresponding to the possible values of `e` modulo `n`.
 -/
 
-set_option autoImplicit true
-
 namespace Mathlib.Tactic.ModCases
 open Lean Meta Elab Tactic Term Qq
 
@@ -62,7 +60,7 @@ and the `a ≡ b (mod n) → p` case becomes a subgoal.
 Proves an expression of the form `OnModCases n a b p` where `n` and `b` are raw nat literals
 and `b ≤ n`. Returns the list of subgoals `?gi : a ≡ i [ZMOD n] → p`.
 -/
-partial def proveOnModCases (n : Q(ℕ)) (a : Q(ℤ)) (b : Q(ℕ)) (p : Q(Sort u)) :
+partial def proveOnModCases {u : Level} (n : Q(ℕ)) (a : Q(ℤ)) (b : Q(ℕ)) (p : Q(Sort u)) :
     MetaM (Q(OnModCases $n $a $b $p) × List MVarId) := do
   if n.natLit! ≤ b.natLit! then
     haveI' : $b =Q $n := ⟨⟩
@@ -138,7 +136,7 @@ and the `a ≡ b (mod n) → p` case becomes a subgoal.
 Proves an expression of the form `OnModCases n a b p` where `n` and `b` are raw nat literals
 and `b ≤ n`. Returns the list of subgoals `?gi : a ≡ i [MOD n] → p`.
 -/
-partial def proveOnModCases (n : Q(ℕ)) (a : Q(ℕ)) (b : Q(ℕ)) (p : Q(Sort u)) :
+partial def proveOnModCases {u : Level} (n : Q(ℕ)) (a : Q(ℕ)) (b : Q(ℕ)) (p : Q(Sort u)) :
     MetaM (Q(OnModCases $n $a $b $p) × List MVarId) := do
   if n.natLit! ≤ b.natLit! then
     pure ((q(onModCases_stop $p $n $a) : Expr), [])

Mathlib/Tactic/Polyrith.lean

@@ -60,8 +60,6 @@ remember to force recompilation of any files that call `polyrith`.
 
 -/
 
-set_option autoImplicit true
-
 namespace Mathlib.Tactic.Polyrith
 open Lean hiding Rat
 open Meta Ring Qq PrettyPrinter AtomM
@@ -131,7 +129,7 @@ def Poly.toSyntax : Poly → Unhygienic Syntax.Term
   | .neg p => do `(-$(← p.toSyntax))
 
 /-- Reifies a ring expression of type `α` as a `Poly`. -/
-partial def parse {u} {α : Q(Type u)} (sα : Q(CommSemiring $α))
+partial def parse {u : Level} {α : Q(Type u)} (sα : Q(CommSemiring $α))
     (c : Ring.Cache sα) (e : Q($α)) : AtomM Poly := do
   let els := do
     try pure <| Poly.const (← (← NormNum.derive e).toRat)
@@ -244,7 +242,7 @@ def Poly.pow' : ℕ → ℕ → Poly
   | i, k => .pow (.var i) (.const k)
 
 /-- Constructs a sum from a monadic function supplying the monomials. -/
-def Poly.sumM [Monad m] (a : Array α) (f : α → m Poly) : m Poly :=
+def Poly.sumM {m : Type → Type*} {α : Type*} [Monad m] (a : Array α) (f : α → m Poly) : m Poly :=
   a.foldlM (init := .const 0) fun p a => return p.add' (← f a)
 
 instance : FromJson Poly where

Mathlib/Tactic/ReduceModChar.lean

@@ -36,21 +36,21 @@ open Lean.Elab
 open Tactic
 open Qq
 
-set_option autoImplicit true
-
 namespace Tactic
 
 namespace ReduceModChar
 
 open Mathlib.Meta.NormNum
 
+variable {u : Level}
+
 lemma CharP.intCast_eq_mod (R : Type _) [Ring R] (p : ℕ) [CharP R p] (k : ℤ) :
     (k : R) = (k % p : ℤ) := by
   calc
     (k : R) = ↑(k % p + p * (k / p)) := by rw [Int.emod_add_ediv]
     _ = ↑(k % p) := by simp [CharP.cast_eq_zero R]
 
-lemma CharP.isInt_of_mod {α : Type _} [Ring α] {n n' : ℕ} (inst : CharP α n) {e : α}
+lemma CharP.isInt_of_mod {e' r : ℤ} {α : Type _} [Ring α] {n n' : ℕ} (inst : CharP α n) {e : α}
     (he : IsInt e e') (hn : IsNat n n') (h₂ : IsInt (e' % n') r) : IsInt e r :=
   ⟨by rw [he.out, CharP.intCast_eq_mod α n, show n = n' from hn.out, h₂.out, Int.cast_id]⟩
 
@@ -127,7 +127,7 @@ inductive TypeToCharPResult (α : Q(Type u))
   | intLike (n : Q(ℕ)) (instRing : Q(Ring $α)) (instCharP : Q(CharP $α $n))
   | failure
 
-instance : Inhabited (TypeToCharPResult α) := ⟨.failure⟩
+instance {α : Q(Type u)} : Inhabited (TypeToCharPResult α) := ⟨.failure⟩
 
 /-- Determine the characteristic of a ring from the type.
 This should be fast, so this pattern-matches on the type, rather than searching for a