chore: disable relaxedAutoImplicit (#5277)

kim-em · Scott Morrison · kim-em · commit 52d95f2b56b6 · 2023-06-25T11:21:15.000Z
We disable the "relaxed" auto-implicit feature, so only single character identifiers become eligible as auto-implicits. See discussion on [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Auto-implicits) and [2](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60autoImplicit.20true.60.20is.20evil). Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>
diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
@@ -57,7 +57,7 @@ that are prime and do not contain the irrelevant ideal. -/
 structure ProjectiveSpectrum where
   asHomogeneousIdeal : HomogeneousIdeal 𝒜
   isPrime : asHomogeneousIdeal.toIdeal.IsPrime
-  not_irrelevant_le : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ as_homogeneous_ideal
+  not_irrelevant_le : ¬HomogeneousIdeal.irrelevant 𝒜 ≤ asHomogeneousIdeal
 #align projective_spectrum ProjectiveSpectrum
 
 attribute [instance] ProjectiveSpectrum.isPrime
diff --git a/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean b/Mathlib/CategoryTheory/Limits/FilteredColimitCommutesFiniteLimit.lean
@@ -39,10 +39,10 @@ namespace CategoryTheory.Limits
 
 variable {J K : Type v} [SmallCategory J] [SmallCategory K]
 
-/-- `(G ⋙ lim).obj S` = `limit (G.obj S)` definitionally, so this
+/-- `(G ⋙ lim).obj j` = `limit (G.obj j)` definitionally, so this
 is just a variant of `limit_ext'`. -/
-@[ext] lemma comp_lim_obj_ext {G : J ⥤ K ⥤ Type v} (x y : (G ⋙ lim).obj S) (w : ∀ (j : K),
-    limit.π (G.obj S) j x = limit.π (G.obj S) j y) : x = y :=
+@[ext] lemma comp_lim_obj_ext {j : J} {G : J ⥤ K ⥤ Type v} (x y : (G ⋙ lim).obj j)
+    (w : ∀ (k : K), limit.π (G.obj j) k x = limit.π (G.obj j) k y) : x = y :=
   limit_ext' _ x y w
 
 variable (F : J × K ⥤ Type v)
@@ -110,7 +110,7 @@ theorem colimitLimitToLimitColimit_injective :
               Finset.mem_image, heq_iff_eq]
             refine' ⟨j, _⟩
             simp only [heq_iff_eq] ))
