diff --git a/src/Init/Data/Ord/Basic.lean b/src/Init/Data/Ord/Basic.lean
index 8ceab3a50b..d9c32974c6 100644
--- a/src/Init/Data/Ord/Basic.lean
+++ b/src/Init/Data/Ord/Basic.lean
@@ -96,7 +96,7 @@ Ordering.lt
   | a => a
 
 /-- Version of `Ordering.then'` for proof by reflection. -/
-noncomputable def then' (a b : Ordering) : Ordering :=
+@[expose] noncomputable def then' (a b : Ordering) : Ordering :=
   Ordering.rec a b a a
 
 /--
diff --git a/src/Init/Grind/Ordered/Linarith.lean b/src/Init/Grind/Ordered/Linarith.lean
index 2efb0b3808..e9cea89c81 100644
--- a/src/Init/Grind/Ordered/Linarith.lean
+++ b/src/Init/Grind/Ordered/Linarith.lean
@@ -12,7 +12,7 @@ public import all Init.Data.Ord.Basic
 public import all Init.Data.AC
 public import Init.Data.RArray
 
-public section
+@[expose] public section
 
 /-!
 Support for the linear arithmetic module for `IntModule` in `grind`
diff --git a/src/Init/Grind/ToInt.lean b/src/Init/Grind/ToInt.lean
index 258d641e6a..07775d131a 100644
--- a/src/Init/Grind/ToInt.lean
+++ b/src/Init/Grind/ToInt.lean
@@ -46,9 +46,9 @@ instance : LawfulBEq IntInterval where
 namespace IntInterval
 
 /-- The interval `[0, 2^n)`. -/
-abbrev uint (n : Nat) := IntInterval.co 0 (2 ^ n)
+@[expose] abbrev uint (n : Nat) := IntInterval.co 0 (2 ^ n)
 /-- The interval `[-2^(n-1), 2^(n-1))`. -/
-abbrev sint (n : Nat) := IntInterval.co (-(2 ^ (n - 1))) (2 ^ (n - 1))
+@[expose] abbrev sint (n : Nat) := IntInterval.co (-(2 ^ (n - 1))) (2 ^ (n - 1))
 
 /-- The lower bound of the interval, if finite. -/
 @[expose] def lo? (i : IntInterval) : Option Int :=
@@ -98,7 +98,7 @@ instance : Membership Int IntInterval where
 theorem nonEmpty_of_mem {x : Int} {i : IntInterval} (h : x ∈ i) : i.nonEmpty := by
   cases i <;> simp_all <;> omega
 
-@[simp]
+@[simp, expose]
 def wrap (i : IntInterval) (x : Int) : Int :=
   match i with
   | co lo hi => (x - lo) % (hi - lo) + lo
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
index 9a9f501712..da4f18cd38 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
@@ -31,11 +31,13 @@ def Mon.lcm : Mon → Mon → Mon
     | .lt => .mult pw₁ (lcm m₁ (.mult pw₂ m₂))
     | .gt => .mult pw₂ (lcm (.mult pw₁ m₁) m₂)
 
+-- Remark: we expose `Mon.divides` and `Mon.div` because we use then to write tests using `rfl`
+
 /--
 `divides m₁ m₂` returns `true` if monomial `m₁` divides `m₂`
 Example: `x^2.z` divides `w.x^3.y^2.z`
 -/
-def Mon.divides : Mon → Mon → Bool
+@[expose] def Mon.divides : Mon → Mon → Bool
   | .unit, _ => true
   | _, .unit => false
   | .mult pw₁ m₁, .mult pw₂ m₂ =>
@@ -49,7 +51,7 @@ Given `m₁` and `m₂` such that `m₂.divides m₁`, then
 `m₁.div m₂` returns the result.
 Example `w.x^3.y^2.z` div `x^2.z` returns `w.x.y^2`
 -/
-def Mon.div : Mon → Mon → Mon
+@[expose] def Mon.div : Mon → Mon → Mon
   | m₁, .unit => m₁
   | .unit, _  => .unit -- reachable only if pre-condition does not hold
   | .mult pw₁ m₁, .mult pw₂ m₂ =>
diff --git a/src/Std.lean b/src/Std.lean
index 9db9fe5433..56724b38a4 100644
--- a/src/Std.lean
+++ b/src/Std.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich
 -/
+module
 prelude
 import Std.Data
 import Std.Do
diff --git a/tests/lean/run/grind_9216.lean b/tests/lean/run/grind_9216.lean
index a82f929859..2d12578ef9 100644
--- a/tests/lean/run/grind_9216.lean
+++ b/tests/lean/run/grind_9216.lean
@@ -1,3 +1,4 @@
+module
 import Std.Data.HashSet
 
 open Std
diff --git a/tests/lean/run/grind_9321.lean b/tests/lean/run/grind_9321.lean
index 93f168428f..28c4d24164 100644
--- a/tests/lean/run/grind_9321.lean
+++ b/tests/lean/run/grind_9321.lean
@@ -1,3 +1,4 @@
+module
 example (z : Int) : z + (Int.cast (R := Int) (-2)) = z - 2 := by grind
 
 attribute [local instance] Lean.Grind.Semiring.natCast Lean.Grind.Ring.intCast
diff --git a/tests/lean/run/grind_9427.lean b/tests/lean/run/grind_9427.lean
index 0c7daa561c..a560642109 100644
--- a/tests/lean/run/grind_9427.lean
+++ b/tests/lean/run/grind_9427.lean
@@ -1,3 +1,4 @@
+module
 example {n} (x y : BitVec n) : x * y = y * x := by
   grind
 
diff --git a/tests/lean/run/grind_9467.lean b/tests/lean/run/grind_9467.lean
index 3b3b776314..e582c3580d 100644
--- a/tests/lean/run/grind_9467.lean
+++ b/tests/lean/run/grind_9467.lean
@@ -1,3 +1,4 @@
+module
 example (x y : Nat) : (x : Int) - (y : Int) = 0 → x = y := by
   grind
 
diff --git a/tests/lean/run/grind_9477.lean b/tests/lean/run/grind_9477.lean
index ae7a7c6aa4..f11d7b281d 100644
--- a/tests/lean/run/grind_9477.lean
+++ b/tests/lean/run/grind_9477.lean
@@ -1,3 +1,4 @@
+module
 structure T where
   upper_bound : Nat
 
diff --git a/tests/lean/run/grind_9485.lean b/tests/lean/run/grind_9485.lean
index bc392e1a9f..ae6b1c24c3 100644
--- a/tests/lean/run/grind_9485.lean
+++ b/tests/lean/run/grind_9485.lean
@@ -1,3 +1,4 @@
+module
 variable (G : Type)
 
 structure G' where p : G
diff --git a/tests/lean/run/grind_9562.lean b/tests/lean/run/grind_9562.lean
index e608833ec2..2f9a434228 100644
--- a/tests/lean/run/grind_9562.lean
+++ b/tests/lean/run/grind_9562.lean
@@ -1,3 +1,4 @@
+module
 axiom A : Type
 axiom angle (x y z : A) : Int
 axiom pi : Int
diff --git a/tests/lean/run/grind_9572.lean b/tests/lean/run/grind_9572.lean
index ea4372ad0e..f1bc1cff43 100644
--- a/tests/lean/run/grind_9572.lean
+++ b/tests/lean/run/grind_9572.lean
@@ -1,3 +1,4 @@
+module
 def List.Disjoint (l₁ l₂ : List α) : Prop :=
   ∀ ⦃a⦄, a ∈ l₁ → a ∈ l₂ → False
 
