chore: fix tests after #6528 disabled autoimplicits (#6597)

alexjbest · alexjbest · commit 3045aef4ffb0 · 2023-08-15T23:11:50.000Z
These work on the command line and therefore didn't fail in CI (as `lake env lean blah.lean` doesn't pick up the extra lean args?) but as soon as you open one of these files in vscode you get a sea of red errors.

I tried to fix a couple in a minimal way, if there was just for example one universe level missing, for most files the "fix" for now is just reenabling autoimplicits for the file.
This revealed a couple of tests that were incorrectly using an implicit type when they thought they were using Nat.
Two files had issues, that we may want to follow up on  `test/superscript.lean` which failed even with autoimplicits turned on when using an autoimplicit superscript variable (unsure if this was intentional).
And the `ToExpr` deriving handler seems to rely on autoimplicits somehow to work properly in the presence of universe, if an explicit universe variable is added there is still an error.
diff --git a/test/Alias.lean b/test/Alias.lean
@@ -73,10 +73,10 @@ example : True := by
   guard_hyp h2 :ₛ 2 = 2 → 1 + 1 = 2
   trivial
 
-def foo : ℕ → ℕ := id
+def foo : Nat → Nat := id
 
 alias foo ← bar
 
-def baz (n : ℕ) := bar n
+def baz (n : Nat) := bar n
 
 end Alias
diff --git a/test/CategoryTheory/Elementwise.lean b/test/CategoryTheory/Elementwise.lean
@@ -2,6 +2,8 @@ import Std.Tactic.GuardExpr
 import Mathlib.Tactic.CategoryTheory.Elementwise
 --import Mathlib.Algebra.Category.Mon.Basic
 
+set_option autoImplicit true
+
 namespace ElementwiseTest
 open CategoryTheory
 
diff --git a/test/CommDiag.lean b/test/CommDiag.lean
@@ -3,6 +3,7 @@ import ProofWidgets.Component.GoalTypePanel
 
 /-! ## Example use of commutative diagram widgets -/
 
+universe u
 namespace CategoryTheory
 open ProofWidgets
 
diff --git a/test/Continuity.lean b/test/Continuity.lean
@@ -1,6 +1,7 @@
 import Mathlib.Topology.Basic
 import Mathlib.Topology.ContinuousFunction.Basic
 
