style: cleanup some autoImplicits (#8288)

In some cases adding the arguments manually results in a more obvious argument order anyway

Mathlib/Algebra/Group/Defs.lean

@@ -40,7 +40,7 @@ actions and register the following instances:
 
 -/
 
-set_option autoImplicit true
+universe u v w
 
 open Function
 
@@ -93,13 +93,11 @@ attribute [to_additive existing (reorder := 1 2, 5 6) hSMul] HPow.hPow
 attribute [to_additive existing (reorder := 1 2, 4 5) smul] Pow.pow
 
 @[to_additive (attr := default_instance)]
-instance instHSMul [SMul α β] : HSMul α β β where
+instance instHSMul {α β} [SMul α β] : HSMul α β β where
   hSMul := SMul.smul
 
 attribute [to_additive existing (reorder := 1 2)] instHPow
 
-universe u
-
 variable {G : Type*}
 
 /-- Class of types that have an inversion operation. -/

Mathlib/Algebra/Group/MinimalAxioms.lean

@@ -21,7 +21,7 @@ equalities.
 
 -/
 
-set_option autoImplicit true
+universe u
 
 /-- Define a `Group` structure on a Type by proving `∀ a, 1 * a = a` and
 `∀ a, a⁻¹ * a = 1`.

Mathlib/Algebra/Group/Semiconj/Basic.lean

@@ -13,13 +13,11 @@ import Mathlib.Algebra.Group.Basic
 
 -/
 
-set_option autoImplicit true
-
 namespace SemiconjBy
 
 section DivisionMonoid
 
-variable [DivisionMonoid G] {a x y : G}
+variable {G : Type*} [DivisionMonoid G] {a x y : G}
 
 @[to_additive (attr := simp)]
 theorem inv_inv_symm_iff : SemiconjBy a⁻¹ x⁻¹ y⁻¹ ↔ SemiconjBy a y x :=

Mathlib/Algebra/Group/Semiconj/Defs.lean

@@ -29,7 +29,7 @@ This file provides only basic operations (`mul_left`, `mul_right`, `inv_right` e
 operations (`pow_right`, field inverse etc) are in the files that define corresponding notions.
 -/
 
-set_option autoImplicit true
+variable {S M G : Type*}
 
 /-- `x` is semiconjugate to `y` by `a`, if `a * x = y * a`. -/
 @[to_additive AddSemiconjBy "`x` is additive semiconjugate to `y` by `a` if `a + x = y + a`"]

Mathlib/Algebra/Group/Semiconj/Units.lean

@@ -29,7 +29,7 @@ This file provides only basic operations (`mul_left`, `mul_right`, `inv_right` e
 operations (`pow_right`, field inverse etc) are in the files that define corresponding notions.
 -/
 
-set_option autoImplicit true
+variable {M G : Type*}
 
 namespace SemiconjBy
 

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -20,11 +20,8 @@ members.
 * `CommGroupWithZero`
 -/
 
-
 universe u
 
-set_option autoImplicit true
-
 -- We have to fix the universe of `G₀` here, since the default argument to
 -- `GroupWithZero.div'` cannot contain a universe metavariable.
 variable {G₀ : Type u} {M₀ M₀' G₀' : Type*}

Mathlib/Algebra/GroupWithZero/NeZero.lean

@@ -17,9 +17,7 @@ which is a part of the algebraic hierarchy used by basic tactics.
 
 universe u
 
-set_option autoImplicit true
-
-variable [MulZeroOneClass M₀] [Nontrivial M₀] {a b : M₀}
+variable {M₀ M₀' : Type*} [MulZeroOneClass M₀] [Nontrivial M₀]
 
 /-- In a nontrivial monoid with zero, zero and one are different. -/
 instance NeZero.one : NeZero (1 : M₀) := ⟨by
@@ -43,7 +41,7 @@ theorem pullback_nonzero [Zero M₀'] [One M₀'] (f : M₀' → M₀) (zero : f
 
 section GroupWithZero
 
-variable [GroupWithZero G₀] {a b c g h x : G₀}
+variable {G₀ : Type*} [GroupWithZero G₀] {a : G₀}
 
 -- Porting note: used `simpa` to prove `False` in lean3
 theorem inv_ne_zero (h : a ≠ 0) : a⁻¹ ≠ 0 := fun a_eq_0 => by

Mathlib/Algebra/Invertible/Defs.lean

@@ -75,9 +75,6 @@ invertible, inverse element, invOf, a half, one half, a third, one third, ½, 
 
 -/
 
-set_option autoImplicit true
-
-
 universe u
 
 variable {α : Type u}
@@ -241,26 +238,27 @@ def Invertible.mul [Monoid α] {a b : α} (_ : Invertible a) (_ : Invertible b)
   invertibleMul _ _
 #align invertible.mul Invertible.mul
 
-theorem mul_right_inj_of_invertible [Monoid α] (c : α) [Invertible c] :
+theorem mul_right_inj_of_invertible [Monoid α] {a b : α} (c : α) [Invertible c] :
     a * c = b * c ↔ a = b :=
   ⟨fun h => by simpa using congr_arg (· * ⅟c) h, congr_arg (· * _)⟩
 
-theorem mul_left_inj_of_invertible [Monoid α] (c : α) [Invertible c] :
+theorem mul_left_inj_of_invertible [Monoid α] {a b : α} (c : α) [Invertible c] :
     c * a = c * b ↔ a = b :=
   ⟨fun h => by simpa using congr_arg (⅟c * ·) h, congr_arg (_ * ·)⟩
 
-theorem invOf_mul_eq_iff_eq_mul_left [Monoid α] [Invertible (c : α)] :
+theorem invOf_mul_eq_iff_eq_mul_left [Monoid α] {a b c : α} [Invertible (c : α)] :
     ⅟c * a = b ↔ a = c * b := by
   rw [← mul_left_inj_of_invertible (c := c), mul_invOf_self_assoc]
 
-theorem mul_left_eq_iff_eq_invOf_mul [Monoid α] [Invertible (c : α)] :
+theorem mul_left_eq_iff_eq_invOf_mul [Monoid α] {a b c : α} [Invertible (c : α)] :
     c * a = b ↔ a = ⅟c * b := by
   rw [← mul_left_inj_of_invertible (c := ⅟c), invOf_mul_self_assoc]
 
-theorem mul_invOf_eq_iff_eq_mul_right [Monoid α] [Invertible (c : α)] :
+
+theorem mul_invOf_eq_iff_eq_mul_right [Monoid α] {a b c : α} [Invertible (c : α)] :
     a * ⅟c = b ↔ a = b * c := by
   rw [← mul_right_inj_of_invertible (c := c), mul_invOf_mul_self_cancel]
 
-theorem mul_right_eq_iff_eq_mul_invOf [Monoid α] [Invertible (c : α)] :
+theorem mul_right_eq_iff_eq_mul_invOf [Monoid α] {a b c : α} [Invertible (c : α)] :
     a * c = b ↔ a = b * ⅟c := by
   rw [← mul_right_inj_of_invertible (c := ⅟c), mul_mul_invOf_self_cancel]

Mathlib/Algebra/Invertible/GroupWithZero.lean

@@ -13,8 +13,6 @@ import Mathlib.Algebra.GroupWithZero.NeZero
 We intentionally keep imports minimal here as this file is used by `Mathlib.Tactic.NormNum`.
 -/
 
-set_option autoImplicit true
-
 universe u
 
 variable {α : Type u}

Mathlib/Algebra/Opposites.lean

@@ -41,11 +41,10 @@ definitional eta reduction for structures (Lean 3 does not).
 multiplicative opposite, additive opposite
 -/
 
-set_option autoImplicit true
-
-
 universe u v
 
+variable {α : Type*}
+
 open Function
 
 /-- Auxiliary type to implement `MulOpposite` and `AddOpposite`.