-    have gH : 
+    have gH :
       ∀ j, (⟨ky, k j, kyO, kjO j, g j⟩ : Σ' (X Y : K) (_ : X ∈ O) (_ : Y ∈ O), X ⟶ Y) ∈ H :=
       fun j =>
       Finset.mem_union.mpr
diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean
@@ -1850,7 +1850,8 @@ theorem stepAux_read (f : Γ → Stmt'₁) (v : σ) (L R : ListBlank Γ) :
   rfl
 #align turing.TM1to1.step_aux_read Turing.TM1to1.stepAux_read
 
-theorem tr_respects : Respects (step M) (step (tr enc dec M)) fun c₁ c₂ ↦ trCfg enc enc₀ c₁ = c₂ :=
+theorem tr_respects {enc₀} :
+    Respects (step M) (step (tr enc dec M)) fun c₁ c₂ ↦ trCfg enc enc₀ c₁ = c₂ :=
   fun_respects.2 fun ⟨l₁, v, T⟩ ↦ by
     obtain ⟨L, R, rfl⟩ := T.exists_mk'
     cases' l₁ with l₁
diff --git a/Mathlib/Data/HashMap.lean b/Mathlib/Data/HashMap.lean
@@ -35,7 +35,7 @@ end Std.HashMap
 namespace Std.RBSet
 
 /-- Insert all elements of a list into an `RBSet`. -/
-def insertList (m : RBSet α cmp) (L : List α) : RBSet α cmp :=
+def insertList {cmp} (m : RBSet α cmp) (L : List α) : RBSet α cmp :=
   L.foldl (fun m a => m.insert a) m
 
 end Std.RBSet
diff --git a/Mathlib/Data/List/Range.lean b/Mathlib/Data/List/Range.lean
@@ -31,7 +31,7 @@ namespace List
 
 variable {α : Type u}
 
-@[simp] theorem range'_one : range' s 1 step = [s] := rfl
+@[simp] theorem range'_one {step} : range' s 1 step = [s] := rfl
 
 #align list.length_range' List.length_range'
 #align list.range'_eq_nil List.range'_eq_nil
diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean
@@ -1253,11 +1253,15 @@ def LiftRelAux (R : α → β → Prop) (C : Computation α → Computation β 
 --porting note: was attribute [simp] LiftRelAux but right now `simp` on defs is a Lean 4 catastrophe
 -- Instead we add the equation lemmas and tag them @[simp]
 @[simp] lemma LiftRelAux_inl_inl : LiftRelAux R C (Sum.inl a) (Sum.inl b) = R a b := rfl
-@[simp] lemma LiftRelAux_inl_inr : LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ b, b ∈ cb ∧ R a b :=
+@[simp] lemma LiftRelAux_inl_inr {cb} :
+    LiftRelAux R C (Sum.inl a) (Sum.inr cb) = ∃ b, b ∈ cb ∧ R a b :=
   rfl
-@[simp] lemma LiftRelAux_inr_inl : LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ a, a ∈ ca ∧ R a b :=
+@[simp] lemma LiftRelAux_inr_inl {ca} :
+    LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ a, a ∈ ca ∧ R a b :=
+  rfl
+@[simp] lemma LiftRelAux_inr_inr {ca cb} :
+    LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb :=
   rfl
-@[simp] lemma LiftRelAux_inr_inr : LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb := rfl
 
 @[simp]
 theorem LiftRelAux.ret_left (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a cb) :
diff --git a/Mathlib/Data/Stream/Init.lean b/Mathlib/Data/Stream/Init.lean
@@ -607,7 +607,8 @@ theorem get?_take_succ (n : Nat) (s : Stream' α) :
   get?_take (Nat.lt_succ_self n)
 #align stream.nth_take_succ Stream'.get?_take_succ
 
-@[simp] theorem dropLast_take : (Stream'.take n xs).dropLast = Stream'.take (n-1) xs := by
+@[simp] theorem dropLast_take {xs : Stream' α} :
+    (Stream'.take n xs).dropLast = Stream'.take (n-1) xs := by
   cases n; case zero => simp
   case succ n => rw [take_succ', List.dropLast_concat, Nat.succ_sub_one]
 
diff --git a/Mathlib/Init/Algebra/Classes.lean b/Mathlib/Init/Algebra/Classes.lean
@@ -68,7 +68,7 @@ class IsSymmOp (α : Type u) (β : Type v) (op : α → α → β) : Prop where
 class IsCommutative (α : Type u) (op : α → α → α) : Prop where
   comm : ∀ a b, op a b = op b a
 
-instance [IsCommutative α op] : Lean.IsCommutative op where
+instance {op} [IsCommutative α op] : Lean.IsCommutative op where
   comm := IsCommutative.comm
 
 instance isSymmOp_of_isCommutative (α : Type u) (op : α → α → α)
@@ -79,7 +79,7 @@ instance isSymmOp_of_isCommutative (α : Type u) (op : α → α → α)
 class IsAssociative (α : Type u) (op : α → α → α) : Prop where
   assoc : ∀ a b c, op (op a b) c = op a (op b c)
 
-instance [IsAssociative α op] : Lean.IsAssociative op where
+instance {op} [IsAssociative α op] : Lean.IsAssociative op where
   assoc := IsAssociative.assoc
 
 /-- A binary operation with a left identity. -/
@@ -90,7 +90,7 @@ class IsLeftId (α : Type u) (op : α → α → α) (o : outParam α) : Prop wh
 class IsRightId (α : Type u) (op : α → α → α) (o : outParam α) : Prop where
   right_id : ∀ a, op a o = a
 
-instance [IsLeftId α op o] [IsRightId α op o] : Lean.IsNeutral op o where
+instance {op} [IsLeftId α op o] [IsRightId α op o] : Lean.IsNeutral op o where
   left_neutral := IsLeftId.left_id
   right_neutral := IsRightId.right_id
 
@@ -109,7 +109,7 @@ class IsRightCancel (α : Type u) (op : α → α → α) : Prop where
 class IsIdempotent (α : Type u) (op : α → α → α) : Prop where
   idempotent : ∀ a, op a a = a
 
-instance [IsIdempotent α op] : Lean.IsIdempotent op where
+instance {op} [IsIdempotent α op] : Lean.IsIdempotent op where
   idempotent := IsIdempotent.idempotent
 
 --class IsLeftDistrib (α : Type u) (op₁ : α → α → α) (op₂ : outParam <| α → α → α) : Prop where
diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
@@ -1367,11 +1367,11 @@ instance linearOrder: LinearOrder PUnit where
   le_antisymm := by intros; rfl
   lt_iff_le_not_le := by simp only [not_true, and_false, forall_const]
 
-theorem max_eq : max a b = star :=
+theorem max_eq : max a b = unit :=
   rfl
 #align punit.max_eq PUnit.max_eq
 
-theorem min_eq : min a b = star :=
+theorem min_eq : min a b = unit :=
   rfl
 #align punit.min_eq PUnit.min_eq
 
diff --git a/Mathlib/Order/OmegaCompletePartialOrder.lean b/Mathlib/Order/OmegaCompletePartialOrder.lean
@@ -572,7 +572,7 @@ if for every chain `c : chain α`, `f (⊔ i, c i) = ⊔ i, f (c i)`.
 This is just the bundled version of `OrderHom.continuous`. -/
 structure ContinuousHom extends OrderHom α β where
   /-- The underlying function of a `ContinuousHom` is continuous, i.e. it preserves `ωSup` -/
-  cont : Continuous (OrderHom.mk toFun Monotone')
+  cont : Continuous (OrderHom.mk toFun monotone')
 #align omega_complete_partial_order.continuous_hom OmegaCompletePartialOrder.ContinuousHom
 
 attribute [nolint docBlame] ContinuousHom.toOrderHom
@@ -813,7 +813,7 @@ def apply : (α →𝒄 β) × α →𝒄 β where
     dsimp
     trans y.fst x.snd <;> [apply h.1; apply y.1.monotone h.2]
   cont := by
-    intro _ c
+    intro c
     apply le_antisymm
     · apply ωSup_le
       intro i
@@ -851,7 +851,7 @@ def flip {α : Type _} (f : α → β →𝒄 γ) :
     β →𝒄 α → γ where
   toFun x y := f y x
   monotone' x y h a := (f a).monotone h
-  cont := by intro _ _; ext x; change f _ _ = _; rw [(f _).continuous]; rfl
+  cont := by intro _; ext x; change f _ _ = _; rw [(f _).continuous]; rfl
 #align omega_complete_partial_order.continuous_hom.flip OmegaCompletePartialOrder.ContinuousHom.flip
 #align omega_complete_partial_order.continuous_hom.flip_apply OmegaCompletePartialOrder.ContinuousHom.flip_apply
 
diff --git a/Mathlib/SetTheory/Game/PGame.lean b/Mathlib/SetTheory/Game/PGame.lean
@@ -100,6 +100,9 @@ An interested reader may like to formalise some of the material from
 
 open Function Relation
 
+-- This is file, we'd like to be able to use multi-character auto-implicits.
+set_option relaxedAutoImplicit true
+
 /-! ### Pre-game moves -/
 
 
diff --git a/Mathlib/Tactic/IntervalCases.lean b/Mathlib/Tactic/IntervalCases.lean
@@ -32,6 +32,8 @@ where the hypotheses should be of the form `hl : a ≤ n` and `hu : n < b`. In t
 -/
 
 set_option linter.unusedVariables false
+-- In this file we would like to be able to use multi-character auto-implicits.
+set_option relaxedAutoImplicit true
 
 namespace Mathlib.Tactic
 
diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean
@@ -91,6 +91,9 @@ ring subexpressions of type `ℕ`.
 -/
 def sℕ : Q(CommSemiring ℕ) := q(instCommSemiringNat)
 
+-- In this file, we would like to use multi-character auto-implicits.
+set_option relaxedAutoImplicit true
+
 mutual
 
 /-- The base `e` of a normalized exponent expression. -/
diff --git a/Mathlib/Tactic/Ring/RingNF.lean b/Mathlib/Tactic/Ring/RingNF.lean
@@ -17,6 +17,9 @@ such as `sin (x + y) + sin (y + x) = 2 * sin (x + y)`.
 
 -/
 
+-- In this file we would like to be able to use multi-character auto-implicits.
+set_option relaxedAutoImplicit true
+
 namespace Mathlib.Tactic
 open Lean hiding Rat
 open Qq Meta
diff --git a/Mathlib/Tactic/Sat/FromLRAT.lean b/Mathlib/Tactic/Sat/FromLRAT.lean
@@ -151,7 +151,7 @@ def Valuation.mk : List Prop → Valuation
 
 /-- The fundamental relationship between `mk` and `implies`:
 `(mk ps).implies p ps 0` is equivalent to `p`. -/
-theorem Valuation.mk_implies (as₁) : as = List.reverseAux as₁ ps →
+theorem Valuation.mk_implies {as ps} (as₁) : as = List.reverseAux as₁ ps →
   (Valuation.mk as).implies p ps as₁.length → p := by
   induction ps generalizing as₁ with
   | nil => exact fun _ ↦ id
@@ -170,7 +170,7 @@ structure Fmla.reify (v : Valuation) (f : Fmla) (p : Prop) : Prop where
 /-- If `f` is unsatisfiable, and every `v` which agrees with `ps` implies `¬⟦f⟧_v → p`, then `p`.
 Equivalently, there exists a valuation `v` which agrees with `ps`,
 and every such valuation yields `¬⟦f⟧_v` because `f` is unsatisfiable. -/
-theorem Fmla.refute (f : Fmla) (hf : f.proof [])
+theorem Fmla.refute {ps} (f : Fmla) (hf : f.proof [])
   (hv : ∀ v, Valuation.implies v (Fmla.reify v f p) ps 0) : p :=
   (Valuation.mk_implies [] rfl (hv _)).1 (hf _)
 
diff --git a/Mathlib/Testing/SlimCheck/Testable.lean b/Mathlib/Testing/SlimCheck/Testable.lean
@@ -255,6 +255,8 @@ instance iffTestable [Testable ((p ∧ q) ∨ (¬ p ∧ ¬ q))] : Testable (p 
     let h ← runProp ((p ∧ q) ∨ (¬ p ∧ ¬ q)) cfg min
     pure $ iff iff_iff_and_or_not_and_not h
 
+variable {var : String}
+
 instance decGuardTestable [PrintableProp p] [Decidable p] {β : p → Prop} [∀ h, Testable (β h)] :
     Testable (NamedBinder var $ ∀ h, β h) where
   run := λ cfg min => do
diff --git a/Mathlib/Topology/MetricSpace/Gluing.lean b/Mathlib/Topology/MetricSpace/Gluing.lean
@@ -482,7 +482,7 @@ def GlueSpace (hΦ : Isometry Φ) (hΨ : Isometry Ψ) : Type _ :=
 #align metric.glue_space Metric.GlueSpace
 
 -- porting note: TODO: w/o `@`, tries to generate some `[MetricSpace _]` before finding `X` `Y`
-instance : MetricSpace (@GlueSpace X Y Z _ _ _ _ _ _ hΦ hΨ) :=
+instance (hΦ : Isometry Φ) (hΨ : Isometry Ψ) : MetricSpace (@GlueSpace X Y Z _ _ _ _ _ _ hΦ hΨ) :=
   inferInstanceAs <| MetricSpace <|
     @UniformSpace.SeparationQuotient _ (gluePremetric hΦ hΨ).toUniformSpace
 
diff --git a/Mathlib/Util/Syntax.lean b/Mathlib/Util/Syntax.lean
@@ -25,5 +25,5 @@ The given array does not include the separators.
 
 Like `Syntax.SepArray.ofElems` but for typed syntax.
 -/
-def Syntax.TSepArray.ofElems (elems : Array (TSyntax k)) : TSepArray k sep :=
+def Syntax.TSepArray.ofElems {sep} (elems : Array (TSyntax k)) : TSepArray k sep :=
   .mk (SepArray.ofElems (sep := sep) elems).1
diff --git a/lakefile.lean b/lakefile.lean
@@ -3,7 +3,8 @@ import Lake
 open Lake DSL
 
 def moreServerArgs := #[
-  "-Dpp.unicode.fun=true" -- pretty-prints `fun a ↦ b`
+  "-Dpp.unicode.fun=true", -- pretty-prints `fun a ↦ b`
+  "-DrelaxedAutoImplicit=false"
 ]
 
 -- These settings only apply during `lake build`, but not in VSCode editor.