+set_option autoImplicit true
 section basic
 
 variable [TopologicalSpace W] [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
diff --git a/test/DeriveFintype.lean b/test/DeriveFintype.lean
@@ -2,6 +2,7 @@ import Mathlib.Tactic.DeriveFintype
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Fintype.Pi
 
+set_option autoImplicit true
 namespace tests
 
 /-
diff --git a/test/DeriveToExpr.lean b/test/DeriveToExpr.lean
@@ -3,6 +3,8 @@ import Mathlib.Tactic.DeriveToExpr
 namespace tests
 open Lean
 
+-- TODO this file fails without this line due to a bug in the handler?
+set_option autoImplicit true
 set_option trace.Elab.Deriving.toExpr true
 
 inductive MyMaybe (α : Type u)
diff --git a/test/ExtractGoal.lean b/test/ExtractGoal.lean
@@ -2,6 +2,7 @@ import Mathlib.Tactic.ExtractGoal
 import Mathlib.Data.Nat.Basic
 
 set_option pp.unicode.fun true
+set_option autoImplicit true
 
 -- the example in the documentation for the tactic.
 /-- info: theorem extracted_1 (i j k : ℕ) (h₀ : i ≤ j) (h₁ : j ≤ k) : i ≤ k := sorry -/
diff --git a/test/FBinop.lean b/test/FBinop.lean
@@ -4,6 +4,7 @@ import Mathlib.Data.Finset.Prod
 import Mathlib.Data.SetLike.Basic
 
 universe u v w
+set_option autoImplicit true
 
 namespace FBinopTests
 
diff --git a/test/Find.lean b/test/Find.lean
@@ -1,6 +1,6 @@
 import Mathlib.Tactic.Find
 
-theorem add_comm_zero : 0 + n = n + 0 := Nat.add_comm _ _
+theorem add_comm_zero {n} : 0 + n = n + 0 := Nat.add_comm _ _
 
 #find _ + _ = _ + _
 #find ?n + _ = _ + ?n
diff --git a/test/GCongr/mod.lean b/test/GCongr/mod.lean
@@ -6,6 +6,7 @@ Authors: Heather Macbeth
 import Mathlib.Data.Int.ModEq
 
 /-! # Modular arithmetic tests for the `gcongr` tactic -/
+set_option autoImplicit true
 
 example (ha : a ≡ 2 [ZMOD 4]) : a * b ^ 2 + a ^ 2 * b + 3 ≡ 2 * b ^ 2 + 2 ^ 2 * b + 3 [ZMOD 4] := by
   gcongr
diff --git a/test/GeneralizeProofs.lean b/test/GeneralizeProofs.lean
@@ -3,6 +3,7 @@ import Mathlib.Tactic.GeneralizeProofs
 import Std.Tactic.GuardExpr
 import Mathlib.Tactic.LibrarySearch
 
+set_option autoImplicit true
 def List.nthLe (l : List α) (n) (h : n < l.length) : α := sorry
 
 example : List.nthLe [1, 2] 1 (by simp) = 2 := by
diff --git a/test/HigherOrder.lean b/test/HigherOrder.lean
@@ -1,5 +1,6 @@
 import Mathlib.Tactic.HigherOrder
 
+set_option autoImplicit true
 namespace HigherOrderTest
 
 @[higher_order map_comp_pure]
diff --git a/test/Inhabit.lean b/test/Inhabit.lean
@@ -1,5 +1,7 @@
 import Mathlib.Tactic.Inhabit
 
+universe u
+
 -- Most basic test (prop)
 noncomputable example {p : Prop} [Nonempty p] : Inhabited p := by
   inhabit p
diff --git a/test/InstanceTransparency.lean b/test/InstanceTransparency.lean
@@ -13,6 +13,8 @@ This file checks that this and similar tricks have had the desired effect:
 `with_reducible_and_instances apply mul_le_mul` fails although `apply mul_le_mul` succeeds.
 -/
 
+set_option autoImplicit true
+
 example {a b : α} [LinearOrderedField α] : a / 2 ≤ b / 2 := by
   fail_if_success with_reducible_and_instances apply mul_le_mul -- fails, as desired
   sorry
diff --git a/test/LibrarySearch/basic.lean b/test/LibrarySearch/basic.lean
@@ -4,6 +4,8 @@ import Mathlib.Algebra.Order.Ring.Canonical
 import Mathlib.Data.Quot
 import Mathlib.Data.Nat.Prime
 
+set_option autoImplicit true
+
 -- Enable this option for tracing:
 -- set_option trace.Tactic.librarySearch true
 -- And this option to trace all candidate lemmas before application.
diff --git a/test/LiftLets.lean b/test/LiftLets.lean
@@ -1,6 +1,8 @@
 import Mathlib.Tactic.LiftLets
 import Std.Tactic.GuardExpr
 
+set_option autoImplicit true
+
 example : (let x := 1; x) = 1 := by
   lift_lets
   guard_target =ₛ let x := 1; x = 1
diff --git a/test/MfldSetTac.lean b/test/MfldSetTac.lean
@@ -16,6 +16,8 @@ in realistic conditions. Instead, we create stub definitions and lemmas on objec
 open Lean Meta Elab Tactic
 
 /-! ## Syntax of objects and lemmas needed for testing `MfldSetTac` -/
+
+set_option autoImplicit true
 section stub_lemmas
 
 structure LocalHomeomorph (α : Type u) (β : Type u) extends LocalEquiv α β
diff --git a/test/MkIffOfInductive.lean b/test/MkIffOfInductive.lean
@@ -14,6 +14,7 @@ example : False ↔ False := test.false_iff
 mk_iff_of_inductive_prop True     test.true_iff
 example : True ↔ True := test.true_iff
 
+universe u
 mk_iff_of_inductive_prop Nonempty test.non_empty_iff
 example (α : Sort u) : Nonempty α ↔ ∃ (_ : α), True := test.non_empty_iff α
 
diff --git a/test/NthRewrite.lean b/test/NthRewrite.lean
@@ -3,6 +3,8 @@ import Mathlib.Algebra.Group.Defs
 import Mathlib.Data.Vector
 import Mathlib.Data.Nat.Basic
 
+set_option autoImplicit true
+
 example [AddZeroClass G] {a : G} (h : a = a): a = (a + 0) := by
   nth_rewrite 2 [←add_zero a] at h
   exact h
diff --git a/test/Recall.lean b/test/Recall.lean
@@ -6,6 +6,7 @@ import Mathlib.Data.Complex.Exponential
 
 -- Remark: When the test is run by make/CI, this option is not set, so we set it here.
 set_option pp.unicode.fun true
+set_option autoImplicit true
 
 /-
 Motivating examples from the initial Zulip thread:
diff --git a/test/Simps.lean b/test/Simps.lean
@@ -8,6 +8,7 @@ import Mathlib.Data.Prod.Basic
 -- set_option trace.simps.debug true
 -- set_option trace.simps.verbose true
 -- set_option pp.universes true
+set_option autoImplicit true
 
 open Lean Meta Elab Term Command Simps
 
diff --git a/test/Tauto.lean b/test/Tauto.lean
@@ -5,6 +5,7 @@ Authors: Simon Hudon, David Renshaw
 -/
 import Mathlib.Tactic.Tauto
 
+set_option autoImplicit true
 section tauto₀
 variable (p q r : Prop)
 variable (h : p ∧ q ∨ p ∧ r)
diff --git a/test/Use.lean b/test/Use.lean
@@ -9,6 +9,8 @@ import Mathlib.Tactic.Basic
 
 namespace UseTests
 
+set_option autoImplicit true
+
 example : ∃ x : Nat, x = x := by use 42
 
 -- Since `Eq` is an inductive type, `use` naturally handles it when applying the constructor.
diff --git a/test/Variable.lean b/test/Variable.lean
@@ -5,6 +5,7 @@ import Mathlib.Algebra.Module.LinearMap
 import Mathlib.RingTheory.UniqueFactorizationDomain
 import Std.Tactic.GuardMsgs
 
+set_option autoImplicit true
 namespace Tests
 
 -- Note about tests: these are just testing how `variable?` works, and for the algebra hierarchy
diff --git a/test/abel.lean b/test/abel.lean
@@ -71,4 +71,4 @@ example [AddCommGroup α] (x y z : α) : y = x + z - (x - y + z) := by
   abel
 
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/abel.20bug.3F/near/368707560
-example [AddCommGroup A] (a b s : A) : -b + (s - a) = s - b - a := by abel_nf
+example [AddCommGroup α] (a b s : α) : -b + (s - a) = s - b - a := by abel_nf
diff --git a/test/apply_fun.lean b/test/apply_fun.lean
@@ -5,6 +5,8 @@ import Mathlib.Init.Function
 import Mathlib.Data.Fintype.Card
 -- import Mathlib.Data.Matrix.Basic
 
+
+set_option autoImplicit true
 open Function
 
 example (f : ℕ → ℕ) (h : f x = f y) : x = y := by
diff --git a/test/apply_rules.lean b/test/apply_rules.lean
@@ -1,6 +1,7 @@
 import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Tactic.SolveByElim
 
+set_option autoImplicit true
 open Nat
 
 example {a b c d e : Nat} (h1 : a ≤ b) (h2 : c ≤ d) (h3 : 0 ≤ e) :
diff --git a/test/apply_with.lean b/test/apply_with.lean
@@ -1,5 +1,6 @@
 import Mathlib.Tactic.ApplyWith
 
+set_option autoImplicit true
 example (f : ∀ x : Nat, x = x → α) : α := by
   apply (config := {}) f
   apply rfl
diff --git a/test/borelize.lean b/test/borelize.lean
@@ -1,5 +1,7 @@
 import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
 
+set_option autoImplicit true
+
 example [TopologicalSpace α] [inst : MeasurableSpace α] [BorelSpace α] : MeasurableSet (∅ : Set α) := by
   guard_target = @MeasurableSet α inst ∅
   borelize α
diff --git a/test/byContra.lean b/test/byContra.lean
@@ -3,6 +3,7 @@ import Mathlib.Tactic.ByContra
 import Mathlib.Tactic.Rename
 import Mathlib.Data.Nat.Basic
 
+set_option autoImplicit true
 example (a b : ℕ) (foo : False)  : a < b := by
   by_contra'
   guard_hyp this : b ≤ a
diff --git a/test/cancel_denoms.lean b/test/cancel_denoms.lean
@@ -1,6 +1,8 @@
 import Mathlib.Tactic.CancelDenoms
 import Mathlib.Tactic.Ring
 
+set_option autoImplicit true
+
 section
 variable {α : Type u} [LinearOrderedField α] (a b c d : α)
 
diff --git a/test/cases.lean b/test/cases.lean
@@ -2,6 +2,7 @@ import Mathlib.Tactic.Cases
 import Mathlib.Init.Logic
 import Mathlib.Init.Data.Nat.Notation
 
+set_option autoImplicit true
 example (x : α × β × γ) : True := by
   cases' x with a b; cases' b with b c
   guard_hyp a : α
diff --git a/test/casesm.lean b/test/casesm.lean
@@ -1,6 +1,8 @@
 import Mathlib.Tactic.CasesM
 import Std.Tactic.GuardExpr
 
+set_option autoImplicit true
+
 example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
   casesm* _∨_, _∧_
   · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
diff --git a/test/change.lean b/test/change.lean
@@ -1,6 +1,7 @@
 import Mathlib.Tactic.Basic
 import Std.Tactic.GuardExpr
 
+set_option autoImplicit true
 example : n + 2 = m := by
   change n + 1 + 1 = _
   guard_target =ₛ n + 1 + 1 = m
diff --git a/test/choose.lean b/test/choose.lean
@@ -6,6 +6,8 @@ import Mathlib.Tactic.Choose
 # Tests for the `choose` tactic
 -/
 
+set_option autoImplicit true
+
 example {α : Type} (h : ∀ n m : α, ∀ (h : n = m), ∃ i j : α, i ≠ j ∧ h = h) : True := by
   choose! i j _x _y using h
   trivial
diff --git a/test/congr.lean b/test/congr.lean
@@ -4,6 +4,8 @@ import Mathlib.Algebra.Group.Basic
 import Mathlib.Data.Subtype
 import Mathlib.Data.List.Defs
 
+set_option autoImplicit true
+
 theorem ex1 (a b c : Nat) (h : a = b) : a + c = b + c := by
   congr!
 
diff --git a/test/convert.lean b/test/convert.lean
@@ -3,6 +3,8 @@ import Std.Tactic.GuardExpr
 import Mathlib.Algebra.Group.Basic
 import Mathlib.Data.Set.Image
 
+set_option autoImplicit true
+
 namespace Tests
 
 example (P : Prop) (h : P) : P := by convert h
diff --git a/test/eqns.lean b/test/eqns.lean
@@ -1,14 +1,14 @@
 import Mathlib.Tactic.Eqns
 
-def transpose {m n} (A : m → n → ℕ) : n → m → ℕ
+def transpose {m n} (A : m → n → Nat) : n → m → Nat
   | i, j => A j i
 
-theorem transpose_apply {m n} (A : m → n → ℕ) (i j) :
+theorem transpose_apply {m n} (A : m → n → Nat) (i j) :
   transpose A i j = A j i := rfl
 
 attribute [eqns transpose_apply] transpose
 
-theorem transpose_const {m n} (c : ℕ) :
+theorem transpose_const {m n} (c : Nat) :
     transpose (fun (_i : m) (_j : n) => c) = fun _j _i => c := by
   fail_if_success {rw [transpose]}
   fail_if_success {simp [transpose]}
diff --git a/test/irreducibleDef.lean b/test/irreducibleDef.lean
@@ -1,6 +1,7 @@
 import Mathlib.Tactic.IrreducibleDef
 import Mathlib.Util.WhatsNew
 
+set_option autoImplicit true
 /-- Add two natural numbers, but not during unification. -/
 irreducible_def frobnicate (a b : Nat) :=
   a + b
diff --git a/test/linarith.lean b/test/linarith.lean
@@ -4,6 +4,7 @@ import Mathlib.Data.Rat.Order
 import Mathlib.Data.Int.Order.Basic
 
 set_option linter.unusedVariables false
+set_option autoImplicit true
 
 example [LinearOrderedCommRing α] {a b : α} (h : a < b) (w : b < a) : False := by
   linarith
diff --git a/test/linear_combination.lean b/test/linear_combination.lean
@@ -1,6 +1,9 @@
 import Mathlib.Tactic.LinearCombination
 import Mathlib.Tactic.Linarith
 
+
+set_option autoImplicit true
+
 -- We deliberately mock R here so that we don't have to import the deps
 axiom Real : Type
 notation "ℝ" => Real
diff --git a/test/nomatch.lean b/test/nomatch.lean
@@ -1,5 +1,6 @@
 import Std.Tactic.NoMatch
 
+set_option autoImplicit true
 example : False → α := fun.
 example : False → α := by intro.
 example : ¬ False := fun.
diff --git a/test/nontriviality.lean b/test/nontriviality.lean
@@ -5,6 +5,7 @@ import Mathlib.Data.Nat.Basic
 
 /-! ### Test `nontriviality` with inequality hypotheses -/
 
+set_option autoImplicit true
 
 example {R : Type} [OrderedRing R] {a : R} (h : 0 < a) : 0 < a := by
   nontriviality
diff --git a/test/norm_cast.lean b/test/norm_cast.lean
@@ -11,6 +11,7 @@ import Mathlib.Data.Rat.Cast
 
 -- set_option trace.Tactic.norm_cast true
 -- set_option trace.Meta.Tactic.simp true
+set_option autoImplicit true
 
 variable (an bn cn dn : ℕ) (az bz cz dz : ℤ)
 variable (aq bq cq dq : ℚ)
diff --git a/test/norm_num.lean b/test/norm_num.lean
@@ -9,6 +9,7 @@ import Mathlib.Tactic.NormNum
 /-!
 # Tests for `norm_num` extensions
 -/
+set_option autoImplicit true
 
 -- We deliberately mock R and C here so that we don't have to import the deps
 axiom Real : Type
diff --git a/test/notation3.lean b/test/notation3.lean
@@ -1,6 +1,8 @@
 import Mathlib.Mathport.Notation
 import Mathlib.Init.Data.Nat.Lemmas
 
+set_option autoImplicit true
+
 namespace Test
 
 -- set_option trace.notation3 true
diff --git a/test/positivity.lean b/test/positivity.lean
diff --git a/test/propose.lean b/test/propose.lean
diff --git a/test/push_neg.lean b/test/push_neg.lean
diff --git a/test/restate_axiom.lean b/test/restate_axiom.lean
diff --git a/test/rfl.lean b/test/rfl.lean
diff --git a/test/ring.lean b/test/ring.lean
diff --git a/test/rsuffices.lean b/test/rsuffices.lean
diff --git a/test/says.lean b/test/says.lean
diff --git a/test/simp_intro.lean b/test/simp_intro.lean
diff --git a/test/solve_by_elim/basic.lean b/test/solve_by_elim/basic.lean
diff --git a/test/spread.lean b/test/spread.lean
diff --git a/test/superscript.lean b/test/superscript.lean
diff --git a/test/symm.lean b/test/symm.lean
diff --git a/test/tfae.lean b/test/tfae.lean
diff --git a/test/toAdditive.lean b/test/toAdditive.lean
diff --git a/test/toAdditiveIrredDef.lean b/test/toAdditiveIrredDef.lean
diff --git a/test/trans.lean b/test/trans.lean