@@ -11,7 +12,7 @@ l : List Nat
 h :
   ¬List.Pairwise
       (fun x y =>
-        (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+        List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
           (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
       l
 ⊢ False
@@ -19,13 +20,13 @@ h :
   [facts] Asserted facts
     [prop] ¬List.Pairwise
             (fun x y =>
-              (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+              List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
                 (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
             l
   [eqc] False propositions
     [prop] List.Pairwise
           (fun x y =>
-            (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
+            List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
               (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
           l
 -/
diff --git a/tests/lean/run/grind_9610.lean b/tests/lean/run/grind_9610.lean
index bf86f4f216..f1ead19cb3 100644
--- a/tests/lean/run/grind_9610.lean
+++ b/tests/lean/run/grind_9610.lean
@@ -1,3 +1,4 @@
+module
 set_option warn.sorry false
 abbrev sixteen : UInt32 := 16
 
diff --git a/tests/lean/run/grind_9769.lean b/tests/lean/run/grind_9769.lean
index 1579ee05d4..d66b822b8f 100644
--- a/tests/lean/run/grind_9769.lean
+++ b/tests/lean/run/grind_9769.lean
@@ -1,3 +1,4 @@
+module
 def Foo (n : Nat) := Σ (m : Nat), {f : Fin (n + 2) → Fin (m + 2) // f 0 = 0}
 
 variable (n : Nat)
diff --git a/tests/lean/run/grind_9825.lean b/tests/lean/run/grind_9825.lean
index 68b8566212..0753d3b924 100644
--- a/tests/lean/run/grind_9825.lean
+++ b/tests/lean/run/grind_9825.lean
@@ -1,3 +1,4 @@
+module
 import Lean.Elab.Command
 
 theorem extracted_1_1 {K : Type} [Lean.Grind.Field K] (pB ppB pBf ifpnf : K) :
diff --git a/tests/lean/run/grind_9828.lean b/tests/lean/run/grind_9828.lean
index c1f2050d2e..732e8de6b7 100644
--- a/tests/lean/run/grind_9828.lean
+++ b/tests/lean/run/grind_9828.lean
@@ -1,3 +1,4 @@
+module
 def Xor' (a b : Prop) := (a ∧ ¬b) ∨ (b ∧ ¬a)
 
 @[grind =] theorem xor_def {a b : Prop} : Xor' a b ↔ (a ∧ ¬b) ∨ (b ∧ ¬a) := Iff.rfl
diff --git a/tests/lean/run/grind_9830.lean b/tests/lean/run/grind_9830.lean
index 49585efd5d..0792becede 100644
--- a/tests/lean/run/grind_9830.lean
+++ b/tests/lean/run/grind_9830.lean
@@ -1,3 +1,4 @@
+module
 abbrev F : Fin 3 → Nat
 | 0 => 0
 | 1 => 1
diff --git a/tests/lean/run/grind_9854.lean b/tests/lean/run/grind_9854.lean
index 877ba15403..5afc0ae9f8 100644
--- a/tests/lean/run/grind_9854.lean
+++ b/tests/lean/run/grind_9854.lean
@@ -1,2 +1,3 @@
+module
 example (x: Nat) : UInt32.size - x < UInt64.size := by
   grind only
diff --git a/tests/lean/run/grind_9856.lean b/tests/lean/run/grind_9856.lean
index 949e3ca832..4679d76f45 100644
--- a/tests/lean/run/grind_9856.lean
+++ b/tests/lean/run/grind_9856.lean
@@ -1,3 +1,4 @@
+module
 inductive T (a:Type) where
   | constuctor1: T a
   | constuctor2: T a
diff --git a/tests/lean/run/grind_9897.lean b/tests/lean/run/grind_9897.lean
index d8bc9810c5..a8545c5429 100644
--- a/tests/lean/run/grind_9897.lean
+++ b/tests/lean/run/grind_9897.lean
@@ -1,3 +1,4 @@
+module
 def Set' (α : Type u) := α → Prop
 
 namespace Set'
diff --git a/tests/lean/run/grind_9899.lean b/tests/lean/run/grind_9899.lean
index 32dcb40fd1..b4ab28e6a4 100644
--- a/tests/lean/run/grind_9899.lean
+++ b/tests/lean/run/grind_9899.lean
@@ -1,3 +1,4 @@
+module
 namespace List
 -- Should not panic
 #guard_msgs (drop error) in
diff --git a/tests/lean/run/grind_9907.lean b/tests/lean/run/grind_9907.lean
index 76bc6e78cf..1b1d2777ed 100644
--- a/tests/lean/run/grind_9907.lean
+++ b/tests/lean/run/grind_9907.lean
@@ -1,3 +1,4 @@
+module
 structure DepThing {α : Type u} (l : List α) : Type u where
   suffix : List α
   property : suffix = l
diff --git a/tests/lean/run/grind_9948.lean b/tests/lean/run/grind_9948.lean
index ca51d1f542..ea700d11a5 100644
--- a/tests/lean/run/grind_9948.lean
+++ b/tests/lean/run/grind_9948.lean
@@ -1,3 +1,4 @@
+module
 theorem sum_of_n (n : Nat) :
   (List.range (n + 1)).sum = n * (n + 1) / 2 := by
   induction n with
diff --git a/tests/lean/run/grind_Poly_mul_0_bug.lean b/tests/lean/run/grind_Poly_mul_0_bug.lean
index f05b84e85d..96d0029935 100644
--- a/tests/lean/run/grind_Poly_mul_0_bug.lean
+++ b/tests/lean/run/grind_Poly_mul_0_bug.lean
@@ -1,3 +1,4 @@
+module
 open Int.Linear
 
 def p : Poly := .add 1 1 <| .add 2 0 <| .num 3
diff --git a/tests/lean/run/grind_abstract_mvars.lean b/tests/lean/run/grind_abstract_mvars.lean
index 9d847f40c6..abaaeb5d60 100644
--- a/tests/lean/run/grind_abstract_mvars.lean
+++ b/tests/lean/run/grind_abstract_mvars.lean
@@ -1,3 +1,4 @@
+module
 example (xs : Array Nat)
     (w : ∀ (j : Nat), 0 ≤ j → ∀ (x : j < xs.size / 2), xs[j] = xs[xs.size - 1 - j])
     (i : Nat) (hi₁ : i < xs.reverse.size) (hi₂ : i < xs.size) (h : i < xs.size / 2) : xs.reverse[i] = xs[i] := by
diff --git a/tests/lean/run/grind_activate_local_issue.lean b/tests/lean/run/grind_activate_local_issue.lean
index 5fd3e8be3e..2937c0087e 100644
--- a/tests/lean/run/grind_activate_local_issue.lean
+++ b/tests/lean/run/grind_activate_local_issue.lean
@@ -1,3 +1,4 @@
+module
 opaque p : Nat → Prop
 
 -- Local forall should be activated only once
diff --git a/tests/lean/run/grind_all_singleton_patterns.lean b/tests/lean/run/grind_all_singleton_patterns.lean
index 039547f71c..586862269d 100644
--- a/tests/lean/run/grind_all_singleton_patterns.lean
+++ b/tests/lean/run/grind_all_singleton_patterns.lean
@@ -1,3 +1,4 @@
+module
 example (p : Nat → Prop) (h₁ : x < n) (h₂ : ¬ p x) : ∃ i, i < n ∧ ¬ p i := by
   grind
 
diff --git a/tests/lean/run/grind_append_issue.lean b/tests/lean/run/grind_append_issue.lean
index e1b3888443..dc3dda32b2 100644
--- a/tests/lean/run/grind_append_issue.lean
+++ b/tests/lean/run/grind_append_issue.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 attribute [grind] List.length_cons List.length_nil List.length_append
 attribute [grind] List.nil_append List.getElem_cons
diff --git a/tests/lean/run/grind_arith_nonstd_insts.lean b/tests/lean/run/grind_arith_nonstd_insts.lean
index 6a93bf1d5a..328aaa4688 100644
--- a/tests/lean/run/grind_arith_nonstd_insts.lean
+++ b/tests/lean/run/grind_arith_nonstd_insts.lean
@@ -1,3 +1,4 @@
+module
 class Distrib (R : Type _) extends Mul R where
 
 namespace Nat
diff --git a/tests/lean/run/grind_array.lean b/tests/lean/run/grind_array.lean
index 7785e14f0a..9616d0145d 100644
--- a/tests/lean/run/grind_array.lean
+++ b/tests/lean/run/grind_array.lean
@@ -1,2 +1,3 @@
+module
 example {l : List α} {i : USize} {a : α} {h : i.toNat < l.toArray.size} :
     l.toArray.uset i a h = (l.set i.toNat a).toArray := by grind
diff --git a/tests/lean/run/grind_assoc.lean b/tests/lean/run/grind_assoc.lean
index 5ab8bed587..97d6cf1b65 100644
--- a/tests/lean/run/grind_assoc.lean
+++ b/tests/lean/run/grind_assoc.lean
@@ -1,3 +1,4 @@
+module
 def α : Type := sorry
 instance : Mul α := sorry
 
diff --git a/tests/lean/run/grind_attrs.lean b/tests/lean/run/grind_attrs.lean
index f12fced84d..baef7ac43a 100644
--- a/tests/lean/run/grind_attrs.lean
+++ b/tests/lean/run/grind_attrs.lean
@@ -1,3 +1,4 @@
+module
 opaque R : Nat → Nat → Prop
 
 @[grind ->]
diff --git a/tests/lean/run/grind_beta.lean b/tests/lean/run/grind_beta.lean
index 983c0fdfe5..c4e4c21572 100644
--- a/tests/lean/run/grind_beta.lean
+++ b/tests/lean/run/grind_beta.lean
@@ -1,3 +1,4 @@
+module
 def f (x : Nat) : Nat → Nat → Nat :=
   match x with
   | 0 => fun _ _ => 0
diff --git a/tests/lean/run/grind_big_poly.lean b/tests/lean/run/grind_big_poly.lean
index f9f87e5f7b..5d6564c472 100644
--- a/tests/lean/run/grind_big_poly.lean
+++ b/tests/lean/run/grind_big_poly.lean
@@ -1,3 +1,4 @@
+module
 /--
 trace: [grind.issues] maximum recursion depth has been reached
     use `set_option maxRecDepth <num>` to increase limit
diff --git a/tests/lean/run/grind_bigstep.lean b/tests/lean/run/grind_bigstep.lean
index 4d38cc687b..d4d04fae1e 100644
--- a/tests/lean/run/grind_bigstep.lean
+++ b/tests/lean/run/grind_bigstep.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section
 abbrev Variable := String
 
 def State := Variable → Nat
diff --git a/tests/lean/run/grind_bintree.lean b/tests/lean/run/grind_bintree.lean
index 147f645ca0..8d192a8cb3 100644
--- a/tests/lean/run/grind_bintree.lean
+++ b/tests/lean/run/grind_bintree.lean
@@ -1,5 +1,6 @@
+module
 reset_grind_attrs%
-
+public section -- TODO: workaround for private declaration + dot-notation issue
 attribute [grind] List.append_assoc List.cons_append List.nil_append
 
 inductive Tree (β : Type v) where
diff --git a/tests/lean/run/grind_bitvec.lean b/tests/lean/run/grind_bitvec.lean
index 31d50d677c..f219e84284 100644
--- a/tests/lean/run/grind_bitvec.lean
+++ b/tests/lean/run/grind_bitvec.lean
@@ -1,3 +1,4 @@
+module
 open BitVec
 
 example (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
diff --git a/tests/lean/run/grind_bitvec2.lean b/tests/lean/run/grind_bitvec2.lean
index 202f3e97c9..78aa65b7b4 100644
--- a/tests/lean/run/grind_bitvec2.lean
+++ b/tests/lean/run/grind_bitvec2.lean
@@ -1,3 +1,4 @@
+module
 set_option linter.unusedSimpArgs false
 
 open BitVec
diff --git a/tests/lean/run/grind_bool_diseq.lean b/tests/lean/run/grind_bool_diseq.lean
index 3d52f25c6d..d722a0027b 100644
--- a/tests/lean/run/grind_bool_diseq.lean
+++ b/tests/lean/run/grind_bool_diseq.lean
@@ -1,3 +1,4 @@
+module
 example (f : Bool → Nat) : (x = y ↔ q) → ¬ q → y = false → f x = 0 → f true = 0 := by
   grind (splits := 0)
 
diff --git a/tests/lean/run/grind_bool_prop.lean b/tests/lean/run/grind_bool_prop.lean
index cfc409ad90..1561b6a55c 100644
--- a/tests/lean/run/grind_bool_prop.lean
+++ b/tests/lean/run/grind_bool_prop.lean
@@ -1,3 +1,4 @@
+module
 example (f : Bool → Nat) : f (a && b) = 0 → a = false → f false = 0 := by grind (splits := 0)
 example (f : Bool → Nat) : f (a && b) = 0 → b = false → f false = 0 := by grind (splits := 0)
 example (f : Bool → Nat) : f (a && b) = 0 → a = true → f b = 0 := by grind (splits := 0)
diff --git a/tests/lean/run/grind_canon_bug.lean b/tests/lean/run/grind_canon_bug.lean
index 1605f7a892..9817146c20 100644
--- a/tests/lean/run/grind_canon_bug.lean
+++ b/tests/lean/run/grind_canon_bug.lean
@@ -1,3 +1,4 @@
+module
 open List
 
 attribute [grind =] getElem_cons_zero
diff --git a/tests/lean/run/grind_canon_insts.lean b/tests/lean/run/grind_canon_insts.lean
index 4e7892e275..58ccebb3ea 100644
--- a/tests/lean/run/grind_canon_insts.lean
+++ b/tests/lean/run/grind_canon_insts.lean
@@ -1,5 +1,6 @@
-import Lean.Meta.Tactic.Grind
-
+module
+public import Lean.Meta.Tactic.Grind
+public section
 set_option grind.debug true
 
 class Semigroup (α : Type u) extends Mul α where
diff --git a/tests/lean/run/grind_canon_types.lean b/tests/lean/run/grind_canon_types.lean
index cf47bd5746..5a40ff9662 100644
--- a/tests/lean/run/grind_canon_types.lean
+++ b/tests/lean/run/grind_canon_types.lean
@@ -1,3 +1,4 @@
+module
 import Lean.Meta.Tactic.Grind
 
 def g (s : Type) := s
diff --git a/tests/lean/run/grind_cases.lean b/tests/lean/run/grind_cases.lean
index b8b8ec41d3..ef2a317f7f 100644
--- a/tests/lean/run/grind_cases.lean
+++ b/tests/lean/run/grind_cases.lean
@@ -1,3 +1,4 @@
+module
 /--
 error: invalid `[grind cases eager]`, `List` is not a non-recursive inductive datatype or an alias for one
 -/
diff --git a/tests/lean/run/grind_cases_tac.lean b/tests/lean/run/grind_cases_tac.lean
index f67878336e..8ffdf11caf 100644
--- a/tests/lean/run/grind_cases_tac.lean
+++ b/tests/lean/run/grind_cases_tac.lean
@@ -1,4 +1,6 @@
-import Lean
+module
+public import Lean
+public meta import Lean.Elab.Tactic
 
 open Lean Meta Grind Elab Tactic in
 elab "cases' " e:term : tactic => withMainContext do
diff --git a/tests/lean/run/grind_casting_issue.lean b/tests/lean/run/grind_casting_issue.lean
index fb659fa7ab..f9b38de41d 100644
--- a/tests/lean/run/grind_casting_issue.lean
+++ b/tests/lean/run/grind_casting_issue.lean
@@ -1,3 +1,4 @@
+module
 
 @[grind] def codelen (c: List Bool) : Int := c.length
 
diff --git a/tests/lean/run/grind_cat.lean b/tests/lean/run/grind_cat.lean
index 053f1b0a4f..984d1592b0 100644
--- a/tests/lean/run/grind_cat.lean
+++ b/tests/lean/run/grind_cat.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
 namespace CategoryTheory
diff --git a/tests/lean/run/grind_cat2.lean b/tests/lean/run/grind_cat2.lean
index 4764043813..49df86ec1f 100644
--- a/tests/lean/run/grind_cat2.lean
+++ b/tests/lean/run/grind_cat2.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section
 -- import Lean.Meta.Tactic.Grind
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 
diff --git a/tests/lean/run/grind_clear_error.lean b/tests/lean/run/grind_clear_error.lean
index f9aa723fdc..97ac049d09 100644
--- a/tests/lean/run/grind_clear_error.lean
+++ b/tests/lean/run/grind_clear_error.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 attribute [grind] List.not_mem_nil
 
diff --git a/tests/lean/run/grind_congr.lean b/tests/lean/run/grind_congr.lean
index f8632f09f3..60f5694d1e 100644
--- a/tests/lean/run/grind_congr.lean
+++ b/tests/lean/run/grind_congr.lean
@@ -1,3 +1,4 @@
+module
 import Lean
 def f (a : Nat) := a + a + a
 def g (a : Nat) := a + a
diff --git a/tests/lean/run/grind_congr1.lean b/tests/lean/run/grind_congr1.lean
index dd8d621bd4..350668816d 100644
--- a/tests/lean/run/grind_congr1.lean
+++ b/tests/lean/run/grind_congr1.lean
@@ -1,3 +1,4 @@
+module
 set_option warningAsError false
 set_option grind.debug true
 set_option grind.debug.proofs true
diff --git a/tests/lean/run/grind_congr_hash_issue.lean b/tests/lean/run/grind_congr_hash_issue.lean
index 0df83aa752..9ef45b1024 100644
--- a/tests/lean/run/grind_congr_hash_issue.lean
+++ b/tests/lean/run/grind_congr_hash_issue.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 
 opaque f : Nat → Nat
diff --git a/tests/lean/run/grind_congr_over_applied.lean b/tests/lean/run/grind_congr_over_applied.lean
index 43ca252949..272dbf2eae 100644
--- a/tests/lean/run/grind_congr_over_applied.lean
+++ b/tests/lean/run/grind_congr_over_applied.lean
@@ -1,3 +1,4 @@
+module
 example {g : (Int → Bool) → Int → Bool} {f : Int → Bool} {a b : Int} (hab : a = b) :
     Nat.repeat g 1 f a = Nat.repeat g 1 f b := by
   grind
diff --git a/tests/lean/run/grind_constProp.lean b/tests/lean/run/grind_constProp.lean
index ed10d48914..7751805a27 100644
--- a/tests/lean/run/grind_constProp.lean
+++ b/tests/lean/run/grind_constProp.lean
@@ -1,4 +1,6 @@
+module
 reset_grind_attrs%
+@[expose] public section -- TODO: remove after we fix congr_eq
 
 attribute [grind cases] Or
 attribute [grind =] List.length_nil List.length_cons Option.getD
diff --git a/tests/lean/run/grind_const_pattern.lean b/tests/lean/run/grind_const_pattern.lean
index 263496f97d..3a82d77ba5 100644
--- a/tests/lean/run/grind_const_pattern.lean
+++ b/tests/lean/run/grind_const_pattern.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 attribute [grind] List.map_append
diff --git a/tests/lean/run/grind_countP.lean b/tests/lean/run/grind_countP.lean
index 4456e89c41..052341999e 100644
--- a/tests/lean/run/grind_countP.lean
+++ b/tests/lean/run/grind_countP.lean
@@ -1,3 +1,4 @@
+module
 variable {α : Type u} {l : List α} {P Q : α → Bool}
 
 attribute [grind] List.countP_nil List.countP_cons
diff --git a/tests/lean/run/grind_ctor_ematch.lean b/tests/lean/run/grind_ctor_ematch.lean
index 880def6887..7243993efa 100644
--- a/tests/lean/run/grind_ctor_ematch.lean
+++ b/tests/lean/run/grind_ctor_ematch.lean
@@ -1,3 +1,4 @@
+module
 inductive Even : Nat → Prop
   | zero : Even 0
   | plus_two {n} : Even n → Even (n + 2)
diff --git a/tests/lean/run/grind_cutsat_auto.lean b/tests/lean/run/grind_cutsat_auto.lean
index d35e12eb11..b8e7039c29 100644
--- a/tests/lean/run/grind_cutsat_auto.lean
+++ b/tests/lean/run/grind_cutsat_auto.lean
@@ -1,3 +1,4 @@
+module
 example : ∀ x : Int, x > 7 → 2 * x > 14 := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_commring.lean b/tests/lean/run/grind_cutsat_commring.lean
index c86a3471cb..c0fe76be07 100644
--- a/tests/lean/run/grind_cutsat_commring.lean
+++ b/tests/lean/run/grind_cutsat_commring.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 
 variable [CommRing R] [LE R] [LT R] [LinearOrder R] [OrderedRing R]
diff --git a/tests/lean/run/grind_cutsat_cooper.lean b/tests/lean/run/grind_cutsat_cooper.lean
index 08de177a3b..9a5a52a522 100644
--- a/tests/lean/run/grind_cutsat_cooper.lean
+++ b/tests/lean/run/grind_cutsat_cooper.lean
@@ -1,3 +1,4 @@
+module
 
 example (x y : Int) :
     27 ≤ 11*x + 13*y →
diff --git a/tests/lean/run/grind_cutsat_decompose.lean b/tests/lean/run/grind_cutsat_decompose.lean
index 4c9482561a..2f892ce3c5 100644
--- a/tests/lean/run/grind_cutsat_decompose.lean
+++ b/tests/lean/run/grind_cutsat_decompose.lean
@@ -1,2 +1,3 @@
+module
 example (n : Int) : n = 1000 * (n / 1000) + 100 * ((n / 100) % 10) + 10 * ((n / 10) % 10) + n % 10 := by
   grind
diff --git a/tests/lean/run/grind_cutsat_diseq_1.lean b/tests/lean/run/grind_cutsat_diseq_1.lean
index dc172723df..ac86d1ef73 100644
--- a/tests/lean/run/grind_cutsat_diseq_1.lean
+++ b/tests/lean/run/grind_cutsat_diseq_1.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_diseq_2.lean b/tests/lean/run/grind_cutsat_diseq_2.lean
index bf61106b5c..4eba490042 100644
--- a/tests/lean/run/grind_cutsat_diseq_2.lean
+++ b/tests/lean/run/grind_cutsat_diseq_2.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_diseq_3.lean b/tests/lean/run/grind_cutsat_diseq_3.lean
index 66302dd557..bac1802d2a 100644
--- a/tests/lean/run/grind_cutsat_diseq_3.lean
+++ b/tests/lean/run/grind_cutsat_diseq_3.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_diseq_cooper.lean b/tests/lean/run/grind_cutsat_diseq_cooper.lean
index 40a38f90ad..d77f504e43 100644
--- a/tests/lean/run/grind_cutsat_diseq_cooper.lean
+++ b/tests/lean/run/grind_cutsat_diseq_cooper.lean
@@ -1,3 +1,4 @@
+module
 theorem ex1 (x : Int) : 10 ≤ x → x ≤ 20 → x ≠ 11 → 11 ∣ x → False := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_div_1.lean b/tests/lean/run/grind_cutsat_div_1.lean
index 5cad76a446..d92cb313a5 100644
--- a/tests/lean/run/grind_cutsat_div_1.lean
+++ b/tests/lean/run/grind_cutsat_div_1.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 set_option pp.structureInstances false
 open Int.Linear
diff --git a/tests/lean/run/grind_cutsat_div_mod.lean b/tests/lean/run/grind_cutsat_div_mod.lean
index e622a38d31..9e2e88724e 100644
--- a/tests/lean/run/grind_cutsat_div_mod.lean
+++ b/tests/lean/run/grind_cutsat_div_mod.lean
@@ -1,3 +1,4 @@
+module
 example (x y : Int) : x / 2 + y = 3 → x = 5 → y = 1 := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_eq_1.lean b/tests/lean/run/grind_cutsat_eq_1.lean
index f8c405329c..d3663fb49c 100644
--- a/tests/lean/run/grind_cutsat_eq_1.lean
+++ b/tests/lean/run/grind_cutsat_eq_1.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_instances.lean b/tests/lean/run/grind_cutsat_instances.lean
index c6aa1dd817..08d451e621 100644
--- a/tests/lean/run/grind_cutsat_instances.lean
+++ b/tests/lean/run/grind_cutsat_instances.lean
@@ -1,3 +1,4 @@
+module
 class Distrib (R : Type _) extends Mul R where
 
 namespace Nat
diff --git a/tests/lean/run/grind_cutsat_le_1.lean b/tests/lean/run/grind_cutsat_le_1.lean
index 16506e823a..87998db74b 100644
--- a/tests/lean/run/grind_cutsat_le_1.lean
+++ b/tests/lean/run/grind_cutsat_le_1.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 
 /--
diff --git a/tests/lean/run/grind_cutsat_le_2.lean b/tests/lean/run/grind_cutsat_le_2.lean
index db17883866..cd8a91b555 100644
--- a/tests/lean/run/grind_cutsat_le_2.lean
+++ b/tests/lean/run/grind_cutsat_le_2.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_natCast_propagation.lean b/tests/lean/run/grind_cutsat_natCast_propagation.lean
index 4a2cf283c8..3b2415779f 100644
--- a/tests/lean/run/grind_cutsat_natCast_propagation.lean
+++ b/tests/lean/run/grind_cutsat_natCast_propagation.lean
@@ -1,3 +1,4 @@
+module
 example (a b : Nat) : a  = a + b - b := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_nat_dvd.lean b/tests/lean/run/grind_cutsat_nat_dvd.lean
index 11fcd3041f..b498a41fe3 100644
--- a/tests/lean/run/grind_cutsat_nat_dvd.lean
+++ b/tests/lean/run/grind_cutsat_nat_dvd.lean
@@ -1,3 +1,4 @@
+module
 theorem ex₁ (a : Nat) (h₁ : 2 ∣ a) (h₂ : 2 ∣ a + 1) : False := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_nat_eq.lean b/tests/lean/run/grind_cutsat_nat_eq.lean
index e999f2fe06..6fc2eecb50 100644
--- a/tests/lean/run/grind_cutsat_nat_eq.lean
+++ b/tests/lean/run/grind_cutsat_nat_eq.lean
@@ -1,3 +1,4 @@
+module
 example (a b c : Nat) : a = 0 → b = 0 → c ≥ a + b := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_nat_le.lean b/tests/lean/run/grind_cutsat_nat_le.lean
index 44a742d229..5acac4b496 100644
--- a/tests/lean/run/grind_cutsat_nat_le.lean
+++ b/tests/lean/run/grind_cutsat_nat_le.lean
@@ -1,3 +1,4 @@
+module
 
 open Int.Linear
 
diff --git a/tests/lean/run/grind_cutsat_omega.lean b/tests/lean/run/grind_cutsat_omega.lean
index 791e0ac66b..ec0ad46dc2 100644
--- a/tests/lean/run/grind_cutsat_omega.lean
+++ b/tests/lean/run/grind_cutsat_omega.lean
@@ -1,3 +1,4 @@
+module
 example (_ : (1 : Int) < (0 : Int)) : False := by grind
 example (_ : (0 : Int) < (0 : Int)) : False := by grind
 example (_ : (0 : Int) < (1 : Int)) : True := by grind
diff --git a/tests/lean/run/grind_cutsat_tests.lean b/tests/lean/run/grind_cutsat_tests.lean
index 678415ed32..1a33f77f03 100644
--- a/tests/lean/run/grind_cutsat_tests.lean
+++ b/tests/lean/run/grind_cutsat_tests.lean
@@ -1,3 +1,4 @@
+module
 example (w x y z : Int) :
   2*w + 3*x - 4*y + z = 10 →
   w - x + 2*y - 3*z = 5 →
diff --git a/tests/lean/run/grind_cutsat_toint_1.lean b/tests/lean/run/grind_cutsat_toint_1.lean
index 6d982d83ea..16390e356b 100644
--- a/tests/lean/run/grind_cutsat_toint_1.lean
+++ b/tests/lean/run/grind_cutsat_toint_1.lean
@@ -1,3 +1,4 @@
+module
 example (a b c : Fin 11) : a ≤ b → b ≤ c → a ≤ c := by
   grind
 
diff --git a/tests/lean/run/grind_cutsat_trim_context.lean b/tests/lean/run/grind_cutsat_trim_context.lean
index f10972fbb1..529be85f96 100644
--- a/tests/lean/run/grind_cutsat_trim_context.lean
+++ b/tests/lean/run/grind_cutsat_trim_context.lean
@@ -1,3 +1,4 @@
+module
 /--
 trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 =>
       let ctx := RArray.leaf (f 2);
diff --git a/tests/lean/run/grind_cutsat_upper_bug.lean b/tests/lean/run/grind_cutsat_upper_bug.lean
index 98c9c46c5a..0d03335313 100644
--- a/tests/lean/run/grind_cutsat_upper_bug.lean
+++ b/tests/lean/run/grind_cutsat_upper_bug.lean
@@ -1,3 +1,4 @@
+module
 /-- trace: [grind.cutsat.model] a := 2 -/
 #guard_msgs (trace) in
 set_option trace.grind.cutsat.model true in
diff --git a/tests/lean/run/grind_cutsat_zero.lean b/tests/lean/run/grind_cutsat_zero.lean
index 45d60bf832..b4b295e884 100644
--- a/tests/lean/run/grind_cutsat_zero.lean
+++ b/tests/lean/run/grind_cutsat_zero.lean
@@ -1 +1,2 @@
+module
 example (hy : y = 0) (hz : z = 0) : 0 = y + z := by grind
diff --git a/tests/lean/run/grind_decide_bool_issues.lean b/tests/lean/run/grind_decide_bool_issues.lean
index 642b7062ef..86112bb232 100644
--- a/tests/lean/run/grind_decide_bool_issues.lean
+++ b/tests/lean/run/grind_decide_bool_issues.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 example {P Q : Prop} [Decidable P] [Decidable Q] : (decide P || decide Q) = decide (P ∨ Q) := by grind
diff --git a/tests/lean/run/grind_dep_match_overlap.lean b/tests/lean/run/grind_dep_match_overlap.lean
index 9bc880e4c2..4b6e7559a7 100644
--- a/tests/lean/run/grind_dep_match_overlap.lean
+++ b/tests/lean/run/grind_dep_match_overlap.lean
@@ -1,7 +1,10 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
 inductive Vec (α : Type u) : Nat → Type u
   | nil : Vec α 0
   | cons : α → Vec α n → Vec α (n+1)
 
+-- The `grind` tactics fail without this `[expose]`
 def h (v w : Vec α n) : Nat :=
   match v, w with
   | _, .cons _ (.cons _ _) => 20
diff --git a/tests/lean/run/grind_diseq.lean b/tests/lean/run/grind_diseq.lean
index 724272154e..fb3a9d3416 100644
--- a/tests/lean/run/grind_diseq.lean
+++ b/tests/lean/run/grind_diseq.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 
 example (p q : Prop) (a b c d : Nat) :
diff --git a/tests/lean/run/grind_diseq_api.lean b/tests/lean/run/grind_diseq_api.lean
index a7bc7a52f7..9d5f037f9c 100644
--- a/tests/lean/run/grind_diseq_api.lean
+++ b/tests/lean/run/grind_diseq_api.lean
@@ -1,3 +1,4 @@
+module
 import Lean
 
 opaque a : Nat
diff --git a/tests/lean/run/grind_dvd_propagate_issue.lean b/tests/lean/run/grind_dvd_propagate_issue.lean
index 017418d1fd..09b0469ba4 100644
--- a/tests/lean/run/grind_dvd_propagate_issue.lean
+++ b/tests/lean/run/grind_dvd_propagate_issue.lean
@@ -1,3 +1,4 @@
+module
 open List
 
 
diff --git a/tests/lean/run/grind_ematch1.lean b/tests/lean/run/grind_ematch1.lean
index 330ae1c13d..a1696f9299 100644
--- a/tests/lean/run/grind_ematch1.lean
+++ b/tests/lean/run/grind_ematch1.lean
@@ -1,5 +1,6 @@
+module
 reset_grind_attrs%
-
+public section
 set_option trace.grind.ematch.pattern true
 
 attribute [grind =] Array.size_set
diff --git a/tests/lean/run/grind_ematch2.lean b/tests/lean/run/grind_ematch2.lean
index 097ce62a43..f9a8445c9b 100644
--- a/tests/lean/run/grind_ematch2.lean
+++ b/tests/lean/run/grind_ematch2.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 attribute [grind =] Array.size_set Array.getElem_set_self Array.getElem_set_ne
diff --git a/tests/lean/run/grind_ematch_gen_pattern.lean b/tests/lean/run/grind_ematch_gen_pattern.lean
index c91aed924c..b55111de50 100644
--- a/tests/lean/run/grind_ematch_gen_pattern.lean
+++ b/tests/lean/run/grind_ematch_gen_pattern.lean
@@ -1,3 +1,4 @@
+module
 def f (x : Option Nat) (h : x ≠ none) : Nat :=
   match x with
   | none => by contradiction
diff --git a/tests/lean/run/grind_ematch_ground_implicit_inst.lean b/tests/lean/run/grind_ematch_ground_implicit_inst.lean
index 86f8ee67d2..7b7f1987fb 100644
--- a/tests/lean/run/grind_ematch_ground_implicit_inst.lean
+++ b/tests/lean/run/grind_ematch_ground_implicit_inst.lean
@@ -1,3 +1,4 @@
+module
 example (a : Nat) : max a a = a := by
   grind
 
diff --git a/tests/lean/run/grind_ematch_patterns.lean b/tests/lean/run/grind_ematch_patterns.lean
index 0cb8b319bf..291ccf7ee3 100644
--- a/tests/lean/run/grind_ematch_patterns.lean
+++ b/tests/lean/run/grind_ematch_patterns.lean
@@ -1,3 +1,5 @@
+module
+public section -- TODO: Fix error messages with private names.
 def replicate : (n : Nat) → (a : α) → List α
   | 0,   _ => []
   | n+1, a => a :: replicate n a
diff --git a/tests/lean/run/grind_ematch_theorem_activation.lean b/tests/lean/run/grind_ematch_theorem_activation.lean
index 6132458569..8a6836f4c3 100644
--- a/tests/lean/run/grind_ematch_theorem_activation.lean
+++ b/tests/lean/run/grind_ematch_theorem_activation.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 attribute [grind] List.length_set
 attribute [grind →] List.eq_nil_of_length_eq_zero
diff --git a/tests/lean/run/grind_ematch_type_error.lean b/tests/lean/run/grind_ematch_type_error.lean
index 2990fe3e1b..c8f21c6798 100644
--- a/tests/lean/run/grind_ematch_type_error.lean
+++ b/tests/lean/run/grind_ematch_type_error.lean
@@ -1,3 +1,4 @@
+module
 example (xs : Array Nat) (w : xs.reverse = xs) (j : Nat) (hj : 0 ≤ j) (hj' : j < xs.size / 2) :
     xs[j] = xs[xs.size - 1 - j] := by
   grind
diff --git a/tests/lean/run/grind_eq.lean b/tests/lean/run/grind_eq.lean
index 115f818a40..5e39fbd018 100644
--- a/tests/lean/run/grind_eq.lean
+++ b/tests/lean/run/grind_eq.lean
@@ -1,3 +1,4 @@
+module
 opaque g : Nat → Nat
 
 set_option trace.Meta.debug true
diff --git a/tests/lean/run/grind_eq_bwd.lean b/tests/lean/run/grind_eq_bwd.lean
index 9d4890f105..180de6e1f0 100644
--- a/tests/lean/run/grind_eq_bwd.lean
+++ b/tests/lean/run/grind_eq_bwd.lean
@@ -1,3 +1,4 @@
+module
 theorem dummy (x : Nat) : x = x :=
   rfl
 
diff --git a/tests/lean/run/grind_eq_bwd_pat_bug.lean b/tests/lean/run/grind_eq_bwd_pat_bug.lean
index 53560ea5c5..9785c506ac 100644
--- a/tests/lean/run/grind_eq_bwd_pat_bug.lean
+++ b/tests/lean/run/grind_eq_bwd_pat_bug.lean
@@ -1,3 +1,4 @@
+module
 @[grind ←=] theorem inv_eq {α : Type} [One α] [Mul α] [Inv α] {a b : α} (w : a * b = 1) : a⁻¹ = b := sorry
 
 theorem test {α : Type} [One α] [Mul α] [Inv α] {a b : α} (w : a * b = 1) : a⁻¹ = b := by
diff --git a/tests/lean/run/grind_eq_false_of_imp_eq_false.lean b/tests/lean/run/grind_eq_false_of_imp_eq_false.lean
index ef30c4df99..fa41dac6ac 100644
--- a/tests/lean/run/grind_eq_false_of_imp_eq_false.lean
+++ b/tests/lean/run/grind_eq_false_of_imp_eq_false.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 open List
 
diff --git a/tests/lean/run/grind_eq_pattern.lean b/tests/lean/run/grind_eq_pattern.lean
index f4da2c60a0..e8fa633f62 100644
--- a/tests/lean/run/grind_eq_pattern.lean
+++ b/tests/lean/run/grind_eq_pattern.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 /--
diff --git a/tests/lean/run/grind_eqres_bug.lean b/tests/lean/run/grind_eqres_bug.lean
index b64a066dc5..0a6c0ef9d9 100644
--- a/tests/lean/run/grind_eqres_bug.lean
+++ b/tests/lean/run/grind_eqres_bug.lean
@@ -1,3 +1,4 @@
+module
 /--
 trace: [grind.eqResolution] ∀ (x : Nat), p x a → ∀ (y : Nat), p y b → ¬x = y, ∀ (y : Nat), p y a → p y b → False
 [grind.ematch.instance] local_0: p c a → ¬p c b
diff --git a/tests/lean/run/grind_erase_attr.lean b/tests/lean/run/grind_erase_attr.lean
index 13d03834e4..df812b3138 100644
--- a/tests/lean/run/grind_erase_attr.lean
+++ b/tests/lean/run/grind_erase_attr.lean
@@ -1,3 +1,5 @@
+module
+public section
 opaque f : Nat → Nat
 
 @[grind] theorem fthm : f (f x) = f x := sorry
diff --git a/tests/lean/run/grind_eta.lean b/tests/lean/run/grind_eta.lean
index 5b8443f9ce..6425054769 100644
--- a/tests/lean/run/grind_eta.lean
+++ b/tests/lean/run/grind_eta.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 example {l : List α} {f : β → α → β} {b : β} :
     l.foldl f b = l.reverse.foldr (fun x y => f y x) b := by
diff --git a/tests/lean/run/grind_etaStruct.lean b/tests/lean/run/grind_etaStruct.lean
index 356fd5e60e..bc3d9f4d96 100644
--- a/tests/lean/run/grind_etaStruct.lean
+++ b/tests/lean/run/grind_etaStruct.lean
@@ -1,3 +1,4 @@
+module
 opaque f (a : Nat) : Nat × Bool
 
 example (a b : Nat) : (f a).1 = (f b).1 → (f a).2 = (f b).2 → f a = f b := by
diff --git a/tests/lean/run/grind_eval_suggest.lean b/tests/lean/run/grind_eval_suggest.lean
index 15668558a4..dc953fab63 100644
--- a/tests/lean/run/grind_eval_suggest.lean
+++ b/tests/lean/run/grind_eval_suggest.lean
@@ -1,5 +1,7 @@
-import Lean.Elab.Tactic.Try
-import Std.Tactic.BVDecide
+module
+public meta import Lean.Elab.Tactic
+public import Lean.Elab.Tactic.Try
+public import Std.Tactic.BVDecide
 
 open Lean Elab Tactic Try
 elab tk:"eval_suggest" tac:tactic : tactic => do
diff --git a/tests/lean/run/grind_exfalso.lean b/tests/lean/run/grind_exfalso.lean
index cb82241e84..1e0065e404 100644
--- a/tests/lean/run/grind_exfalso.lean
+++ b/tests/lean/run/grind_exfalso.lean
@@ -1,3 +1,4 @@
+module
 example (x : Nat) (h : x < 0) : Nat → Nat := by
   grind
 
diff --git a/tests/lean/run/grind_fastEraseDups.lean b/tests/lean/run/grind_fastEraseDups.lean
index b27a3a331f..be0324a51b 100644
--- a/tests/lean/run/grind_fastEraseDups.lean
+++ b/tests/lean/run/grind_fastEraseDups.lean
@@ -1,3 +1,4 @@
+module
 
 import Std.Data.HashSet
 
diff --git a/tests/lean/run/grind_field_div.lean b/tests/lean/run/grind_field_div.lean
index 5d2ba62e1d..cb25104f2a 100644
--- a/tests/lean/run/grind_field_div.lean
+++ b/tests/lean/run/grind_field_div.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 set_option grind.debug true
 
diff --git a/tests/lean/run/grind_field_norm.lean b/tests/lean/run/grind_field_norm.lean
index 4a8674613c..763ceda733 100644
--- a/tests/lean/run/grind_field_norm.lean
+++ b/tests/lean/run/grind_field_norm.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 set_option grind.debug true
 
diff --git a/tests/lean/run/grind_field_norm_2.lean b/tests/lean/run/grind_field_norm_2.lean
index a917cb202c..f2c4db9f55 100644
--- a/tests/lean/run/grind_field_norm_2.lean
+++ b/tests/lean/run/grind_field_norm_2.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 
 variable (R : Type u) [Field R]
diff --git a/tests/lean/run/grind_finVal.lean b/tests/lean/run/grind_finVal.lean
index 8703cb7084..7d33691a15 100644
--- a/tests/lean/run/grind_finVal.lean
+++ b/tests/lean/run/grind_finVal.lean
@@ -1,3 +1,4 @@
+module
 example (a b : Fin 2) (n : Nat) : n = 1 → ↑(a + b) ≠ n → a ≠ 0 → b = 0 → False := by
   grind -ring
 
diff --git a/tests/lean/run/grind_fun_singleton.lean b/tests/lean/run/grind_fun_singleton.lean
index 6aa79d6ef3..883143a280 100644
--- a/tests/lean/run/grind_fun_singleton.lean
+++ b/tests/lean/run/grind_fun_singleton.lean
@@ -1,3 +1,4 @@
+module
 example (h : (fun (_ : Unit) => x = 1) = (fun _ => True)) : x = 1 := by
   grind
 
diff --git a/tests/lean/run/grind_funext.lean b/tests/lean/run/grind_funext.lean
index 58819569b7..10b8b4335e 100644
--- a/tests/lean/run/grind_funext.lean
+++ b/tests/lean/run/grind_funext.lean
@@ -1,3 +1,4 @@
+module
 example (f : (Nat → Nat) → Nat → Nat → Nat) : a = b → f (fun x => a + x) 1 b = f (fun x => b + x) 1 a := by
   grind
 
diff --git a/tests/lean/run/grind_getElem.lean b/tests/lean/run/grind_getElem.lean
index 84f1d676d0..9c7153c30d 100644
--- a/tests/lean/run/grind_getElem.lean
+++ b/tests/lean/run/grind_getElem.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 attribute [grind]
diff --git a/tests/lean/run/grind_getLast_dropLast.lean b/tests/lean/run/grind_getLast_dropLast.lean
index e01620e5b5..dd1fd344ff 100644
--- a/tests/lean/run/grind_getLast_dropLast.lean
+++ b/tests/lean/run/grind_getLast_dropLast.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 open List
 
diff --git a/tests/lean/run/grind_guide.lean b/tests/lean/run/grind_guide.lean
index d396fd72e2..ccc9438685 100644
--- a/tests/lean/run/grind_guide.lean
+++ b/tests/lean/run/grind_guide.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
 /-
 `grind` is inspired by automated reasoning techniques developed in the world of Satisfiability Modulo Theories (SMT).
 
diff --git a/tests/lean/run/grind_hashmap_list.lean b/tests/lean/run/grind_hashmap_list.lean
index ca9c3ef29a..b22cbed32c 100644
--- a/tests/lean/run/grind_hashmap_list.lean
+++ b/tests/lean/run/grind_hashmap_list.lean
@@ -1,3 +1,4 @@
+module
 import Std.Data.HashMap
 reset_grind_attrs%
 
diff --git a/tests/lean/run/grind_hcongr.lean b/tests/lean/run/grind_hcongr.lean
index a451d5d178..94dcca22d0 100644
--- a/tests/lean/run/grind_hcongr.lean
+++ b/tests/lean/run/grind_hcongr.lean
@@ -1,3 +1,4 @@
+module
 def Matrix (m : Type) (n : Type) (α : Type) : Type :=
   m → n → α
 
diff --git a/tests/lean/run/grind_heapsort.lean b/tests/lean/run/grind_heapsort.lean
index be1d0dc67e..60561003dc 100644
--- a/tests/lean/run/grind_heapsort.lean
+++ b/tests/lean/run/grind_heapsort.lean
@@ -1,3 +1,4 @@
+module
 import Lean
 /-
 Use `grind` as one of the tactics for array-element access and termination proofs.
diff --git a/tests/lean/run/grind_heartbeats.lean b/tests/lean/run/grind_heartbeats.lean
index 2245808287..e4a86ede3c 100644
--- a/tests/lean/run/grind_heartbeats.lean
+++ b/tests/lean/run/grind_heartbeats.lean
@@ -1,3 +1,4 @@
+module
 opaque f : Nat → Nat
 opaque op : Nat → Nat → Nat
 @[grind] theorem op_comm : op x y = op y x := sorry
diff --git a/tests/lean/run/grind_heq_proof_issue.lean b/tests/lean/run/grind_heq_proof_issue.lean
index 1c16050d7f..7c3b5c2ea1 100644
--- a/tests/lean/run/grind_heq_proof_issue.lean
+++ b/tests/lean/run/grind_heq_proof_issue.lean
@@ -1,3 +1,4 @@
+module
 def f (a : α) := a
 
 example (a b : α) (x y : β) : a ≍ x → x = y → y ≍ b → f a = f b := by
diff --git a/tests/lean/run/grind_hyper_ex.lean b/tests/lean/run/grind_hyper_ex.lean
index 9398f5a68c..333677dcf5 100644
--- a/tests/lean/run/grind_hyper_ex.lean
+++ b/tests/lean/run/grind_hyper_ex.lean
@@ -1,3 +1,4 @@
+module
 abbrev ℕ :=  Nat
 
 def hyperoperation : ℕ → ℕ → ℕ → ℕ
diff --git a/tests/lean/run/grind_ignore_impl_detail.lean b/tests/lean/run/grind_ignore_impl_detail.lean
index 0b8b56bb60..ce4a27533e 100644
--- a/tests/lean/run/grind_ignore_impl_detail.lean
+++ b/tests/lean/run/grind_ignore_impl_detail.lean
@@ -1,3 +1,4 @@
+module
 example {p q : Prop} : True := by
   have (__x : p ∧ q) : p := by
     fail_if_success grind -- should fail because `__x` is an implementation detail, and `grind` ignores them.
diff --git a/tests/lean/run/grind_implies.lean b/tests/lean/run/grind_implies.lean
index 353dfe8015..2bce3c6250 100644
--- a/tests/lean/run/grind_implies.lean
+++ b/tests/lean/run/grind_implies.lean
@@ -1,3 +1,4 @@
+module
 set_option trace.grind.eqc true
 set_option trace.grind.internalize true
 
diff --git a/tests/lean/run/grind_indexmap.lean b/tests/lean/run/grind_indexmap.lean
index 4855c3ea94..9d190dcfe0 100644
--- a/tests/lean/run/grind_indexmap.lean
+++ b/tests/lean/run/grind_indexmap.lean
@@ -1,9 +1,9 @@
 -- See also the companion file `grind_indexmap_pre.lean`,
 -- showing this file might have looked like before any proofs are written.
 -- This file fills them all in with `grind`!
-
 import Std.Data.HashMap
 
+
 macro_rules | `(tactic| get_elem_tactic_extensible) => `(tactic| grind)
 
 open Std
diff --git a/tests/lean/run/grind_indexmap_pre.lean b/tests/lean/run/grind_indexmap_pre.lean
index 0a6acea2d1..fda89f2f7d 100644
--- a/tests/lean/run/grind_indexmap_pre.lean
+++ b/tests/lean/run/grind_indexmap_pre.lean
@@ -1,3 +1,4 @@
+module
 -- This is a companion file for `grind_indexmap.lean`,
 -- showing what an outline of this file might look like before any proofs are written.
 
diff --git a/tests/lean/run/grind_issue_9125.lean b/tests/lean/run/grind_issue_9125.lean
index 57b6cc3e0b..3bd8c92bd0 100644
--- a/tests/lean/run/grind_issue_9125.lean
+++ b/tests/lean/run/grind_issue_9125.lean
@@ -1,3 +1,4 @@
+module
 variable {R : Type} [Lean.Grind.CommRing R]
 -- My real code uses CommRing from Mathlib instead, and sees the same behavior.
 
diff --git a/tests/lean/run/grind_issue_9187.lean b/tests/lean/run/grind_issue_9187.lean
index aa7923bc15..9365254bc6 100644
--- a/tests/lean/run/grind_issue_9187.lean
+++ b/tests/lean/run/grind_issue_9187.lean
@@ -1,3 +1,4 @@
+module
 structure Cat (C : Type) where
   hom : C → C → Type
   comp {x y z : C} (f : hom x y) (g : hom y z) : hom x z
diff --git a/tests/lean/run/grind_ite.lean b/tests/lean/run/grind_ite.lean
index 4df23b0402..daba3c5fde 100644
--- a/tests/lean/run/grind_ite.lean
+++ b/tests/lean/run/grind_ite.lean
@@ -1,5 +1,7 @@
-import Std
-
+module
+public import Std.Data.HashMap
+public import Std.Data.TreeMap
+public section -- TODO: Workaround for private declaration issue
 /-!
 # If normalization
 
@@ -124,10 +126,6 @@ we are allowed to increase the size of the branches by one, and still be smaller
   | var _ => 1
   | .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1
 
--- TODO: `grind` canonicalizer is spending a lot of time unfolding the following function.
--- TODO: remove after the new module system will hide this declaration.
-seal Std.DHashMap.insert
-seal Std.TreeMap.insert
 
 def normalize (assign : Std.HashMap Nat Bool) : IfExpr → IfExpr
   | lit b => lit b
diff --git a/tests/lean/run/grind_ite_congr.lean b/tests/lean/run/grind_ite_congr.lean
index b7b9375f6c..ec8f2a60b9 100644
--- a/tests/lean/run/grind_ite_congr.lean
+++ b/tests/lean/run/grind_ite_congr.lean
@@ -1,3 +1,4 @@
+module
 example : ((if true then id else id) false) = false := by
   grind
 
diff --git a/tests/lean/run/grind_ite_split_issue.lean b/tests/lean/run/grind_ite_split_issue.lean
index f8b174a37b..b347b557fd 100644
--- a/tests/lean/run/grind_ite_split_issue.lean
+++ b/tests/lean/run/grind_ite_split_issue.lean
@@ -1,3 +1,4 @@
+module
 example (a b : Int) : min a b = 10 → a ≥ 10 := by
   grind
 
diff --git a/tests/lean/run/grind_ite_unused_match.lean b/tests/lean/run/grind_ite_unused_match.lean
index ec8a905d17..c9c20a141d 100644
--- a/tests/lean/run/grind_ite_unused_match.lean
+++ b/tests/lean/run/grind_ite_unused_match.lean
@@ -1,4 +1,7 @@
-import Std.Data.HashMap.Lemmas
+module
+public import Std.Data.HashMap.Lemmas
+@[expose] public section -- TODO: remove after we fix congr_eq
+
 
 -- This is a variant of the "if normalization" example, acting as a regression test for a now-fixed problem in grind.
 -- It is not a solution to the "if normalization" challenge.
diff --git a/tests/lean/run/grind_lawful_eq_cmp.lean b/tests/lean/run/grind_lawful_eq_cmp.lean
index 9b313ee3d0..f530cdafd3 100644
--- a/tests/lean/run/grind_lawful_eq_cmp.lean
+++ b/tests/lean/run/grind_lawful_eq_cmp.lean
@@ -1,3 +1,4 @@
+module
 import Std
 
 example (f : α → α → Ordering) [Std.LawfulEqCmp f] (a b c : α) : b = c → f a b = o → o = .eq → a = c := by
diff --git a/tests/lean/run/grind_lazy_ite.lean b/tests/lean/run/grind_lazy_ite.lean
index d25eea3da8..7f150c7072 100644
--- a/tests/lean/run/grind_lazy_ite.lean
+++ b/tests/lean/run/grind_lazy_ite.lean
@@ -1,3 +1,4 @@
+module
 def f (n : Nat) (m : Nat) :=
   if n < m then
     f (n+1) m + n
diff --git a/tests/lean/run/grind_lex.lean b/tests/lean/run/grind_lex.lean
index c59fa11d97..00b79ff138 100644
--- a/tests/lean/run/grind_lex.lean
+++ b/tests/lean/run/grind_lex.lean
@@ -1,3 +1,4 @@
+module
 -- From Mathlib.Data.List.Defs
 -- These needed `attribute [grind =] Prod.lex_def`
 
diff --git a/tests/lean/run/grind_linarith_1.lean b/tests/lean/run/grind_linarith_1.lean
index 75480e9aca..2ef9dd9b1a 100644
--- a/tests/lean/run/grind_linarith_1.lean
+++ b/tests/lean/run/grind_linarith_1.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 set_option grind.debug true
 
diff --git a/tests/lean/run/grind_linarith_2.lean b/tests/lean/run/grind_linarith_2.lean
index d3de4a5e26..608c91f9c8 100644
--- a/tests/lean/run/grind_linarith_2.lean
+++ b/tests/lean/run/grind_linarith_2.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 set_option grind.debug true
 
diff --git a/tests/lean/run/grind_linarith_spurious_issues.lean b/tests/lean/run/grind_linarith_spurious_issues.lean
index b50e770b88..617f1de45f 100644
--- a/tests/lean/run/grind_linarith_spurious_issues.lean
+++ b/tests/lean/run/grind_linarith_spurious_issues.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 
 -- Should not produced spurious issues.
diff --git a/tests/lean/run/grind_linarith_trim_context.lean b/tests/lean/run/grind_linarith_trim_context.lean
index 688a801af9..fc7e450a39 100644
--- a/tests/lean/run/grind_linarith_trim_context.lean
+++ b/tests/lean/run/grind_linarith_trim_context.lean
@@ -1,3 +1,4 @@
+module
 /--
 trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 =>
       let ctx := RArray.branch 1 (RArray.leaf One.one) (RArray.leaf (f 2));
diff --git a/tests/lean/run/grind_linearize.lean b/tests/lean/run/grind_linearize.lean
index 14e87814aa..480c632dbd 100644
--- a/tests/lean/run/grind_linearize.lean
+++ b/tests/lean/run/grind_linearize.lean
@@ -1,3 +1,4 @@
+module
 example (x y z w : Int) : z * x * y = 4 → x = z + w → z = 1 → w = 2 → False := by
   grind -ring
 
diff --git a/tests/lean/run/grind_list.lean b/tests/lean/run/grind_list.lean
index 8d6d460063..f36f6fe83a 100644
--- a/tests/lean/run/grind_list.lean
+++ b/tests/lean/run/grind_list.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 namespace List
 
diff --git a/tests/lean/run/grind_list2.lean b/tests/lean/run/grind_list2.lean
index b3c903eaf2..d3d771e3d7 100644
--- a/tests/lean/run/grind_list2.lean
+++ b/tests/lean/run/grind_list2.lean
@@ -1,3 +1,4 @@
+module
 -- Note that `grind_list.lean` uses `reset_grind_attrs%` to clear the grind attributes.
 -- This file does not: it is testing the grind attributes in the library.
 
@@ -9,7 +10,7 @@
 -- This file only contains those theorems that can be proved "effortlessly" with `grind`.
 -- `tests/lean/grind/experiments/list.lean` contains everything from `Data/List/Lemmas.lean`
 -- that still resists `grind`!
-
+@[expose] public section -- TODO: remove after congr_eq has been fixed
 open List Nat
 
 namespace Hidden
diff --git a/tests/lean/run/grind_list_count.lean b/tests/lean/run/grind_list_count.lean
index f50aff706c..c7cdd99702 100644
--- a/tests/lean/run/grind_list_count.lean
+++ b/tests/lean/run/grind_list_count.lean
@@ -1,3 +1,4 @@
+module
 
 open List Nat
 
diff --git a/tests/lean/run/grind_list_drop_take.lean b/tests/lean/run/grind_list_drop_take.lean
index 58cb821e0e..ff0570ca32 100644
--- a/tests/lean/run/grind_list_drop_take.lean
+++ b/tests/lean/run/grind_list_drop_take.lean
@@ -1,3 +1,4 @@
+module
 example : (List.range' 1 n).drop (List.range' 1 n).length = [] := by grind -- solves
 example : [].sum = 0 := by grind -- solves
 example : ((List.range' 1 n).drop (List.range' 1 n).length).sum = 0 := by grind -- solves
diff --git a/tests/lean/run/grind_list_erase.lean b/tests/lean/run/grind_list_erase.lean
index bed9926518..debe14e85c 100644
--- a/tests/lean/run/grind_list_erase.lean
+++ b/tests/lean/run/grind_list_erase.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section -- TODO: remove after `congr_eq` fixed
 open List
 
 theorem eraseP_eq_nil_iff {xs : List α} {p : α → Bool} : xs.eraseP p = [] ↔ xs = [] ∨ ∃ x, p x ∧ xs = [x] := by
diff --git a/tests/lean/run/grind_list_find.lean b/tests/lean/run/grind_list_find.lean
index 731cc2cc48..4342772358 100644
--- a/tests/lean/run/grind_list_find.lean
+++ b/tests/lean/run/grind_list_find.lean
@@ -1,3 +1,4 @@
+module
 open List
 
 theorem findSome?_eq_none_iff : findSome? p l = none ↔ ∀ x ∈ l, p x = none := by
diff --git a/tests/lean/run/grind_list_issue.lean b/tests/lean/run/grind_list_issue.lean
index 1fa8622f2c..aa45eb0dbb 100644
--- a/tests/lean/run/grind_list_issue.lean
+++ b/tests/lean/run/grind_list_issue.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 open List Nat
 
diff --git a/tests/lean/run/grind_list_perm.lean b/tests/lean/run/grind_list_perm.lean
index c4b3f0ccda..733987b9ab 100644
--- a/tests/lean/run/grind_list_perm.lean
+++ b/tests/lean/run/grind_list_perm.lean
@@ -1,3 +1,4 @@
+module
 open List
 
 example : [3,1,4,2] ~ [2,4,1,3] := by grind
diff --git a/tests/lean/run/grind_list_sublist.lean b/tests/lean/run/grind_list_sublist.lean
index e94ea638af..bdaf65b6c4 100644
--- a/tests/lean/run/grind_list_sublist.lean
+++ b/tests/lean/run/grind_list_sublist.lean
@@ -1,3 +1,4 @@
+module
 open List
 
 variable {α} {l₁ l₂ l₃ l₄ l₅ : List α}
diff --git a/tests/lean/run/grind_lookahead.lean b/tests/lean/run/grind_lookahead.lean
index 6883b8e619..b3f200c27d 100644
--- a/tests/lean/run/grind_lookahead.lean
+++ b/tests/lean/run/grind_lookahead.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 attribute [grind] List.eq_nil_of_length_eq_zero
diff --git a/tests/lean/run/grind_many_eqs.lean b/tests/lean/run/grind_many_eqs.lean
index efddd3e5f2..9fbc7ec72e 100644
--- a/tests/lean/run/grind_many_eqs.lean
+++ b/tests/lean/run/grind_many_eqs.lean
@@ -1,3 +1,4 @@
+module
 import Lean.Meta.Tactic.Grind
 
 def f (a : Nat) := a + a + a
diff --git a/tests/lean/run/grind_map.lean b/tests/lean/run/grind_map.lean
index fa2c569af0..38cb85a959 100644
--- a/tests/lean/run/grind_map.lean
+++ b/tests/lean/run/grind_map.lean
@@ -1,3 +1,4 @@
+module
 import Std.Data.HashMap
 import Std.Data.DHashMap
 import Std.Data.ExtHashMap
diff --git a/tests/lean/run/grind_mark_nested_proofs_bug.lean b/tests/lean/run/grind_mark_nested_proofs_bug.lean
index 8a09fbf3a0..098dec01c1 100644
--- a/tests/lean/run/grind_mark_nested_proofs_bug.lean
+++ b/tests/lean/run/grind_mark_nested_proofs_bug.lean
@@ -1,3 +1,4 @@
+module
 example (as bs cs : Array α) (v : α)
         (i : Nat)
         (h₁ : i < as.size)
diff --git a/tests/lean/run/grind_match1.lean b/tests/lean/run/grind_match1.lean
index 3d36d7f891..33c55717a9 100644
--- a/tests/lean/run/grind_match1.lean
+++ b/tests/lean/run/grind_match1.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
 def g (xs : List α) (ys : List α) :=
   match xs, ys with
   | [], _         => ys
diff --git a/tests/lean/run/grind_match2.lean b/tests/lean/run/grind_match2.lean
index 108c4fa0c2..f692cfff0d 100644
--- a/tests/lean/run/grind_match2.lean
+++ b/tests/lean/run/grind_match2.lean
@@ -1,3 +1,6 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
+
 def g (a : α) (as : List α) : List α :=
   match as with
   | [] => [a]
diff --git a/tests/lean/run/grind_match_cond_contra.lean b/tests/lean/run/grind_match_cond_contra.lean
index 74960767ef..2c5b2d4e5e 100644
--- a/tests/lean/run/grind_match_cond_contra.lean
+++ b/tests/lean/run/grind_match_cond_contra.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
 def f : List Nat → List Nat → Nat
   | _, 1 :: _ :: _ => 1
   | _, _ :: _ => 2
diff --git a/tests/lean/run/grind_match_cond_split.lean b/tests/lean/run/grind_match_cond_split.lean
index 90864d43cd..3d7450ad9c 100644
--- a/tests/lean/run/grind_match_cond_split.lean
+++ b/tests/lean/run/grind_match_cond_split.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
 example (x n : Nat)
     : 0 < match x with
           | 0  => 1
diff --git a/tests/lean/run/grind_match_eq_propagation.lean b/tests/lean/run/grind_match_eq_propagation.lean
index 276bf21ef3..c0e1e29714 100644
--- a/tests/lean/run/grind_match_eq_propagation.lean
+++ b/tests/lean/run/grind_match_eq_propagation.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
 set_option grind.debug true
 inductive S where
   | mk1 (n : Nat)
diff --git a/tests/lean/run/grind_match_with_eq.lean b/tests/lean/run/grind_match_with_eq.lean
index f542814355..0fe77779ce 100644
--- a/tests/lean/run/grind_match_with_eq.lean
+++ b/tests/lean/run/grind_match_with_eq.lean
@@ -1,3 +1,6 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
+
 def f (a : Option Nat) (h : a ≠ none) : Nat :=
  match a with
  | some a => a
diff --git a/tests/lean/run/grind_mbtc_1.lean b/tests/lean/run/grind_mbtc_1.lean
index d0935e434c..80b36c450c 100644
--- a/tests/lean/run/grind_mbtc_1.lean
+++ b/tests/lean/run/grind_mbtc_1.lean
@@ -1,3 +1,4 @@
+module
 example (f : Int → Int) (x : Int)
     : 0 ≤ x → x ≠ 0 → x ≤ 1 → f x = 2 → f 1 = 2 := by
   grind
diff --git a/tests/lean/run/grind_min.lean b/tests/lean/run/grind_min.lean
index e5d8f7cabb..bd3488b70d 100644
--- a/tests/lean/run/grind_min.lean
+++ b/tests/lean/run/grind_min.lean
@@ -1,3 +1,4 @@
+module
 example (as : Array α) (lo hi i j : Nat) (h₁ : lo ≤ i) (_ : i < j) (_ : j ≤ hi) (_ : j < as.size)
     (_ : ¬as.size = 0) : min lo (as.size - 1) ≤ i := by
   grind
diff --git a/tests/lean/run/grind_module_eqs.lean b/tests/lean/run/grind_module_eqs.lean
index cf8f2b724e..e74227a6d7 100644
--- a/tests/lean/run/grind_module_eqs.lean
+++ b/tests/lean/run/grind_module_eqs.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 
 example [IntModule α] (x y : α) : x - y ≠ 0 - 2*y → x + y = 0 → False := by
diff --git a/tests/lean/run/grind_module_normalization.lean b/tests/lean/run/grind_module_normalization.lean
index f73f3e31a1..16981fa04f 100644
--- a/tests/lean/run/grind_module_normalization.lean
+++ b/tests/lean/run/grind_module_normalization.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 variable (R : Type u) [IntModule R]
 set_option grind.debug true
diff --git a/tests/lean/run/grind_module_relations.lean b/tests/lean/run/grind_module_relations.lean
index b2289cd8c0..b6f703d78d 100644
--- a/tests/lean/run/grind_module_relations.lean
+++ b/tests/lean/run/grind_module_relations.lean
@@ -1,3 +1,4 @@
+module
 -- Tests for `grind` as solver for linear equations in an `IntModule` or `RatModule`.
 
 open Lean.Grind
diff --git a/tests/lean/run/grind_mon_order.lean b/tests/lean/run/grind_mon_order.lean
index 6e119e938f..08973e9d31 100644
--- a/tests/lean/run/grind_mon_order.lean
+++ b/tests/lean/run/grind_mon_order.lean
@@ -1,4 +1,6 @@
-import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
+module
+public import Init.Grind.Ring.Poly
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 open Lean.Grind.CommRing
 
 def w : Var := 0
diff --git a/tests/lean/run/grind_mvar.lean b/tests/lean/run/grind_mvar.lean
index c09b476791..d6527b3616 100644
--- a/tests/lean/run/grind_mvar.lean
+++ b/tests/lean/run/grind_mvar.lean
@@ -1,3 +1,4 @@
+module
 open List
 reset_grind_attrs%
 attribute [grind →] Array.eq_empty_of_append_eq_empty eq_nil_of_length_eq_zero
diff --git a/tests/lean/run/grind_natCast.lean b/tests/lean/run/grind_natCast.lean
index 7c99fbfc95..a69d9776af 100644
--- a/tests/lean/run/grind_natCast.lean
+++ b/tests/lean/run/grind_natCast.lean
@@ -1,3 +1,4 @@
+module
 example (x : Nat) : x ≥ (0 : Int) := by grind
 example (x : Nat) : Int.ofNat x ≥ (0 : Int) := by grind
 example (x : Nat) : NatCast.natCast x ≥ 0 := by grind
diff --git a/tests/lean/run/grind_natCast_intCast.lean b/tests/lean/run/grind_natCast_intCast.lean
index c5e592d8c0..252e32c8aa 100644
--- a/tests/lean/run/grind_natCast_intCast.lean
+++ b/tests/lean/run/grind_natCast_intCast.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 
 attribute [local instance] Semiring.natCast Ring.intCast
diff --git a/tests/lean/run/grind_natCast_issue.lean b/tests/lean/run/grind_natCast_issue.lean
index 8321dc5077..a8ea15400c 100644
--- a/tests/lean/run/grind_natCast_issue.lean
+++ b/tests/lean/run/grind_natCast_issue.lean
@@ -1,2 +1,3 @@
+module
 example (n : Int) (n0 : ¬0 ≤ n) (a : Nat) : n ≠ (a : Int) := by
   grind
diff --git a/tests/lean/run/grind_nat_bitwise.lean b/tests/lean/run/grind_nat_bitwise.lean
index 3f0e05c06a..8411785f9e 100644
--- a/tests/lean/run/grind_nat_bitwise.lean
+++ b/tests/lean/run/grind_nat_bitwise.lean
@@ -1,3 +1,4 @@
+module
 example (x y z : Nat) : x &&& (y ||| z) = (x &&& y) ||| (x &&& z) := by grind
 example (w x y z : Nat) : (w ||| x) &&& (y ||| z) = (w &&& y) ||| (w &&& z) ||| (x &&& y) ||| (x &&& z) := by grind
 
diff --git a/tests/lean/run/grind_nat_semiring.lean b/tests/lean/run/grind_nat_semiring.lean
index e057b54da2..63f0727517 100644
--- a/tests/lean/run/grind_nat_semiring.lean
+++ b/tests/lean/run/grind_nat_semiring.lean
@@ -1,3 +1,4 @@
+module
 example (a b : Nat) : 3 * a * b = a * b * 3 := by grind
 
 example (k z : Nat) : k * (z * 2 * (z * 2 + 1)) = z * (k * (2 * (z * 2 + 1))) := by grind
diff --git a/tests/lean/run/grind_nat_sub_encoding.lean b/tests/lean/run/grind_nat_sub_encoding.lean
index 92efcbf643..e0f7bda4ad 100644
--- a/tests/lean/run/grind_nat_sub_encoding.lean
+++ b/tests/lean/run/grind_nat_sub_encoding.lean
@@ -1,3 +1,4 @@
+module
 /-!
 This is a `grind` regression reported by David Renshaw:
 the following proof works in v4.22.0 but not in v4.23.0-rc2. (Increasing the splits threshold does not help.)
diff --git a/tests/lean/run/grind_nested_proof_issue.lean b/tests/lean/run/grind_nested_proof_issue.lean
index de8b141fef..76f49dbc2a 100644
--- a/tests/lean/run/grind_nested_proof_issue.lean
+++ b/tests/lean/run/grind_nested_proof_issue.lean
@@ -1,3 +1,4 @@
+module
 example (as bs : Array α) (v : α)
         (i : Nat)
         (h₁ : i < as.size)
diff --git a/tests/lean/run/grind_nested_proofs.lean b/tests/lean/run/grind_nested_proofs.lean
index b1e55d3256..f9f70b823d 100644
--- a/tests/lean/run/grind_nested_proofs.lean
+++ b/tests/lean/run/grind_nested_proofs.lean
@@ -1,3 +1,4 @@
+module
 import Lean.Meta.Tactic.Grind
 
 def f (α : Type) [Add α] (a : α) := a + a + a
diff --git a/tests/lean/run/grind_nochrono.lean b/tests/lean/run/grind_nochrono.lean
index 021740ecf5..cad5602a2b 100644
--- a/tests/lean/run/grind_nochrono.lean
+++ b/tests/lean/run/grind_nochrono.lean
@@ -1,3 +1,4 @@
+module
 -- In the following test, the first 8 case-splits are irrelevant,
 -- and non-choronological backtracking is used to avoid searching
 -- (2^8 - 1) irrelevant branches
diff --git a/tests/lean/run/grind_norm_levels.lean b/tests/lean/run/grind_norm_levels.lean
index f692c87b68..0c930165a8 100644
--- a/tests/lean/run/grind_norm_levels.lean
+++ b/tests/lean/run/grind_norm_levels.lean
@@ -1,3 +1,4 @@
+module
 import Lean.Meta.Tactic.Grind
 
 def g {α : Sort u} (a : α) := a
diff --git a/tests/lean/run/grind_offset.lean b/tests/lean/run/grind_offset.lean
index d8226fa895..be1f2c1374 100644
--- a/tests/lean/run/grind_offset.lean
+++ b/tests/lean/run/grind_offset.lean
@@ -1,3 +1,4 @@
+module
 opaque g : Nat → Nat
 
 @[simp] def f (a : Nat) :=
diff --git a/tests/lean/run/grind_offset_cnstr.lean b/tests/lean/run/grind_offset_cnstr.lean
index f0083aaf0e..7d33cff821 100644
--- a/tests/lean/run/grind_offset_cnstr.lean
+++ b/tests/lean/run/grind_offset_cnstr.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 
 /--
@@ -256,28 +257,24 @@ example (a b c : Nat) : a + 1 ≤ b → b ≤ c + 2 → a ≤ c + 1 := by
 example (a b c : Nat) : a + 2 ≤ b → b ≤ c + 2 → a ≤ c := by
   grind
 
-theorem ex1 (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 := by
-  grind
-
 /--
-info: theorem ex1._proof_1_1 : ∀ {a4 : Nat} (p : Prop) (a1 a2 a3 : Nat),
-  (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 :=
-fun {a4} p a1 a2 a3 =>
-  intro_with_eq (p ↔ a2 ≤ a1) (p = (a2 ≤ a1)) (¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4) (iff_eq p (a2 ≤ a1))
-    fun h h_1 h_2 =>
-    intro_with_eq (p ↔ a4 ≤ a3 + 2) (p = (a4 ≤ a3 + 2)) (a1 ≤ a4) (iff_eq p (a4 ≤ a3 + 2)) fun h_3 =>
-      Classical.byContradiction
-        (intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_le_eq a1 a4) fun h_4 =>
-          Eq.mp
-            (Eq.trans (Eq.symm (eq_true h_4))
-              (Nat.lo_eq_false_of_lo a1 a4 7 1 rfl_true
-                (Nat.lo_lo a1 a2 a4 1 6 (Nat.of_le_eq_false a2 a1 (Eq.trans (Eq.symm h) (eq_false h_1)))
-                  (Nat.lo_lo a2 a3 a4 3 3 h_2 (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm h_3) (eq_false h_1)))))))
-            True.intro)
+trace: [grind.debug.proof] intro_with_eq (p ↔ a2 ≤ a1) (p = (a2 ≤ a1)) (¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4)
+      (iff_eq p (a2 ≤ a1)) fun h h_1 h_2 =>
+      intro_with_eq (p ↔ a4 ≤ a3 + 2) (p = (a4 ≤ a3 + 2)) (a1 ≤ a4) (iff_eq p (a4 ≤ a3 + 2)) fun h_3 =>
+        Classical.byContradiction
+          (intro_with_eq (¬a1 ≤ a4) (a4 + 1 ≤ a1) False (Nat.not_le_eq a1 a4) fun h_4 =>
+            Eq.mp
+              (Eq.trans (Eq.symm (eq_true h_4))
+                (Nat.lo_eq_false_of_lo a1 a4 7 1 rfl_true
+                  (Nat.lo_lo a1 a2 a4 1 6 (Nat.of_le_eq_false a2 a1 (Eq.trans (Eq.symm h) (eq_false h_1)))
+                    (Nat.lo_lo a2 a3 a4 3 3 h_2 (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm h_3) (eq_false h_1)))))))
+              True.intro)
 -/
 #guard_msgs in
 open Lean Grind in
-#print ex1._proof_1_1
+set_option trace.grind.debug.proof true in
+theorem ex1 (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → (p ↔ a4 ≤ a3 + 2) → a1 ≤ a4 := by
+  grind
 
 /-! Propagate `cnstr = False` tests -/
 
diff --git a/tests/lean/run/grind_offset_model.lean b/tests/lean/run/grind_offset_model.lean
index f9bd77a500..4639fc1128 100644
--- a/tests/lean/run/grind_offset_model.lean
+++ b/tests/lean/run/grind_offset_model.lean
@@ -1,3 +1,4 @@
+module
 def g (i : Nat) (j : Nat) := i + j
 
 set_option grind.debug true
diff --git a/tests/lean/run/grind_omega_examples.lean b/tests/lean/run/grind_omega_examples.lean
index 0a0d594db7..54bc59e9a9 100644
--- a/tests/lean/run/grind_omega_examples.lean
+++ b/tests/lean/run/grind_omega_examples.lean
@@ -1,3 +1,4 @@
+module
 example {x y : Nat} (_ : x + y > 10) (_ : x < 5) (_ : y < 5) : False := by grind
 example {x y : Nat} (_ : x + y > 10) (_ : 2 * x < 11) (_ : y < 5) : False := by grind
 example {x y : Nat} (_ : 2 * x + 4 * y = 5) : False := by grind
diff --git a/tests/lean/run/grind_omega_tests.lean b/tests/lean/run/grind_omega_tests.lean
index cb2347c893..258d7791d0 100644
--- a/tests/lean/run/grind_omega_tests.lean
+++ b/tests/lean/run/grind_omega_tests.lean
@@ -1,3 +1,4 @@
+module
 class SubNegMonoid (G : Type u) extends Neg G where
 
 instance Int.instSubNegMonoid : SubNegMonoid Int where
diff --git a/tests/lean/run/grind_option.lean b/tests/lean/run/grind_option.lean
index 914467f78c..0a5bc5997d 100644
--- a/tests/lean/run/grind_option.lean
+++ b/tests/lean/run/grind_option.lean
@@ -1,3 +1,4 @@
+module
 -- This file uses `#guard_msgs` to check which lemmas `grind` is using.
 -- This may prove fragile, so remember it is okay to update the expected output if appropriate!
 -- Hopefully these will act as regression tests against `grind` activating irrelevant lemmas.
diff --git a/tests/lean/run/grind_ord_module.lean b/tests/lean/run/grind_ord_module.lean
index c790ffccc8..8922c6445a 100644
--- a/tests/lean/run/grind_ord_module.lean
+++ b/tests/lean/run/grind_ord_module.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 
 variable (R : Type u) [IntModule R] [LE R] [LT R] [LinearOrder R] [OrderedAdd R]
diff --git a/tests/lean/run/grind_overapplied_ite.lean b/tests/lean/run/grind_overapplied_ite.lean
index 3b8d750bf1..0262c29c2a 100644
--- a/tests/lean/run/grind_overapplied_ite.lean
+++ b/tests/lean/run/grind_overapplied_ite.lean
@@ -1,3 +1,4 @@
+module
 example : (if (!false) = true then id else id) false = false := by
   grind
 
diff --git a/tests/lean/run/grind_palindrome2.lean b/tests/lean/run/grind_palindrome2.lean
index 09822e12c8..d1f5bab22f 100644
--- a/tests/lean/run/grind_palindrome2.lean
+++ b/tests/lean/run/grind_palindrome2.lean
@@ -1,3 +1,4 @@
+module
 def IsPalindrome (xs : Array Nat) : Prop := xs.reverse = xs
 
 def checkPalin1 (xs : Array Nat) : Bool :=
diff --git a/tests/lean/run/grind_palindromes.lean b/tests/lean/run/grind_palindromes.lean
index 376fc5a94e..7da2e66b06 100644
--- a/tests/lean/run/grind_palindromes.lean
+++ b/tests/lean/run/grind_palindromes.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
 reset_grind_attrs%
 
 attribute [grind cases] Or
diff --git a/tests/lean/run/grind_panic_invariant.lean b/tests/lean/run/grind_panic_invariant.lean
index 72b3184de3..9399d00bb0 100644
--- a/tests/lean/run/grind_panic_invariant.lean
+++ b/tests/lean/run/grind_panic_invariant.lean
@@ -1,3 +1,4 @@
+module
 -- grind fails, but also produces a panic.
 
 @[grind] inductive star (R : α → α → Prop) : α → α → Prop where
diff --git a/tests/lean/run/grind_params.lean b/tests/lean/run/grind_params.lean
index 66f0955241..8cd5ebdf28 100644
--- a/tests/lean/run/grind_params.lean
+++ b/tests/lean/run/grind_params.lean
@@ -1,3 +1,4 @@
+module
 def foo (x : Nat) := x + 2
 
 example (f : Nat → Nat) : f (foo a) = b → f (c + 1) = d → c = a + 1 → b = d := by
@@ -19,11 +20,11 @@ error: invalid `grind` forward theorem, theorem `blathm` does not have propositi
 example : bla (foo a) = b → bla b = bla (a + 2) := by
   grind [foo, → blathm]
 
-opaque P : Nat → Prop
-opaque Q : Nat → Prop
+public opaque P : Nat → Prop
+public opaque Q : Nat → Prop
 opaque R : Nat → Prop
 
-theorem pq : P x → Q x := sorry
+public theorem pq : P x → Q x := sorry
 theorem qr : Q x → R x := sorry
 
 example : P x → R x := by
diff --git a/tests/lean/run/grind_pattern1.lean b/tests/lean/run/grind_pattern1.lean
index fe9a2f9abc..6b778d12d7 100644
--- a/tests/lean/run/grind_pattern1.lean
+++ b/tests/lean/run/grind_pattern1.lean
@@ -1,3 +1,6 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
+
 set_option trace.grind.ematch.pattern true
 
 /--
diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean
index 0b16cab693..29d416a5ff 100644
--- a/tests/lean/run/grind_pattern2.lean
+++ b/tests/lean/run/grind_pattern2.lean
@@ -1,3 +1,4 @@
+module
 def Set (α : Type) := α → Bool
 
 def insertElem [DecidableEq α] (s : Set α) (a : α) : Set α :=
diff --git a/tests/lean/run/grind_pattern3.lean b/tests/lean/run/grind_pattern3.lean
index 189c207fa3..f4d2df422b 100644
--- a/tests/lean/run/grind_pattern3.lean
+++ b/tests/lean/run/grind_pattern3.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 def Set (α : Type) := α → Bool
 
diff --git a/tests/lean/run/grind_pattern_proj.lean b/tests/lean/run/grind_pattern_proj.lean
index d98fab52db..9a974b4fdf 100644
--- a/tests/lean/run/grind_pattern_proj.lean
+++ b/tests/lean/run/grind_pattern_proj.lean
@@ -1,3 +1,4 @@
+module
 universe v v₁ v₂ u u₁ u₂
 
 namespace CategoryTheory
diff --git a/tests/lean/run/grind_pow_add_semiring.lean b/tests/lean/run/grind_pow_add_semiring.lean
index 2fdb7b9142..56910a4b8a 100644
--- a/tests/lean/run/grind_pow_add_semiring.lean
+++ b/tests/lean/run/grind_pow_add_semiring.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 
 variable [Field R]
diff --git a/tests/lean/run/grind_pow_zero.lean b/tests/lean/run/grind_pow_zero.lean
index ad30a41243..a2e945569d 100644
--- a/tests/lean/run/grind_pow_zero.lean
+++ b/tests/lean/run/grind_pow_zero.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 
 example [CommRing α] (a : α) : a^0 = 1 := by grind
diff --git a/tests/lean/run/grind_pp_attr.lean b/tests/lean/run/grind_pp_attr.lean
index 306dc6b6f8..42000c78f9 100644
--- a/tests/lean/run/grind_pp_attr.lean
+++ b/tests/lean/run/grind_pp_attr.lean
@@ -1,3 +1,4 @@
+module
 import Lean.Elab.Command
 
 open Lean Elab Command
diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean
index afd930a734..2a8373dfa8 100644
--- a/tests/lean/run/grind_pre.lean
+++ b/tests/lean/run/grind_pre.lean
@@ -1,3 +1,4 @@
+module
 abbrev f (a : α) := a
 set_option grind.debug true
 set_option grind.debug.proofs true
diff --git a/tests/lean/run/grind_preord_module.lean b/tests/lean/run/grind_preord_module.lean
index 733b06ac20..cb6db38f81 100644
--- a/tests/lean/run/grind_preord_module.lean
+++ b/tests/lean/run/grind_preord_module.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 
 -- `grind linarith` currently does not support negation of linear constraints.
diff --git a/tests/lean/run/grind_prod.lean b/tests/lean/run/grind_prod.lean
index 3a04a84362..34d595c32c 100644
--- a/tests/lean/run/grind_prod.lean
+++ b/tests/lean/run/grind_prod.lean
@@ -1,3 +1,4 @@
+module
 open Prod
 
 theorem swap_swap : ∀ x : α × β, swap (swap x) = x
diff --git a/tests/lean/run/grind_product_eta_and_split.lean b/tests/lean/run/grind_product_eta_and_split.lean
index b0c8f0b007..76212741ee 100644
--- a/tests/lean/run/grind_product_eta_and_split.lean
+++ b/tests/lean/run/grind_product_eta_and_split.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 
 def α : Type := Unit × Unit
diff --git a/tests/lean/run/grind_prop_arrow.lean b/tests/lean/run/grind_prop_arrow.lean
index 2f29830ae2..d86cf6653f 100644
--- a/tests/lean/run/grind_prop_arrow.lean
+++ b/tests/lean/run/grind_prop_arrow.lean
@@ -1,3 +1,4 @@
+module
 opaque f (a : Array Bool) (i : Nat) (h : i < a.size) : Bool
 
 set_option trace.grind.eqc true
diff --git a/tests/lean/run/grind_propagate_connectives.lean b/tests/lean/run/grind_propagate_connectives.lean
index 350b59b66f..1072f59da7 100644
--- a/tests/lean/run/grind_propagate_connectives.lean
+++ b/tests/lean/run/grind_propagate_connectives.lean
@@ -1,3 +1,4 @@
+module
 import Lean.Meta.Tactic.Grind
 
 set_option trace.Meta.debug true
diff --git a/tests/lean/run/grind_proveEqIssue.lean b/tests/lean/run/grind_proveEqIssue.lean
index 44e54c9df4..a82548bfd4 100644
--- a/tests/lean/run/grind_proveEqIssue.lean
+++ b/tests/lean/run/grind_proveEqIssue.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 open List Nat
 
diff --git a/tests/lean/run/grind_qsort.lean b/tests/lean/run/grind_qsort.lean
index 439a19bc38..1fdc9efe6f 100644
--- a/tests/lean/run/grind_qsort.lean
+++ b/tests/lean/run/grind_qsort.lean
@@ -3,7 +3,6 @@ Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
-
 module
 import all Init.Data.Array.QSort.Basic
 
diff --git a/tests/lean/run/grind_refl_cmp.lean b/tests/lean/run/grind_refl_cmp.lean
index a196882b93..c50fa1b57e 100644
--- a/tests/lean/run/grind_refl_cmp.lean
+++ b/tests/lean/run/grind_refl_cmp.lean
@@ -1,4 +1,5 @@
-import Std
+module
+import Std.Data
 
 example (f : α → α → Ordering) [Std.ReflCmp f] (a : α) : f a a = .eq := by
   grind
diff --git a/tests/lean/run/grind_regression.lean b/tests/lean/run/grind_regression.lean
index 5cc3f2438c..9d38fcc8bc 100644
--- a/tests/lean/run/grind_regression.lean
+++ b/tests/lean/run/grind_regression.lean
@@ -1,9 +1,10 @@
+module
 /-
 Copyright (c) 2024 Marcus Rossel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Marcus Rossel, Kim Morrison
 -/
-import Lean.Elab.Term
+public meta import Lean.Elab.Term
 /-!
 These tests are originally from the `lean-egg` repository at
 https://github.com/marcusrossel/lean-egg and were written by Marcus Rossel.
diff --git a/tests/lean/run/grind_ring_1.lean b/tests/lean/run/grind_ring_1.lean
index 7030ae49fb..1a8d85f307 100644
--- a/tests/lean/run/grind_ring_1.lean
+++ b/tests/lean/run/grind_ring_1.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 
 open Lean.Grind
diff --git a/tests/lean/run/grind_ring_2.lean b/tests/lean/run/grind_ring_2.lean
index 9289ed7e9b..6d281eae13 100644
--- a/tests/lean/run/grind_ring_2.lean
+++ b/tests/lean/run/grind_ring_2.lean
@@ -1,3 +1,4 @@
+module
 set_option grind.debug true
 open Lean.Grind
 
diff --git a/tests/lean/run/grind_ring_3.lean b/tests/lean/run/grind_ring_3.lean
index 0aedea597e..f12f364b96 100644
--- a/tests/lean/run/grind_ring_3.lean
+++ b/tests/lean/run/grind_ring_3.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 
 example {α} [CommRing α] [IsCharP α 0]
diff --git a/tests/lean/run/grind_ring_4.lean b/tests/lean/run/grind_ring_4.lean
index c16ed99123..3a073f5039 100644
--- a/tests/lean/run/grind_ring_4.lean
+++ b/tests/lean/run/grind_ring_4.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 
 example {α} [CommRing α] [IsCharP α 0] [NoNatZeroDivisors α]
diff --git a/tests/lean/run/grind_ring_5.lean b/tests/lean/run/grind_ring_5.lean
index da09fec46b..f20b3bdebb 100644
--- a/tests/lean/run/grind_ring_5.lean
+++ b/tests/lean/run/grind_ring_5.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 
 
diff --git a/tests/lean/run/grind_ring_trim_context.lean b/tests/lean/run/grind_ring_trim_context.lean
index 283a2d1f7c..9be264d8a9 100644
--- a/tests/lean/run/grind_ring_trim_context.lean
+++ b/tests/lean/run/grind_ring_trim_context.lean
@@ -1,3 +1,4 @@
+module
 /--
 trace: [grind.debug.proof] fun h h_1 h_2 h_3 =>
       Classical.byContradiction fun h_4 =>
diff --git a/tests/lean/run/grind_semiring.lean b/tests/lean/run/grind_semiring.lean
index 046d2d06df..f3182ae268 100644
--- a/tests/lean/run/grind_semiring.lean
+++ b/tests/lean/run/grind_semiring.lean
@@ -1,3 +1,4 @@
+module
 example (n t : Nat) : 1 ^ (n / 3) * 2 ^ t = 2 ^ t := by grind
 
 example (n t : Nat) : (1 : Int) ^ (n / 3) * 2 ^ t = 2 ^ t := by grind
diff --git a/tests/lean/run/grind_semiring_norm.lean b/tests/lean/run/grind_semiring_norm.lean
index 33c2469330..9b560d1e38 100644
--- a/tests/lean/run/grind_semiring_norm.lean
+++ b/tests/lean/run/grind_semiring_norm.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 
 section CommSemiring
diff --git a/tests/lean/run/grind_shelf.lean b/tests/lean/run/grind_shelf.lean
index b2a067344b..3579874bb7 100644
--- a/tests/lean/run/grind_shelf.lean
+++ b/tests/lean/run/grind_shelf.lean
@@ -1,3 +1,4 @@
+module
 class Shelf (α : Type u) where
   act : α → α → α
   self_distrib : ∀ {x y z : α}, act x (act y z) = act (act x y) (act x z)
diff --git a/tests/lean/run/grind_smul_issue.lean b/tests/lean/run/grind_smul_issue.lean
index 24cb202147..6ac4b995e5 100644
--- a/tests/lean/run/grind_smul_issue.lean
+++ b/tests/lean/run/grind_smul_issue.lean
@@ -1,3 +1,4 @@
+module
 example (x : BitVec 2) : x - 2 • x + x = 0 := by
   grind
 
diff --git a/tests/lean/run/grind_som1.lean b/tests/lean/run/grind_som1.lean
index e1d4d3b2ea..da2fbffe7c 100644
--- a/tests/lean/run/grind_som1.lean
+++ b/tests/lean/run/grind_som1.lean
@@ -1,4 +1,6 @@
+module
 import Lean
+public meta import Lean.Elab.Tactic
 
 open Lean.Grind
 open Lean.Grind.CommRing
diff --git a/tests/lean/run/grind_sort_eqc.lean b/tests/lean/run/grind_sort_eqc.lean
index 958626ae00..c38293a632 100644
--- a/tests/lean/run/grind_sort_eqc.lean
+++ b/tests/lean/run/grind_sort_eqc.lean
@@ -1,3 +1,4 @@
+module
 opaque f [Inhabited α] : α → α
 theorem feq [Inhabited α] [Add α] [One α] (x : α) : f x = f (f x) + 1 := sorry
 opaque g [Inhabited α] : α → α → α
diff --git a/tests/lean/run/grind_split.lean b/tests/lean/run/grind_split.lean
index 56accbc822..84b0d1f95f 100644
--- a/tests/lean/run/grind_split.lean
+++ b/tests/lean/run/grind_split.lean
@@ -1,3 +1,4 @@
+module
 set_option trace.grind.split true
 set_option trace.grind.eqc true
 example (p q : Prop) : p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → False := by
diff --git a/tests/lean/run/grind_split_arith_imp.lean b/tests/lean/run/grind_split_arith_imp.lean
index 7ad7488a3a..ee0fb9217f 100644
--- a/tests/lean/run/grind_split_arith_imp.lean
+++ b/tests/lean/run/grind_split_arith_imp.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 attribute [grind] Vector.getElem_swap_of_ne
 
diff --git a/tests/lean/run/grind_split_data.lean b/tests/lean/run/grind_split_data.lean
index 168e093ff5..87cf74742f 100644
--- a/tests/lean/run/grind_split_data.lean
+++ b/tests/lean/run/grind_split_data.lean
@@ -1,3 +1,4 @@
+module
 inductive C where
   | a | b | c
 
diff --git a/tests/lean/run/grind_split_issue.lean b/tests/lean/run/grind_split_issue.lean
index 435ab672d2..80e9ce7bd4 100644
--- a/tests/lean/run/grind_split_issue.lean
+++ b/tests/lean/run/grind_split_issue.lean
@@ -1,3 +1,4 @@
+module
 variable (d : Nat) in
 inductive X : Nat → Prop
   | f {s : Nat} : X s
diff --git a/tests/lean/run/grind_spoly.lean b/tests/lean/run/grind_spoly.lean
index 738db67227..5115a9299a 100644
--- a/tests/lean/run/grind_spoly.lean
+++ b/tests/lean/run/grind_spoly.lean
@@ -1,3 +1,4 @@
+module
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly
 open Lean.Grind.CommRing
 
diff --git a/tests/lean/run/grind_sym_prio.lean b/tests/lean/run/grind_sym_prio.lean
index 49039d01ba..0cb046fdfc 100644
--- a/tests/lean/run/grind_sym_prio.lean
+++ b/tests/lean/run/grind_sym_prio.lean
@@ -1,3 +1,4 @@
+module
 opaque q : Nat → Prop
 opaque p : Nat → Prop
 
diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean
index dee647db64..06d05fd672 100644
--- a/tests/lean/run/grind_t1.lean
+++ b/tests/lean/run/grind_t1.lean
@@ -1,3 +1,4 @@
+module
 example (a b : List Nat) : a = [] → b = [2] → a = b → False := by
   grind
 
diff --git a/tests/lean/run/grind_toInt_issue.lean b/tests/lean/run/grind_toInt_issue.lean
index 832f7d25fa..a86a2b2451 100644
--- a/tests/lean/run/grind_toInt_issue.lean
+++ b/tests/lean/run/grind_toInt_issue.lean
@@ -1,3 +1,4 @@
+module
 open Lean Grind
 
 example (x : Fin 2) : ToInt.toInt x ≠ 0 → ToInt.toInt x ≠ 1 → False := by
diff --git a/tests/lean/run/grind_toint_instances.lean b/tests/lean/run/grind_toint_instances.lean
index d58a3e9d5c..402ea93eac 100644
--- a/tests/lean/run/grind_toint_instances.lean
+++ b/tests/lean/run/grind_toint_instances.lean
@@ -1,3 +1,4 @@
+module
 open Lean.Grind
 
 #synth ToInt.Add Nat (.ci 0)
diff --git a/tests/lean/run/grind_trace.lean b/tests/lean/run/grind_trace.lean
index 59e7b46e33..718f435a81 100644
--- a/tests/lean/run/grind_trace.lean
+++ b/tests/lean/run/grind_trace.lean
@@ -1,3 +1,4 @@
+module
 reset_grind_attrs%
 
 attribute [grind =] List.length_cons
@@ -47,7 +48,7 @@ theorem map_replicate' : (List.replicate n a).map f = List.replicate n (f a) :=
 theorem mem_of_getLast?_eq_some' {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs := by
   grind?
 
-def f : Nat → Nat
+@[expose] public def f : Nat → Nat
   | 0 => 1
   | _ => 2
 
diff --git a/tests/lean/run/grind_trig.lean b/tests/lean/run/grind_trig.lean
index 2dd3035a50..dddd01634f 100644
--- a/tests/lean/run/grind_trig.lean
+++ b/tests/lean/run/grind_trig.lean
@@ -1,3 +1,4 @@
+module
 axiom R : Type
 instance : Lean.Grind.CommRing R := sorry
 
diff --git a/tests/lean/run/grind_try_exact.lean b/tests/lean/run/grind_try_exact.lean
index 9c70d544d8..1176165816 100644
--- a/tests/lean/run/grind_try_exact.lean
+++ b/tests/lean/run/grind_try_exact.lean
@@ -1,3 +1,5 @@
+module
+public section -- TODO: `try?` fails if theorems are private
 opaque P : Nat → Prop
 opaque Q : Nat → Prop
 
diff --git a/tests/lean/run/grind_try_extend.lean b/tests/lean/run/grind_try_extend.lean
index 2caff6deed..9c691ebf46 100644
--- a/tests/lean/run/grind_try_extend.lean
+++ b/tests/lean/run/grind_try_extend.lean
@@ -1,4 +1,6 @@
-import Lean
+module
+public import Lean
+public meta import Lean.Elab.Tactic
 
 open Lean Meta Elab Tactic Try
 
diff --git a/tests/lean/run/grind_try_trace.lean b/tests/lean/run/grind_try_trace.lean
index 2ab8301de7..4e438870fa 100644
--- a/tests/lean/run/grind_try_trace.lean
+++ b/tests/lean/run/grind_try_trace.lean
@@ -1,3 +1,5 @@
+module
+@[expose] public section -- TODO: remove after we fix congr_eq
 reset_grind_attrs%
 
 /--
@@ -41,7 +43,7 @@ info: Try these:
 example (f : Nat → Nat) : f a = b → a = c → f c = b := by
   try?
 
-def f : Nat → Nat
+public def f : Nat → Nat
   | 0 => 1
   | _ => 2
 
diff --git a/tests/lean/run/grind_unfold_reducible_issue.lean b/tests/lean/run/grind_unfold_reducible_issue.lean
index 67675e5880..76c32e373d 100644
--- a/tests/lean/run/grind_unfold_reducible_issue.lean
+++ b/tests/lean/run/grind_unfold_reducible_issue.lean
@@ -1,3 +1,4 @@
+module
 import Std.Do
 
 /--
diff --git a/tests/lean/run/grind_unfold_reducible_regression.lean b/tests/lean/run/grind_unfold_reducible_regression.lean
index 6ce98fd281..9a5d7ef2ad 100644
--- a/tests/lean/run/grind_unfold_reducible_regression.lean
+++ b/tests/lean/run/grind_unfold_reducible_regression.lean
@@ -1,5 +1,6 @@
-import Std
-
+module
+public import Std.Data.ExtTreeMap
+public section
 open Std
 
 /--
@@ -53,7 +54,7 @@ instance : EmptyCollection (TreeMapD α β d) :=
 instance : Inhabited (TreeMapD α β d) :=
   ⟨empty⟩
 
-@[grind =] theorem getElem_empty (a : α) : (∅ : TreeMapD α β d)[a] = d := rfl
+@[grind =] theorem getElem_empty (a : α) : (∅ : TreeMapD α β d)[a] = d := (rfl)
 
 variable [DecidableEq β]
 
diff --git a/tests/lean/run/grind_univ_poly_ground_pattern.lean b/tests/lean/run/grind_univ_poly_ground_pattern.lean
index cddb01239b..03a8064816 100644
--- a/tests/lean/run/grind_univ_poly_ground_pattern.lean
+++ b/tests/lean/run/grind_univ_poly_ground_pattern.lean
@@ -1,3 +1,4 @@
+module
 /-! Test for E-matching patterns containing nested universe polymorphic ground patterns. -/
 example : Id.run (pure true) = true := by
   grind only [Id.run_pure]
diff --git a/tests/lean/run/grind_usr.lean b/tests/lean/run/grind_usr.lean
index 13d3b736ce..de15f1c713 100644
--- a/tests/lean/run/grind_usr.lean
+++ b/tests/lean/run/grind_usr.lean
@@ -1,11 +1,12 @@
-opaque f : Nat → Nat
+module
+public opaque f : Nat → Nat
 
 /--
 error: the modifier `usr` is only relevant in parameters for `grind only`
 -/
 #guard_msgs (error) in
 @[grind usr]
-theorem fthm : f (f x) = f x := sorry
+public theorem fthm : f (f x) = f x := sorry
 
 /-- trace: [grind.ematch.pattern] fthm: [f #0] -/
 #guard_msgs (trace) in
diff --git a/tests/lean/run/grind_vector.lean b/tests/lean/run/grind_vector.lean
index cd2fd02097..62c777ff79 100644
--- a/tests/lean/run/grind_vector.lean
+++ b/tests/lean/run/grind_vector.lean
@@ -1,3 +1,4 @@
+module
 example [BEq α] (xs ys : Vector α n) : (xs.toList == ys.toList) = (xs == ys) := by grind
 
 example [LT α] {xs ys : Vector α n} : xs.toList < ys.toList ↔ xs < ys := by grind
diff --git a/tests/lean/run/grind_warn_param.lean b/tests/lean/run/grind_warn_param.lean
index 5dd9e2ff26..cf8745fc26 100644
--- a/tests/lean/run/grind_warn_param.lean
+++ b/tests/lean/run/grind_warn_param.lean
@@ -1,4 +1,6 @@
+module
 reset_grind_attrs%
+public section
 set_option warn.sorry false
 
 attribute [grind =] Array.size_set