chore: remove more autoImplicit (#11336)

... or reduce its scope (the full removal is not as obvious).

Archive/Imo/Imo1987Q1.lean

@@ -24,9 +24,6 @@ The original problem assumes `n ≥ 1`. It turns out that a version with `n * (n
 holds true for `n = 0` as well, so we first prove it, then deduce the original version in the case
 `n ≥ 1`. -/
 
-
-set_option autoImplicit true
-
 variable (α : Type*) [Fintype α] [DecidableEq α]
 
 open scoped BigOperators Nat
@@ -62,7 +59,7 @@ def fiber (k : ℕ) : Set (Perm α) :=
   {σ : Perm α | card (fixedPoints σ) = k}
 #align imo1987_q1.fiber Imo1987Q1.fiber
 
-instance : Fintype (fiber α k) := by unfold fiber; infer_instance
+instance {k : ℕ} : Fintype (fiber α k) := by unfold fiber; infer_instance
 
 @[simp]
 theorem mem_fiber {σ : Perm α} {k : ℕ} : σ ∈ fiber α k ↔ card (fixedPoints σ) = k :=

Mathlib/Algebra/AddTorsor.lean

@@ -39,9 +39,6 @@ multiplicative group actions).
 
 -/
 
-set_option autoImplicit true
-
-
 /-- An `AddTorsor G P` gives a structure to the nonempty type `P`,
 acted on by an `AddGroup G` with a transitive and free action given
 by the `+ᵥ` operation and a corresponding subtraction given by the
@@ -277,7 +274,7 @@ end comm
 
 namespace Prod
 
-variable {G : Type*} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P']
+variable {G G' P P' : Type*} [AddGroup G] [AddGroup G'] [AddTorsor G P] [AddTorsor G' P']
 
 instance instAddTorsor : AddTorsor (G × G') (P × P') where
   vadd v p := (v.1 +ᵥ p.1, v.2 +ᵥ p.2)

Mathlib/Algebra/Algebra/Equiv.lean

@@ -21,9 +21,6 @@ This file defines bundled isomorphisms of `R`-algebras.
 * `A ≃ₐ[R] B` : `R`-algebra equivalence from `A` to `B`.
 -/
 
-set_option autoImplicit true
-
-
 open BigOperators
 
 universe u v w u₁ v₁

Mathlib/Algebra/Algebra/Hom.lean

@@ -23,9 +23,6 @@ This file defines bundled homomorphisms of `R`-algebras.
 * `A →ₐ[R] B` : `R`-algebra homomorphism from `A` to `B`.
 -/
 
-set_option autoImplicit true
-
-
 open BigOperators
 
 universe u v w u₁ v₁
@@ -62,7 +59,7 @@ class AlgHomClass (F : Type*) (R A B : outParam Type*)
 
 namespace AlgHomClass
 
-variable {R : Type*} {A : Type*} {B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
+variable {R A B F : Type*} [CommSemiring R] [Semiring A] [Semiring B]
   [Algebra R A] [Algebra R B] [FunLike F A B]
 
 -- see Note [lower instance priority]

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -43,9 +43,6 @@ TODO: add `NonUnitalAlgEquiv` when needed.
 non-unital, algebra, morphism
 -/
 
-set_option autoImplicit true
-
-
 universe u v w w₁ w₂ w₃
 
 variable (R : Type u) (A : Type v) (B : Type w) (C : Type w₁)
@@ -442,7 +439,7 @@ variable {R A B} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A]
   [Algebra R B]
 
 -- see Note [lower instance priority]
-instance (priority := 100) [FunLike F A B] [AlgHomClass F R A B] :
+instance (priority := 100) {F : Type*} [FunLike F A B] [AlgHomClass F R A B] :
     NonUnitalAlgHomClass F R A B :=
   { ‹AlgHomClass F R A B› with map_smul := map_smul }
 

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -19,9 +19,6 @@ We introduce the bundled categories:
 along with the relevant forgetful functors between them, and to the bundled monoid categories.
 -/
 
-set_option autoImplicit true
-
-
 universe u v
 
 open CategoryTheory
@@ -80,7 +77,7 @@ lemma coe_comp {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X →
 lemma comp_def {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl
 
 -- porting note (#10756): added lemma
-@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl
+@[simp] lemma forget_map {X Y : GroupCat} (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl
 
 @[to_additive (attr := ext)]
 lemma ext {X Y : GroupCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=

Mathlib/Algebra/Category/GroupWithZeroCat.lean

@@ -14,9 +14,6 @@ import Mathlib.Algebra.Category.MonCat.Basic
 This file defines `GroupWithZeroCat`, the category of groups with zero.
 -/
 
-set_option autoImplicit true
-
-
 universe u
 
 open CategoryTheory Order
@@ -73,7 +70,9 @@ instance groupWithZeroConcreteCategory : ConcreteCategory GroupWithZeroCat where
   forget_faithful := ⟨fun h => DFunLike.coe_injective h⟩
 
 -- porting note (#10756): added lemma
-@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupWithZeroCat).map f = f := rfl
+@[simp] lemma forget_map {X Y : GroupWithZeroCat} (f : X ⟶ Y) :
+  (forget GroupWithZeroCat).map f = f := rfl
+
 instance hasForgetToBipointed : HasForget₂ GroupWithZeroCat Bipointed where
   forget₂ :=
       { obj := fun X => ⟨X, 0, 1⟩

Mathlib/Algebra/Category/ModuleCat/Free.lean

@@ -26,8 +26,6 @@ linear algebra, module, free
 
 -/
 
-set_option autoImplicit true
-
 open CategoryTheory
 
 namespace ModuleCat
@@ -83,7 +81,7 @@ end LinearIndependent
 
 section Span
 
-
+set_option autoImplicit true in
 /-- In the commutative diagram
 ```
     f     g
@@ -166,7 +164,7 @@ theorem free_shortExact_rank_add [Module.Free R S.X₁] [Module.Free R S.X₃]
   exact ⟨Basis.indexEquiv (Module.Free.chooseBasis R S.X₂) (Basis.ofShortExact hS'
     (Module.Free.chooseBasis R S.X₁) (Module.Free.chooseBasis R S.X₃))⟩
 
-theorem free_shortExact_finrank_add [Module.Free R S.X₁] [Module.Free R S.X₃]
+theorem free_shortExact_finrank_add {n p : ℕ} [Module.Free R S.X₁] [Module.Free R S.X₃]
     [Module.Finite R S.X₁] [Module.Finite R S.X₃]
     (hN : FiniteDimensional.finrank R S.X₁ = n)
     (hP : FiniteDimensional.finrank R S.X₃ = p)

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -22,13 +22,12 @@ as a presheaf of abelian groups with additional data.
 * Pushforward and pullback.
 -/
 
-universe v₁ u₁ u
+universe v₁ u₁ u v
 
 open CategoryTheory LinearMap Opposite
 
 variable {C : Type u₁} [Category.{v₁} C]
 
-set_option autoImplicit true in
 /-- A presheaf of modules over a given presheaf of rings,
 described as a presheaf of abelian groups, and the extra data of the action at each object,
 and a condition relating functoriality and scalar multiplication. -/

Mathlib/Algebra/Category/ModuleCat/Projective.lean

@@ -15,9 +15,7 @@ import Mathlib.Data.Finsupp.Basic
 # The category of `R`-modules has enough projectives.
 -/
 
-set_option autoImplicit true
-
-universe v u
+universe v u u'
 
 open CategoryTheory
 

Mathlib/Algebra/Category/MonCat/Basic.lean

@@ -20,9 +20,6 @@ We introduce the bundled categories:
 along with the relevant forgetful functors between them.
 -/
 
-set_option autoImplicit true
-
-
 universe u v
 
 open CategoryTheory
@@ -102,7 +99,8 @@ lemma coe_id {X : MonCat} : (𝟙 X : X → X) = id := rfl
 lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 -- porting note (#10756): added lemma
-@[to_additive (attr := simp)] lemma forget_map (f : X ⟶ Y) : (forget MonCat).map f = f := rfl
+@[to_additive (attr := simp)] lemma forget_map {X Y : MonCat} (f : X ⟶ Y) :
+    (forget MonCat).map f = f := rfl
 
 @[to_additive (attr := ext)]
 lemma ext {X Y : MonCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=

Mathlib/Algebra/Category/Ring/Basic.lean

@@ -20,9 +20,6 @@ We introduce the bundled categories:
 along with the relevant forgetful functors between them.
 -/
 
-set_option autoImplicit true
-
-
 universe u v
 
 open CategoryTheory
@@ -92,7 +89,8 @@ lemma coe_id {X : SemiRingCat} : (𝟙 X : X → X) = id := rfl
 lemma coe_comp {X Y Z : SemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 -- porting note (#10756): added lemma
-@[simp] lemma forget_map (f : X ⟶ Y) : (forget SemiRingCat).map f = (f : X → Y) := rfl
+@[simp] lemma forget_map {X Y : SemiRingCat} (f : X ⟶ Y) :
+    (forget SemiRingCat).map f = (f : X → Y) := rfl
 
 lemma ext {X Y : SemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
   RingHom.ext w
@@ -150,6 +148,7 @@ theorem ofHom_apply {R S : Type u} [Semiring R] [Semiring S] (f : R →+* S) (x
 set_option linter.uppercaseLean3 false in
 #align SemiRing.of_hom_apply SemiRingCat.ofHom_apply
 
+set_option autoImplicit true in
 /--
 Ring equivalence are isomorphisms in category of semirings
 -/
@@ -216,7 +215,7 @@ lemma coe_id {X : RingCat} : (𝟙 X : X → X) = id := rfl
 lemma coe_comp {X Y Z : RingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 -- porting note (#10756): added lemma
-@[simp] lemma forget_map (f : X ⟶ Y) : (forget RingCat).map f = (f : X → Y) := rfl
+@[simp] lemma forget_map {X Y : RingCat} (f : X ⟶ Y) : (forget RingCat).map f = (f : X → Y) := rfl
 
 lemma ext {X Y : RingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
   RingHom.ext w
@@ -322,7 +321,8 @@ lemma coe_id {X : CommSemiRingCat} : (𝟙 X : X → X) = id := rfl
 lemma coe_comp {X Y Z : CommSemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 -- porting note (#10756): added lemma
-@[simp] lemma forget_map (f : X ⟶ Y) : (forget CommSemiRingCat).map f = (f : X → Y) := rfl
+@[simp] lemma forget_map {X Y : CommSemiRingCat} (f : X ⟶ Y) :
+  (forget CommSemiRingCat).map f = (f : X → Y) := rfl
 
 lemma ext {X Y : CommSemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
   RingHom.ext w
@@ -379,6 +379,7 @@ instance hasForgetToCommMonCat : HasForget₂ CommSemiRingCat CommMonCat :=
 set_option linter.uppercaseLean3 false in
 #align CommSemiRing.has_forget_to_CommMon CommSemiRingCat.hasForgetToCommMonCat
 
+set_option autoImplicit true in
 /--
 Ring equivalence are isomorphisms in category of commutative semirings
 -/
@@ -442,7 +443,8 @@ lemma coe_id {X : CommRingCat} : (𝟙 X : X → X) = id := rfl
 lemma coe_comp {X Y Z : CommRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl
 
 -- porting note (#10756): added lemma
-@[simp] lemma forget_map (f : X ⟶ Y) : (forget CommRingCat).map f = (f : X → Y) := rfl
+@[simp] lemma forget_map {X Y : CommRingCat} (f : X ⟶ Y) :
+    (forget CommRingCat).map f = (f : X → Y) := rfl
 
 lemma ext {X Y : CommRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
   RingHom.ext w

Mathlib/Algebra/CharZero/Defs.lean

@@ -29,8 +29,6 @@ from the natural numbers into it is injective.
 * Unify with `CharP` (possibly using an out-parameter)
 -/
 
-set_option autoImplicit true
-
 /-- Typeclass for monoids with characteristic zero.
   (This is usually stated on fields but it makes sense for any additive monoid with 1.)
 
@@ -47,6 +45,8 @@ class CharZero (R) [AddMonoidWithOne R] : Prop where
   cast_injective : Function.Injective (Nat.cast : ℕ → R)
 #align char_zero CharZero
 
+variable {R : Type*}
+
 theorem charZero_of_inj_zero [AddGroupWithOne R] (H : ∀ n : ℕ, (n : R) = 0 → n = 0) :
     CharZero R :=
   ⟨@fun m n h => by

Mathlib/Algebra/Field/MinimalAxioms.lean

@@ -19,7 +19,7 @@ a minimum number of equalities.
 
 -/
 
-set_option autoImplicit true
+universe u
 
 /-- Define a `Field` structure on a Type by proving a minimized set of axioms.
 Note that this uses the default definitions for `npow`, `nsmul`, `zsmul`, `div` and `sub`

Mathlib/Algebra/Field/Opposite.lean

@@ -13,8 +13,6 @@ import Mathlib.Data.Int.Cast.Lemmas
 # Field structure on the multiplicative/additive opposite
 -/
 
-set_option autoImplicit true
-
 namespace MulOpposite
 
 variable (α : Type*)
@@ -59,6 +57,8 @@ end MulOpposite
 
 namespace AddOpposite
 
+variable {α : Type*}
+
 instance divisionSemiring [DivisionSemiring α] : DivisionSemiring αᵃᵒᵖ :=
   { AddOpposite.groupWithZero α, AddOpposite.semiring α with }
 

Mathlib/Algebra/Homology/DifferentialObject.lean

@@ -18,9 +18,6 @@ This equivalence is probably not particularly useful in practice;
 it's here to check that definitions match up as expected.
 -/
 
-set_option autoImplicit true
-
-
 open CategoryTheory CategoryTheory.Limits
 
 open scoped Classical
@@ -58,7 +55,7 @@ theorem objEqToHom_d {x y : β} (h : x = y) :
 #align homological_complex.eq_to_hom_d CategoryTheory.DifferentialObject.objEqToHom_d
 
 @[reassoc (attr := simp)]
-theorem d_squared_apply : X.d x ≫ X.d _ = 0 := congr_fun X.d_squared _
+theorem d_squared_apply {x : β} : X.d x ≫ X.d _ = 0 := congr_fun X.d_squared _
 
 @[reassoc (attr := simp)]
 theorem eqToHom_f' {X Y : DifferentialObject ℤ (GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β}

Mathlib/Algebra/Homology/ImageToKernel.lean

@@ -24,10 +24,7 @@ renamed `homology'`. It is planned that this definition shall be removed and rep
 
 -/
 
-set_option autoImplicit true
-
-
-universe v u
+universe v u w
 
 open CategoryTheory CategoryTheory.Limits
 

Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

@@ -29,8 +29,6 @@ and `S.homology`.
 
 -/
 
-set_option autoImplicit true
-
 namespace CategoryTheory
 
 open Category Limits
@@ -421,21 +419,22 @@ instance : Epi S.leftHomologyπ := by
   dsimp only [leftHomologyπ]
   infer_instance
 
-lemma leftHomology_ext_iff (f₁ f₂ : S.leftHomology ⟶ A) :
+lemma leftHomology_ext_iff {A : C} (f₁ f₂ : S.leftHomology ⟶ A) :
     f₁ = f₂ ↔ S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂ := by
   rw [cancel_epi]
 
 @[ext]
-lemma leftHomology_ext (f₁ f₂ : S.leftHomology ⟶ A)
+lemma leftHomology_ext {A : C} (f₁ f₂ : S.leftHomology ⟶ A)
     (h : S.leftHomologyπ ≫ f₁ = S.leftHomologyπ ≫ f₂) : f₁ = f₂ := by
   simpa only [leftHomology_ext_iff] using h
 
-lemma cycles_ext_iff (f₁ f₂ : A ⟶ S.cycles) :
+lemma cycles_ext_iff {A : C} (f₁ f₂ : A ⟶ S.cycles) :
     f₁ = f₂ ↔ f₁ ≫ S.iCycles = f₂ ≫ S.iCycles := by
   rw [cancel_mono]
 
 @[ext]
-lemma cycles_ext (f₁ f₂ : A ⟶ S.cycles) (h : f₁ ≫ S.iCycles = f₂ ≫ S.iCycles) : f₁ = f₂ := by
+lemma cycles_ext {A : C} (f₁ f₂ : A ⟶ S.cycles) (h : f₁ ≫ S.iCycles = f₂ ≫ S.iCycles) :
+    f₁ = f₂ := by
   simpa only [cycles_ext_iff] using h
 
 lemma isIso_iCycles (hg : S.g = 0) : IsIso S.iCycles :=