chore: modulize tests (5/N) (leanprover-community#37654)

Co-authored-by: Komyyy <pol_tta@outlook.jp>

Author: Komyyy

MathlibTest/CategoryTheory/PrettyPrinting.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel
 -/
+module
 import Mathlib.CategoryTheory.Functor.Basic
 
 /-!

MathlibTest/DefEqAbuse.lean

@@ -1,3 +1,4 @@
+module
 import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.Order.CompleteLattice.Basic
 import Mathlib.Tactic.DefEqAbuse

MathlibTest/DefEqTransformations.lean

@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.DefEqTransformations
 
 set_option autoImplicit true

MathlibTest/FBinop.lean

@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.FBinop
 import Mathlib.Data.Set.Prod
 import Mathlib.Data.Finset.Prod
@@ -15,7 +16,7 @@ class SProd' (α : Type u) (β : Type v) (γ : outParam (Type w)) where
   sprod : α → β → γ
 
 -- This notation binds more strongly than (pre)images, unions and intersections.
-@[inherit_doc SProd'.sprod] infixr:82 " ×ˢ' " => SProd'.sprod
+@[inherit_doc SProd'.sprod] local infixr:82 " ×ˢ' " => SProd'.sprod
 macro_rules | `($x ×ˢ' $y)   => `(fbinop% SProd'.sprod $x $y)
 
 @[default_instance]

MathlibTest/FunLike.lean

@@ -1,3 +1,4 @@
+module
 import Mathlib.Data.FunLike.Basic
 
 variable {F α β : Sort*} [i : FunLike F α β] (f : F) (a : α)

MathlibTest/InstanceTransparency.lean

@@ -1,3 +1,4 @@
+module
 import Mathlib.Data.Real.Basic
 
 /-! # Test transparency level of `Div` field in `DivInvMonoid`

MathlibTest/Linarith/Basic.lean

@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
 import Mathlib.Algebra.BigOperators.Group.Finset.Pi
@@ -9,7 +10,7 @@ set_option linter.unusedVariables false
 set_option autoImplicit false
 
 open Lean.Elab.Tactic in
-def testSorryTac : TacticM Unit := do
+meta def testSorryTac : TacticM Unit := do
   let e ← getMainTarget
   let t ← `(test_sorry)
   closeMainGoalUsing `sorry fun _ _ => elabTerm t e
@@ -720,11 +721,11 @@ example {x1 x2 x3 x4 x5 x6 x7 x8 : ℚ} :
 
 section findSquares
 
-private abbrev wrapped (z : ℤ) : ℤ := z
+abbrev wrapped (z : ℤ) : ℤ := z
 /-- the `findSquares` preprocessor can look through reducible defeq -/
 example (x : ℤ) : 0 ≤ x * wrapped x := by nlinarith
 
-private def tightlyWrapped (z : ℤ) : ℤ := z
+def tightlyWrapped (z : ℤ) : ℤ := z
 /--
 error: linarith failed to find a contradiction
 case h

MathlibTest/Linarith/NNReal.lean

@@ -1,3 +1,4 @@
+module
 import Mathlib.Tactic.Linarith.NNRealPreprocessor
 import Mathlib.Data.ENNReal.Operations
 import Mathlib.Data.ENNReal.Inv

MathlibTest/Monotonicity.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Simon Hudon
 -/
+module
 import Mathlib.Algebra.Order.Ring.Defs
 import Mathlib.Data.List.Defs
 import Mathlib.Tactic.Monotonicity

MathlibTest/Replace.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Arthur Paulino. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Arthur Paulino
 -/
+module
 import Mathlib.Tactic.Replace
 
 set_option linter.unusedVariables false