diff --git a/script/benchReelabRss.lean b/script/benchReelabRss.lean
index 3b6969d3ae..dbbe0bcadf 100644
--- a/script/benchReelabRss.lean
+++ b/script/benchReelabRss.lean
@@ -8,12 +8,12 @@ open Lean.JsonRpc
 Tests language server memory use by repeatedly re-elaborate a given file.
 
 NOTE: only works on Linux for now.
-ot to touch the imports for usual files.
 -/
 
 def main (args : List String) : IO Unit := do
   let leanCmd :: file :: iters :: args := args | panic! "usage: script <lean> <file> <#iterations> <server-args>..."
-  let uri := s!"file:///{file}"
+  let file ← IO.FS.realPath file
+  let uri := s!"file://{file}"
   Ipc.runWith leanCmd (#["--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do
   -- for use with heaptrack:
   --Ipc.runWith "heaptrack" (#[leanCmd, "--worker", "-DstderrAsMessages=false"] ++ args ++ #[uri]) do
diff --git a/src/Init/BinderNameHint.lean b/src/Init/BinderNameHint.lean
index f2d5e259a8..d04722db3d 100644
--- a/src/Init/BinderNameHint.lean
+++ b/src/Init/BinderNameHint.lean
@@ -40,5 +40,5 @@ This gadget is supported by
 It is ineffective in other positions (hyptheses of rewrite rules) or when used by other tactics
 (e.g. `apply`).
 -/
-@[simp ↓]
+@[simp ↓, expose]
 def binderNameHint {α : Sort u} {β : Sort v} {γ : Sort w} (v : α) (binder : β) (e : γ) : γ := e
diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index e9d7f30035..54c6fea91a 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -127,7 +127,7 @@ end Except
 /--
 Adds exceptions of type `ε` to a monad `m`.
 -/
-def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
+@[expose] def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
   m (Except ε α)
 
 /--
diff --git a/src/Init/Control/ExceptCps.lean b/src/Init/Control/ExceptCps.lean
index 3fb22e9eb7..eeec68ae52 100644
--- a/src/Init/Control/ExceptCps.lean
+++ b/src/Init/Control/ExceptCps.lean
@@ -18,7 +18,7 @@ Adds exceptions of type `ε` to a monad `m`.
 Instead of using `Except ε` to model exceptions, this implementation uses continuation passing
 style. This has different performance characteristics from `ExceptT ε`.
 -/
-def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
+@[expose] def ExceptCpsT (ε : Type u) (m : Type u → Type v) (α : Type u) := (β : Type u) → (α → m β) → (ε → m β) → m β
 
 namespace ExceptCpsT
 
diff --git a/src/Init/Control/Id.lean b/src/Init/Control/Id.lean
index eb72b1dfbc..f96f16db8a 100644
--- a/src/Init/Control/Id.lean
+++ b/src/Init/Control/Id.lean
@@ -34,7 +34,7 @@ def containsFive (xs : List Nat) : Bool := Id.run do
 true
 ```
 -/
-def Id (type : Type u) : Type u := type
+@[expose] def Id (type : Type u) : Type u := type
 
 namespace Id
 
@@ -56,7 +56,7 @@ Runs a computation in the identity monad.
 This function is the identity function. Because its parameter has type `Id α`, it causes
 `do`-notation in its arguments to use the `Monad Id` instance.
 -/
-@[always_inline, inline]
+@[always_inline, inline, expose]
 protected def run (x : Id α) : α := x
 
 instance [OfNat α n] : OfNat (Id α) n :=
diff --git a/src/Init/Control/Lawful/Instances.lean b/src/Init/Control/Lawful/Instances.lean
index 68f17d11f1..e3cc50c14c 100644
--- a/src/Init/Control/Lawful/Instances.lean
+++ b/src/Init/Control/Lawful/Instances.lean
@@ -7,7 +7,8 @@ module
 
 prelude
 import Init.Control.Lawful.Basic
-import Init.Control.Except
+import all Init.Control.Except
+import all Init.Control.State
 import Init.Control.StateRef
 import Init.Ext
 
@@ -98,7 +99,7 @@ end ExceptT
 
 instance : LawfulMonad (Except ε) := LawfulMonad.mk'
   (id_map := fun x => by cases x <;> rfl)
-  (pure_bind := fun _ _ => rfl)
+  (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun a _ _ => by cases a <;> rfl)
 
 instance : LawfulApplicative (Except ε) := inferInstance
@@ -247,7 +248,7 @@ instance : LawfulMonad (EStateM ε σ) := .mk'
     match x s with
     | .ok _ _ => rfl
     | .error _ _ => rfl)
-  (pure_bind := fun _ _ => rfl)
+  (pure_bind := fun _ _ => by rfl)
   (bind_assoc := fun x _ _ => funext <| fun s => by
     dsimp only [EStateM.instMonad, EStateM.bind]
     match x s with
diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index 32b0b0d3e7..f211be0498 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -20,7 +20,7 @@ instance : ToBool (Option α) := ⟨Option.isSome⟩
 Adds the ability to fail to a monad. Unlike ordinary exceptions, there is no way to signal why a
 failure occurred.
 -/
-def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
+@[expose] def OptionT (m : Type u → Type v) (α : Type u) : Type v :=
   m (Option α)
 
 /--
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index 711a7311a3..2a4e190a65 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -22,7 +22,7 @@ Adds a mutable state of type `σ` to a monad.
 Actions in the resulting monad are functions that take an initial state and return, in `m`, a tuple
 of a value and a state.
 -/
-def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+@[expose] def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
   σ → m (α × σ)
 
 /--
@@ -47,7 +47,7 @@ A tuple-based state monad.
 Actions in `StateM σ` are functions that take an initial state and return a value paired with a
 final state.
 -/
-@[reducible]
+@[expose, reducible]
 def StateM (σ α : Type u) : Type u := StateT σ Id α
 
 instance {σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α) where
diff --git a/src/Init/Control/StateCps.lean b/src/Init/Control/StateCps.lean
index 35a9fd9136..13a1983f15 100644
--- a/src/Init/Control/StateCps.lean
+++ b/src/Init/Control/StateCps.lean
@@ -18,7 +18,7 @@ The State monad transformer using CPS style.
 An alternative implementation of a state monad transformer that internally uses continuation passing
 style instead of tuples.
 -/
-def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
+@[expose] def StateCpsT (σ : Type u) (m : Type u → Type v) (α : Type u) := (δ : Type u) → σ → (α → σ → m δ) → m δ
 
 namespace StateCpsT
 
diff --git a/src/Init/Control/StateRef.lean b/src/Init/Control/StateRef.lean
index 1a9999ac6c..3cb89aa68f 100644
--- a/src/Init/Control/StateRef.lean
+++ b/src/Init/Control/StateRef.lean
@@ -17,7 +17,7 @@ A state monad that uses an actual mutable reference cell (i.e. an `ST.Ref ω σ`
 
 The macro `StateRefT σ m α` infers `ω` from `m`. It should normally be used instead.
 -/
-def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
+@[expose] def StateRefT' (ω : Type) (σ : Type) (m : Type → Type) (α : Type) : Type := ReaderT (ST.Ref ω σ) m α
 
 /-! Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/
 
diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 0db8d81ea5..0bd6cbad7d 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -12,6 +12,8 @@ import Init.Prelude
 import Init.SizeOf
 set_option linter.missingDocs true -- keep it documented
 
+@[expose] section
+
 universe u v w
 
 /--
diff --git a/src/Init/Data/Array/Attach.lean b/src/Init/Data/Array/Attach.lean
index ee63152b12..f497a4acff 100644
--- a/src/Init/Data/Array/Attach.lean
+++ b/src/Init/Data/Array/Attach.lean
@@ -9,7 +9,7 @@ prelude
 import Init.Data.Array.Mem
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Count
-import Init.Data.List.Attach
+import all Init.Data.List.Attach
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 6ee24f6a4e..1f0b7d5dc1 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -13,8 +13,8 @@ import Init.Data.UInt.BasicAux
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
-import Init.Data.List.ToArrayImpl
-import Init.Data.Array.Set
+import all Init.Data.List.ToArrayImpl
+import all Init.Data.Array.Set
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
diff --git a/src/Init/Data/Array/BasicAux.lean b/src/Init/Data/Array/BasicAux.lean
index 159257664d..73559d4b93 100644
--- a/src/Init/Data/Array/BasicAux.lean
+++ b/src/Init/Data/Array/BasicAux.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
+import all Init.Data.Array.Basic
 import Init.Data.Nat.Linear
 import Init.NotationExtra
 
diff --git a/src/Init/Data/Array/Bootstrap.lean b/src/Init/Data/Array/Bootstrap.lean
index e3819ffacf..eb4906a2ea 100644
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -8,6 +8,7 @@ module
 
 prelude
 import Init.Data.List.TakeDrop
+import all Init.Data.Array.Basic
 
 /-!
 ## Bootstrapping theorems about arrays
@@ -52,8 +53,8 @@ theorem foldlM_toList.aux [Monad m]
   · rename_i i; rw [Nat.succ_add] at H
     simp [foldlM_toList.aux (j := j+1) H]
     rw (occs := [2]) [← List.getElem_cons_drop_succ_eq_drop ‹_›]
-    rfl
-  · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
+    simp
+  · rw [List.drop_of_length_le (Nat.ge_of_not_lt ‹_›)]; simp
 
 @[simp, grind =] theorem foldlM_toList [Monad m]
     {f : β → α → m β} {init : β} {xs : Array α} :
@@ -69,14 +70,14 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
     (xs.toList.take i).reverse.foldlM (fun x y => f y x) init = foldrM.fold f xs 0 i h init := by
   unfold foldrM.fold
   match i with
-  | 0 => simp [List.foldlM, List.take]
+  | 0 => simp
   | i+1 => rw [← List.take_concat_get h]; simp [← aux]
 
 theorem foldrM_eq_reverse_foldlM_toList [Monad m] {f : α → β → m β} {init : β} {xs : Array α} :
     xs.foldrM f init = xs.toList.reverse.foldlM (fun x y => f y x) init := by
   have : xs = #[] ∨ 0 < xs.size :=
     match xs with | ⟨[]⟩ => .inl rfl | ⟨a::l⟩ => .inr (Nat.zero_lt_succ _)
-  match xs, this with | _, .inl rfl => rfl | xs, .inr h => ?_
+  match xs, this with | _, .inl rfl => simp [foldrM] | xs, .inr h => ?_
   simp [foldrM, h, ← foldrM_eq_reverse_foldlM_toList.aux, List.take_length]
 
 @[simp, grind =] theorem foldrM_toList [Monad m]
diff --git a/src/Init/Data/Array/Count.lean b/src/Init/Data/Array/Count.lean
index 64decc3e12..3e131938fc 100644
--- a/src/Init/Data/Array/Count.lean
+++ b/src/Init/Data/Array/Count.lean
@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Count
 
diff --git a/src/Init/Data/Array/DecidableEq.lean b/src/Init/Data/Array/DecidableEq.lean
index 3de14baf3b..594f125a07 100644
--- a/src/Init/Data/Array/DecidableEq.lean
+++ b/src/Init/Data/Array/DecidableEq.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Array.Basic
+import all Init.Data.Array.Basic
 import Init.Data.BEq
 import Init.Data.List.Nat.BEq
 import Init.ByCases
diff --git a/src/Init/Data/Array/Erase.lean b/src/Init/Data/Array/Erase.lean
index 372b4570f7..4e94267933 100644
--- a/src/Init/Data/Array/Erase.lean
+++ b/src/Init/Data/Array/Erase.lean
@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Nat.Basic
diff --git a/src/Init/Data/Array/Find.lean b/src/Init/Data/Array/Find.lean
index 43e468b13e..73cd1fe1da 100644
--- a/src/Init/Data/Array/Find.lean
+++ b/src/Init/Data/Array/Find.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Data.List.Nat.Find
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.Array.Range
diff --git a/src/Init/Data/Array/GetLit.lean b/src/Init/Data/Array/GetLit.lean
index f98cd76a1f..f020cad254 100644
--- a/src/Init/Data/Array/GetLit.lean
+++ b/src/Init/Data/Array/GetLit.lean
@@ -27,11 +27,13 @@ theorem extLit {n : Nat}
     (h : (i : Nat) → (hi : i < n) → xs.getLit i hsz₁ hi = ys.getLit i hsz₂ hi) : xs = ys :=
   Array.ext (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
 
-def toListLitAux (xs : Array α) (n : Nat) (hsz : xs.size = n) : ∀ (i : Nat), i ≤ xs.size → List α → List α
+-- has to be expose for array literal support
+@[expose] def toListLitAux (xs : Array α) (n : Nat) (hsz : xs.size = n) : ∀ (i : Nat), i ≤ xs.size → List α → List α
   | 0,     _,  acc => acc
   | (i+1), hi, acc => toListLitAux xs n hsz i (Nat.le_of_succ_le hi) (xs.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
 
-def toArrayLit (xs : Array α) (n : Nat) (hsz : xs.size = n) : Array α :=
+-- has to be expose for array literal support
+@[expose] def toArrayLit (xs : Array α) (n : Nat) (hsz : xs.size = n) : Array α :=
   List.toArray <| toListLitAux xs n hsz n (hsz ▸ Nat.le_refl _) []
 
 theorem toArrayLit_eq (xs : Array α) (n : Nat) (hsz : xs.size = n) : xs = toArrayLit xs n hsz := by
diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index e8b48a4aca..130a637358 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -8,11 +8,13 @@ module
 prelude
 import Init.Data.Nat.Lemmas
 import Init.Data.List.Range
+import all Init.Data.List.Control
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Modify
 import Init.Data.List.Nat.Basic
 import Init.Data.List.Monadic
 import Init.Data.List.OfFn
+import all Init.Data.Array.Bootstrap
 import Init.Data.Array.Mem
 import Init.Data.Array.DecidableEq
 import Init.Data.Array.Lex.Basic
@@ -852,7 +854,7 @@ abbrev elem_eq_true_of_mem := @contains_eq_true_of_mem
     elem a xs = xs.contains a := by
   simp [elem]
 
-@[grind] theorem contains_empty [BEq α] : (#[] : Array α).contains a = false := rfl
+@[grind] theorem contains_empty [BEq α] : (#[] : Array α).contains a = false := by simp
 
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     elem a xs = true ↔ a ∈ xs := ⟨mem_of_contains_eq_true, contains_eq_true_of_mem⟩
@@ -869,8 +871,8 @@ theorem elem_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
 @[simp, grind] theorem contains_eq_mem [BEq α] [LawfulBEq α] {a : α} {xs : Array α} :
     xs.contains a = decide (a ∈ xs) := by rw [← elem_eq_contains, elem_eq_mem]
 
-@[simp, grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := rfl
-@[simp, grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := rfl
+@[simp, grind] theorem any_empty [BEq α] {p : α → Bool} : (#[] : Array α).any p = false := by simp
+@[simp, grind] theorem all_empty [BEq α] {p : α → Bool} : (#[] : Array α).all p = true := by simp
 
 /-- Variant of `any_push` with a side condition on `stop`. -/
 @[simp, grind] theorem any_push' [BEq α] {xs : Array α} {a : α} {p : α → Bool} (h : stop = xs.size + 1) :
@@ -4152,7 +4154,7 @@ theorem swapAt!_def {xs : Array α} {i : Nat} {v : α} (h : i < xs.size) :
 section replace
 variable [BEq α]
 
-@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by rfl
+@[simp, grind] theorem replace_empty : (#[] : Array α).replace a b = #[] := by simp [replace]
 
 @[simp, grind] theorem replace_singleton {a b c : α} : #[a].replace b c = #[if a == b then c else a] := by
   simp only [replace, List.finIdxOf?_toArray, List.finIdxOf?]
diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean
index 61a9afcea9..69fa203ea0 100644
--- a/src/Init/Data/Array/Lex/Lemmas.lean
+++ b/src/Init/Data/Array/Lex/Lemmas.lean
@@ -6,6 +6,7 @@ Author: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Lex.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Lex
 
diff --git a/src/Init/Data/Array/MapIdx.lean b/src/Init/Data/Array/MapIdx.lean
index 62f5ca3c33..316045e6a3 100644
--- a/src/Init/Data/Array/MapIdx.lean
+++ b/src/Init/Data/Array/MapIdx.lean
@@ -6,10 +6,11 @@ Authors: Mario Carneiro, Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.Array.OfFn
-import Init.Data.List.MapIdx
+import all Init.Data.List.MapIdx
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
diff --git a/src/Init/Data/Array/Monadic.lean b/src/Init/Data/Array/Monadic.lean
index 5a641c5c21..33acd55e1d 100644
--- a/src/Init/Data/Array/Monadic.lean
+++ b/src/Init/Data/Array/Monadic.lean
@@ -6,6 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.List.Control
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.Array.Attach
 import Init.Data.List.Monadic
diff --git a/src/Init/Data/Array/OfFn.lean b/src/Init/Data/Array/OfFn.lean
index ab6b7532df..bdd6351175 100644
--- a/src/Init/Data/Array/OfFn.lean
+++ b/src/Init/Data/Array/OfFn.lean
@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.OfFn
 
diff --git a/src/Init/Data/Array/Perm.lean b/src/Init/Data/Array/Perm.lean
index ca23b7ef62..75af793a38 100644
--- a/src/Init/Data/Array/Perm.lean
+++ b/src/Init/Data/Array/Perm.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Data.List.Nat.Perm
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
diff --git a/src/Init/Data/Array/Range.lean b/src/Init/Data/Array/Range.lean
index c0e332ce0c..47e1f007ea 100644
--- a/src/Init/Data/Array/Range.lean
+++ b/src/Init/Data/Array/Range.lean
@@ -7,7 +7,8 @@ module
 
 prelude
 import Init.Data.Array.Lemmas
-import Init.Data.Array.OfFn
+import all Init.Data.Array.Basic
+import all Init.Data.Array.OfFn
 import Init.Data.Array.MapIdx
 import Init.Data.Array.Zip
 import Init.Data.List.Nat.Range
@@ -80,7 +81,7 @@ theorem range'_append {s m n step : Nat} :
     range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1)
 
 theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ #[s + step * n] := by
-  simpa using range'_append.symm
+  simp [← range'_append]
 
 theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ #[s + n] := by
   simp [range'_concat]
diff --git a/src/Init/Data/Array/Subarray/Split.lean b/src/Init/Data/Array/Subarray/Split.lean
index f75ae8dd01..c431037fc3 100644
--- a/src/Init/Data/Array/Subarray/Split.lean
+++ b/src/Init/Data/Array/Subarray/Split.lean
@@ -8,7 +8,7 @@ module
 
 prelude
 import Init.Data.Array.Basic
-import Init.Data.Array.Subarray
+import all Init.Data.Array.Subarray
 import Init.Omega
 
 /-
diff --git a/src/Init/Data/Array/TakeDrop.lean b/src/Init/Data/Array/TakeDrop.lean
index 7262302a11..de1db6899d 100644
--- a/src/Init/Data/Array/TakeDrop.lean
+++ b/src/Init/Data/Array/TakeDrop.lean
@@ -6,6 +6,7 @@ Authors: Markus Himmel
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Lemmas
 import Init.Data.List.Nat.TakeDrop
 
diff --git a/src/Init/Data/Array/Zip.lean b/src/Init/Data/Array/Zip.lean
index f2822618db..4ee3287f7b 100644
--- a/src/Init/Data/Array/Zip.lean
+++ b/src/Init/Data/Array/Zip.lean
@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.TakeDrop
 import Init.Data.List.Zip
 
diff --git a/src/Init/Data/BitVec/BasicAux.lean b/src/Init/Data/BitVec/BasicAux.lean
index 06d331b586..84f32e4c8c 100644
--- a/src/Init/Data/BitVec/BasicAux.lean
+++ b/src/Init/Data/BitVec/BasicAux.lean
@@ -22,7 +22,7 @@ section Nat
 /--
 The bitvector with value `i mod 2^n`.
 -/
-@[match_pattern]
+@[expose, match_pattern]
 protected def ofNat (n : Nat) (i : Nat) : BitVec n where
   toFin := Fin.ofNat' (2^n) i
 
diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean
index 6a57da700a..e2d1d7e543 100644
--- a/src/Init/Data/BitVec/Bitblast.lean
+++ b/src/Init/Data/BitVec/Bitblast.lean
@@ -7,9 +7,11 @@ module
 
 prelude
 import Init.Data.BitVec.Folds
+import all Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Mod
+import all Init.Data.Int.DivMod
 import Init.Data.Int.LemmasAux
-import Init.Data.BitVec.Lemmas
+import all Init.Data.BitVec.Lemmas
 
 /-!
 # Bit blasting of bitvectors
diff --git a/src/Init/Data/BitVec/Folds.lean b/src/Init/Data/BitVec/Folds.lean
index 23585f7619..8ad231d06b 100644
--- a/src/Init/Data/BitVec/Folds.lean
+++ b/src/Init/Data/BitVec/Folds.lean
@@ -6,6 +6,7 @@ Authors: Joe Hendrix, Harun Khan
 module
 
 prelude
+import all Init.Data.BitVec.Basic
 import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 6171ebda51..270e00c11e 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -8,7 +8,8 @@ module
 
 prelude
 import Init.Data.Bool
-import Init.Data.BitVec.Basic
+import all Init.Data.BitVec.Basic
+import all Init.Data.BitVec.BasicAux
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Div.Lemmas
@@ -343,7 +344,7 @@ theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
   cases b <;> rfl
 
 @[simp] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by
-  cases b <;> rfl
+  cases b <;> simp
 
 @[simp] theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat) := by
   cases b <;> rfl
@@ -1972,7 +1973,7 @@ theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} :
 /-! ### shiftLeft reductions from BitVec to Nat -/
 
 @[simp]
-theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat := by rfl
+theorem shiftLeft_eq' {x : BitVec w₁} {y : BitVec w₂} : x <<< y = x <<< y.toNat := rfl
 
 theorem shiftLeft_zero' {x : BitVec w₁} : x <<< 0#w₂ = x := by simp
 
@@ -2132,7 +2133,7 @@ theorem msb_ushiftRight {x : BitVec w} {n : Nat} :
 
 @[simp]
 theorem ushiftRight_eq' (x : BitVec w₁) (y : BitVec w₂) :
-    x >>> y = x >>> y.toNat := by rfl
+    x >>> y = x >>> y.toNat := rfl
 
 theorem ushiftRight_ofNat_eq {x : BitVec w} {k : Nat} : x >>> (BitVec.ofNat w k) = x >>> (k % 2^w) := rfl
 
@@ -3372,7 +3373,7 @@ theorem add_eq_xor {a b : BitVec 1} : a + b = a ^^^ b := by
 
 /-! ### sub/neg -/
 
-theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := by rfl
+theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toNat) := rfl
 
 @[simp] theorem toNat_sub {n} (x y : BitVec n) :
     (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl
@@ -3683,7 +3684,7 @@ theorem fill_false {w : Nat} : fill w false = 0#w := by
 
 /-! ### mul -/
 
-theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
+theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := rfl
 
 @[simp, bitvec_to_nat] theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
 @[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl
@@ -4166,7 +4167,7 @@ theorem sdiv_eq_and (x y : BitVec 1) : x.sdiv y = x &&& y := by
   have hy : y = 0#1 ∨ y = 1#1 := by bv_omega
   rcases hx with rfl | rfl <;>
     rcases hy with rfl | rfl <;>
-      rfl
+      simp
 
 @[simp]
 theorem sdiv_self {x : BitVec w} :
@@ -5349,7 +5350,7 @@ theorem neg_ofNat_eq_ofInt_neg {w : Nat} {x : Nat} :
 
 /-! ### abs -/
 
-theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := by rfl
+theorem abs_eq (x : BitVec w) : x.abs = if x.msb then -x else x := rfl
 
 @[simp, bitvec_to_nat]
 theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
index a8edd526db..20455896d9 100644
--- a/src/Init/Data/Bool.lean
+++ b/src/Init/Data/Bool.lean
@@ -432,7 +432,7 @@ theorem and_or_inj_left_iff :
 /--
 Converts `true` to `1` and `false` to `0`.
 -/
-def toNat (b : Bool) : Nat := cond b 1 0
+@[expose] def toNat (b : Bool) : Nat := cond b 1 0
 
 @[simp, bitvec_to_nat] theorem toNat_false : false.toNat = 0 := rfl
 
@@ -687,7 +687,7 @@ def boolPredToPred : Coe (α → Bool) (α  → Prop) where
 This should not be turned on globally as an instance because it degrades performance in Mathlib,
 but may be used locally.
 -/
-def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
+@[expose] def boolRelToRel : Coe (α → α → Bool) (α → α → Prop) where
   coe r := fun a b => Eq (r a b) true
 
 /-! ### subtypes -/
diff --git a/src/Init/Data/ByteArray/Basic.lean b/src/Init/Data/ByteArray/Basic.lean
index df1425eafa..75a387d5eb 100644
--- a/src/Init/Data/ByteArray/Basic.lean
+++ b/src/Init/Data/ByteArray/Basic.lean
@@ -9,6 +9,7 @@ prelude
 import Init.Data.Array.Basic
 import Init.Data.Array.Subarray
 import Init.Data.UInt.Basic
+import all Init.Data.UInt.BasicAux
 import Init.Data.Option.Basic
 universe u
 
diff --git a/src/Init/Data/Cast.lean b/src/Init/Data/Cast.lean
index 65931ce137..037b7c1da1 100644
--- a/src/Init/Data/Cast.lean
+++ b/src/Init/Data/Cast.lean
@@ -64,7 +64,7 @@ class NatCast (R : Type u) where
 
 instance : NatCast Nat where natCast n := n
 
-@[coe, reducible, match_pattern, inherit_doc NatCast]
+@[coe, expose, reducible, match_pattern, inherit_doc NatCast]
 protected def Nat.cast {R : Type u} [NatCast R] : Nat → R :=
   NatCast.natCast
 
diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean
index 88df42e589..1e89f580f6 100644
--- a/src/Init/Data/Char/Basic.lean
+++ b/src/Init/Data/Char/Basic.lean
@@ -20,13 +20,13 @@ namespace Char
 /--
 One character is less than another if its code point is strictly less than the other's.
 -/
-protected def lt (a b : Char) : Prop := a.val < b.val
+@[expose] protected def lt (a b : Char) : Prop := a.val < b.val
 
 /--
 One character is less than or equal to another if its code point is less than or equal to the
 other's.
 -/
-protected def le (a b : Char) : Prop := a.val ≤ b.val
+@[expose] protected def le (a b : Char) : Prop := a.val ≤ b.val
 
 instance : LT Char := ⟨Char.lt⟩
 instance : LE Char := ⟨Char.le⟩
diff --git a/src/Init/Data/Char/Lemmas.lean b/src/Init/Data/Char/Lemmas.lean
index 4fbc4f43ab..ea7a7336de 100644
--- a/src/Init/Data/Char/Lemmas.lean
+++ b/src/Init/Data/Char/Lemmas.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
-import Init.Data.Char.Basic
+import all Init.Data.Char.Basic
 import Init.Data.UInt.Lemmas
 
 namespace Char
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 28976e74ee..302a114a59 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -8,6 +8,8 @@ module
 prelude
 import Init.Data.Nat.Bitwise.Basic
 
+@[expose] section
+
 open Nat
 
 namespace Fin
@@ -44,7 +46,7 @@ Returns `a` modulo `n` as a `Fin n`.
 
 The assumption `NeZero n` ensures that `Fin n` is nonempty.
 -/
-protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
+@[expose] protected def ofNat' (n : Nat) [NeZero n] (a : Nat) : Fin n :=
   ⟨a % n, Nat.mod_lt _ (pos_of_neZero n)⟩
 
 /--
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index 446edb85a3..35b6d7e86a 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -6,7 +6,6 @@ Authors: Mario Carneiro, Leonardo de Moura
 module
 
 prelude
-import Init.Data.Fin.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Int.DivMod.Lemmas
 import Init.Ext
diff --git a/src/Init/Data/Function.lean b/src/Init/Data/Function.lean
index 6db6c5212d..2075027f35 100644
--- a/src/Init/Data/Function.lean
+++ b/src/Init/Data/Function.lean
@@ -18,7 +18,7 @@ Examples:
  * `Function.curry (fun (x, y) => x + y) 3 5 = 8`
  * `Function.curry Prod.swap 3 "five" = ("five", 3)`
 -/
-@[inline]
+@[inline, expose]
 def curry : (α × β → φ) → α → β → φ := fun f a b => f (a, b)
 
 /--
@@ -28,7 +28,7 @@ Examples:
  * `Function.uncurry List.drop (1, ["a", "b", "c"]) = ["b", "c"]`
  * `[("orange", 2), ("android", 3) ].map (Function.uncurry String.take) = ["or", "and"]`
 -/
-@[inline]
+@[inline, expose]
 def uncurry : (α → β → φ) → α × β → φ := fun f a => f a.1 a.2
 
 @[simp]
diff --git a/src/Init/Data/Int/Basic.lean b/src/Init/Data/Int/Basic.lean
index d79b7fe550..de5c9d0e07 100644
--- a/src/Init/Data/Int/Basic.lean
+++ b/src/Init/Data/Int/Basic.lean
@@ -11,6 +11,8 @@ prelude
 import Init.Data.Cast
 import Init.Data.Nat.Div.Basic
 
+@[expose] section
+
 set_option linter.missingDocs true -- keep it documented
 open Nat
 
diff --git a/src/Init/Data/Int/Bitwise/Lemmas.lean b/src/Init/Data/Int/Bitwise/Lemmas.lean
index e057d40d77..57a160db0d 100644
--- a/src/Init/Data/Int/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Int/Bitwise/Lemmas.lean
@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.Nat.Bitwise.Lemmas
-import Init.Data.Int.Bitwise.Basic
+import all Init.Data.Int.Bitwise.Basic
 import Init.Data.Int.DivMod.Lemmas
 
 namespace Int
diff --git a/src/Init/Data/Int/Compare.lean b/src/Init/Data/Int/Compare.lean
index 8b503c69e7..b53a35d524 100644
--- a/src/Init/Data/Int/Compare.lean
+++ b/src/Init/Data/Int/Compare.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Paul Reichert
 module
 
 prelude
-import Init.Data.Ord
+import all Init.Data.Ord
 import Init.Data.Int.Order
 
 /-! # Basic lemmas about comparing integers
diff --git a/src/Init/Data/Int/DivMod/Basic.lean b/src/Init/Data/Int/DivMod/Basic.lean
index 26ee89d2bf..8e89e76c4c 100644
--- a/src/Init/Data/Int/DivMod/Basic.lean
+++ b/src/Init/Data/Int/DivMod/Basic.lean
@@ -8,6 +8,8 @@ module
 prelude
 import Init.Data.Int.Basic
 
+@[expose] section
+
 open Nat
 
 namespace Int
diff --git a/src/Init/Data/Int/Lemmas.lean b/src/Init/Data/Int/Lemmas.lean
index 94c2406c64..9a0b7e57b3 100644
--- a/src/Init/Data/Int/Lemmas.lean
+++ b/src/Init/Data/Int/Lemmas.lean
@@ -6,7 +6,6 @@ Authors: Jeremy Avigad, Deniz Aydin, Floris van Doorn, Mario Carneiro
 module
 
 prelude
-import Init.Data.Int.Basic
 import Init.Conv
 import Init.NotationExtra
 import Init.PropLemmas
diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 632b6fdada..dffceeddfc 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -12,9 +12,9 @@ import Init.Data.Int.Lemmas
 import Init.Data.Int.LemmasAux
 import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Int.Cooper
-import Init.Data.Int.Gcd
+import all Init.Data.Int.Gcd
 import Init.Data.RArray
-import Init.Data.AC
+import all Init.Data.AC
 
 namespace Int.Linear
 
diff --git a/src/Init/Data/List/Attach.lean b/src/Init/Data/List/Attach.lean
index 7e97886210..a3b408b9e6 100644
--- a/src/Init/Data/List/Attach.lean
+++ b/src/Init/Data/List/Attach.lean
@@ -6,6 +6,7 @@ Authors: Mario Carneiro
 module
 
 prelude
+import all Init.Data.List.Lemmas  -- for dsimping with `getElem?_cons_succ`
 import Init.Data.List.Count
 import Init.Data.Subtype
 import Init.BinderNameHint
@@ -242,9 +243,8 @@ theorem getElem?_pmap {p : α → Prop} {f : ∀ a, p a → β} {l : List α} (h
   | nil => simp
   | cons hd tl hl =>
     rcases i with ⟨i⟩
-    · simp only [Option.pmap]
-      split <;> simp_all
-    · simp only [pmap, getElem?_cons_succ, hl, Option.pmap]
+    · simp
+    · simp only [pmap, getElem?_cons_succ, hl]
 
 set_option linter.deprecated false in
 @[deprecated List.getElem?_pmap (since := "2025-02-12")]
diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean
index 5f5d36848d..d0d98ad01b 100644
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -10,6 +10,8 @@ import Init.SimpLemmas
 import Init.Data.Nat.Basic
 import Init.Data.List.Notation
 
+@[expose] section
+
 /-!
 # Basic operations on `List`.
 
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index c371f62881..c94a059bda 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -9,7 +9,6 @@ prelude
 import Init.Control.Basic
 import Init.Control.Id
 import Init.Control.Lawful
-import Init.Data.List.Basic
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
@@ -341,9 +340,9 @@ def findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : Lis
 theorem findM?_pure {m} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) :
     findM? (m := m) (pure <| p ·) as = pure (as.find? p) := by
   induction as with
-  | nil => rfl
+  | nil => simp [findM?, find?_nil]
   | cons a as ih =>
-    simp only [findM?, find?]
+    simp only [findM?, find?_cons]
     cases p a with
     | true  => simp
     | false => simp [ih]
diff --git a/src/Init/Data/List/FinRange.lean b/src/Init/Data/List/FinRange.lean
index 26c86cd67a..c900188eec 100644
--- a/src/Init/Data/List/FinRange.lean
+++ b/src/Init/Data/List/FinRange.lean
@@ -29,7 +29,7 @@ def finRange (n : Nat) : List (Fin n) := ofFn fun i => i
     (finRange n)[i] = Fin.cast length_finRange ⟨i, h⟩ := by
   simp [List.finRange]
 
-@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange, ofFn]
+@[simp] theorem finRange_zero : finRange 0 = [] := by simp [finRange]
 
 theorem finRange_succ {n} : finRange (n+1) = 0 :: (finRange n).map Fin.succ := by
   apply List.ext_getElem; simp; intro i; cases i <;> simp
diff --git a/src/Init/Data/List/Find.lean b/src/Init/Data/List/Find.lean
index e2647724a1..da48058c17 100644
--- a/src/Init/Data/List/Find.lean
+++ b/src/Init/Data/List/Find.lean
@@ -11,6 +11,7 @@ import Init.Data.List.Lemmas
 import Init.Data.List.Sublist
 import Init.Data.List.Range
 import Init.Data.List.Impl
+import all Init.Data.List.Attach
 import Init.Data.Fin.Lemmas
 
 /-!
@@ -94,7 +95,7 @@ theorem findSome?_eq_some_iff {f : α → Option β} {l : List α} {b : β} :
   induction l with
   | nil => simp
   | cons x xs ih =>
-    simp [guard, findSome?, find?]
+    simp [findSome?, find?]
     split <;> rename_i h
     · simp only [Option.guard_eq_some_iff] at h
       obtain ⟨rfl, h⟩ := h
@@ -1002,9 +1003,8 @@ theorem isNone_findFinIdx? {l : List α} {p : α → Bool} :
 @[simp] theorem findFinIdx?_subtype {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp)) := by
-  unfold unattach
   induction l with
-  | nil => simp
+  | nil => simp [unattach]
   | cons a l ih =>
     simp [hf, findFinIdx?_cons]
     split <;> simp [ih, Function.comp_def]
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index c4e6a97cc6..662866c7dc 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -9,8 +9,8 @@ module
 prelude
 import Init.Data.Bool
 import Init.Data.Option.Lemmas
-import Init.Data.List.BasicAux
-import Init.Data.List.Control
+import all Init.Data.List.BasicAux
+import all Init.Data.List.Control
 import Init.Control.Lawful.Basic
 import Init.BinderPredicates
 
@@ -1745,7 +1745,7 @@ theorem head_append_right {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []) (h : l
   rw [head_append, dif_pos (by simp_all)]
 
 @[simp, grind] theorem head?_append {l : List α} : (l ++ l').head? = l.head?.or l'.head? := by
-  cases l <;> rfl
+  cases l <;> simp
 
 -- Note:
 -- `getLast_append_of_ne_nil`, `getLast_append` and `getLast?_append`
@@ -2052,7 +2052,7 @@ theorem eq_iff_flatten_eq : ∀ {L L' : List (List α)},
 
 /-! ### flatMap -/
 
-theorem flatMap_def {l : List α} {f : α → List β} : l.flatMap f = flatten (map f l) := by rfl
+theorem flatMap_def {l : List α} {f : α → List β} : l.flatMap f = flatten (map f l) := rfl
 
 @[simp] theorem flatMap_id {L : List (List α)} : L.flatMap id = L.flatten := by simp [flatMap_def]
 
@@ -3054,7 +3054,7 @@ theorem head?_dropLast {xs : List α} : xs.dropLast.head? = if 1 < xs.length the
 
 theorem getLast_dropLast {xs : List α} (h) :
    xs.dropLast.getLast h =
-     xs[xs.length - 2]'(match xs, h with | (_ :: _ :: _), _ => Nat.lt_trans (Nat.lt_add_one _) (Nat.lt_add_one _)) := by
+     xs[xs.length - 2]'(by match xs, h with | (_ :: _ :: _), _ => exact Nat.lt_trans (Nat.lt_add_one _) (Nat.lt_add_one _)) := by
   rw [getLast_eq_getElem, getElem_dropLast]
   congr 1
   simp; rfl
diff --git a/src/Init/Data/List/Monadic.lean b/src/Init/Data/List/Monadic.lean
index ce1b593fc1..a172ad11a1 100644
--- a/src/Init/Data/List/Monadic.lean
+++ b/src/Init/Data/List/Monadic.lean
@@ -8,6 +8,7 @@ module
 prelude
 import Init.Data.List.TakeDrop
 import Init.Data.List.Attach
+import all Init.Data.List.Control
 
 /-!
 # Lemmas about `List.mapM` and `List.forM`.
@@ -437,7 +438,6 @@ and simplifies these to the function directly taking the value.
     {f : β → { x // p x } → m β} {g : β → α → m β} {x : β}
     (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
     l.foldlM f x = l.unattach.foldlM g x := by
-  unfold unattach
   induction l generalizing x with
   | nil => simp
   | cons a l ih => simp [ih, hf]
@@ -460,7 +460,6 @@ and simplifies these to the function directly taking the value.
     {f : { x // p x } → β → m β} {g : α → β → m β} {x : β}
     (hf : ∀ x h b, f ⟨x, h⟩ b = g x b) :
     l.foldrM f x = l.unattach.foldrM g x := by
-  unfold unattach
   induction l generalizing x with
   | nil => simp
   | cons a l ih =>
@@ -486,7 +485,6 @@ and simplifies these to the function directly taking the value.
 @[simp] theorem mapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → m β} {g : α → m β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.mapM f = l.unattach.mapM g := by
-  unfold unattach
   simp [← List.mapM'_eq_mapM]
   induction l with
   | nil => simp
@@ -504,7 +502,6 @@ and simplifies these to the function directly taking the value.
 @[simp] theorem filterMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → m (Option β)} {g : α → m (Option β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     l.filterMapM f = l.unattach.filterMapM g := by
-  unfold unattach
   induction l with
   | nil => simp
   | cons a l ih => simp [ih, hf, filterMapM_cons]
@@ -523,10 +520,9 @@ and simplifies these to the function directly taking the value.
 @[simp] theorem flatMapM_subtype [Monad m] [LawfulMonad m] {p : α → Prop} {l : List { x // p x }}
     {f : { x // p x } → m (List β)} {g : α → m (List β)} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
     (l.flatMapM f) = l.unattach.flatMapM g := by
-  unfold unattach
   induction l with
-  | nil => simp
-  | cons a l ih => simp [ih, hf]
+  | nil => simp [flatMapM_nil]
+  | cons a l ih => simp only [flatMapM_cons, hf, ih, bind_pure_comp, unattach_cons]
 
 @[wf_preprocess] theorem flatMapM_wfParam [Monad m] [LawfulMonad m]
     {xs : List α} {f : α → m (List β)} :
diff --git a/src/Init/Data/List/Nat/Modify.lean b/src/Init/Data/List/Nat/Modify.lean
index 2d9523c492..3ec310af81 100644
--- a/src/Init/Data/List/Nat/Modify.lean
+++ b/src/Init/Data/List/Nat/Modify.lean
@@ -148,7 +148,7 @@ theorem modifyTailIdx_modifyTailIdx_self {f g : List α → List α} (i : Nat) (
     (a :: l).modify 0 f = f a :: l := rfl
 
 @[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (i) :
-    (a :: l).modify (i + 1) f = a :: l.modify i f := by rfl
+    (a :: l).modify (i + 1) f = a :: l.modify i f := rfl
 
 theorem modifyHead_eq_modify_zero (f : α → α) (l : List α) :
     l.modifyHead f = l.modify 0 f := by cases l <;> simp
diff --git a/src/Init/Data/List/Pairwise.lean b/src/Init/Data/List/Pairwise.lean
index 46fec42cd3..4b69097155 100644
--- a/src/Init/Data/List/Pairwise.lean
+++ b/src/Init/Data/List/Pairwise.lean
@@ -254,7 +254,7 @@ theorem pairwise_pmap {p : β → Prop} {f : ∀ b, p b → α} {l : List β} (h
   | nil => simp
   | cons a l ihl =>
     obtain ⟨_, hl⟩ : p a ∧ ∀ b, b ∈ l → p b := by simpa using h
-    simp only [ihl hl, pairwise_cons, exists₂_imp, pmap, and_congr_left_iff, mem_pmap]
+    simp only [pmap_cons, pairwise_cons, mem_pmap, forall_exists_index, ihl hl, and_congr_left_iff]
     refine fun _ => ⟨fun H b hb _ hpb => H _ _ hb rfl, ?_⟩
     rintro H _ b hb rfl
     exact H b hb _ _
diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean
index 42190d524a..c76d7d0813 100644
--- a/src/Init/Data/List/Perm.lean
+++ b/src/Init/Data/List/Perm.lean
@@ -9,6 +9,7 @@ prelude
 import Init.Data.List.Pairwise
 import Init.Data.List.Erase
 import Init.Data.List.Find
+import all Init.Data.List.Attach
 
 /-!
 # List Permutations
diff --git a/src/Init/Data/List/Sort/Impl.lean b/src/Init/Data/List/Sort/Impl.lean
index f26c4e7617..c7b69d4986 100644
--- a/src/Init/Data/List/Sort/Impl.lean
+++ b/src/Init/Data/List/Sort/Impl.lean
@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.List.Sort.Basic
 import Init.Data.List.Sort.Lemmas
 
 /-!
diff --git a/src/Init/Data/List/Sort/Lemmas.lean b/src/Init/Data/List/Sort/Lemmas.lean
index 89565e4450..8847c3be5b 100644
--- a/src/Init/Data/List/Sort/Lemmas.lean
+++ b/src/Init/Data/List/Sort/Lemmas.lean
@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.List.Perm
-import Init.Data.List.Sort.Basic
+import all Init.Data.List.Sort.Basic
 import Init.Data.List.Nat.Range
 import Init.Data.Bool
 
diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean
index 54961416b6..81d737cee9 100644
--- a/src/Init/Data/List/TakeDrop.lean
+++ b/src/Init/Data/List/TakeDrop.lean
@@ -6,6 +6,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 module
 
 prelude
+import all Init.Data.List.Basic
 import Init.Data.List.Lemmas
 
 /-!
@@ -241,7 +242,7 @@ theorem dropLast_eq_take {l : List α} : l.dropLast = l.take (l.length - 1) := b
     ∀ {l : List α} {i : Nat}, (l.take i).map f = (l.map f).take i
   | [], i => by simp
   | _, 0 => by simp
-  | _ :: tl, n + 1 => by dsimp; rw [map_take]
+  | _ :: tl, n + 1 => by simp [map_take]
 
 @[simp] theorem map_drop {f : α → β} :
     ∀ {l : List α} {i : Nat}, (l.drop i).map f = (l.map f).drop i
diff --git a/src/Init/Data/List/ToArray.lean b/src/Init/Data/List/ToArray.lean
index 7167e399c1..70aa5ebb7b 100644
--- a/src/Init/Data/List/ToArray.lean
+++ b/src/Init/Data/List/ToArray.lean
@@ -6,11 +6,14 @@ Authors: Mario Carneiro
 module
 
 prelude
+import all Init.Data.List.Control
 import Init.Data.List.Impl
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Monadic
 import Init.Data.List.Nat.InsertIdx
 import Init.Data.Array.Lex.Basic
+import all Init.Data.Array.Basic
+import all Init.Data.Array.Set
 
 /-! ### Lemmas about `List.toArray`.
 
diff --git a/src/Init/Data/Nat/Basic.lean b/src/Init/Data/Nat/Basic.lean
index cb1e3b991b..1e051d25e2 100644
--- a/src/Init/Data/Nat/Basic.lean
+++ b/src/Init/Data/Nat/Basic.lean
@@ -57,7 +57,7 @@ Examples:
 * `Nat.repeat f 3 a = f <| f <| f <| a`
 * `Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"`
 -/
-@[specialize] def repeat {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α
+@[specialize, expose] def repeat {α : Type u} (f : α → α) : (n : Nat) → (a : α) → α
   | 0,      a => a
   | succ n, a => f (repeat f n a)
 
@@ -89,7 +89,7 @@ Examples:
  * `Nat.blt 5 2 = false`
  * `Nat.blt 5 5 = false`
 -/
-def blt (a b : Nat) : Bool :=
+@[expose] def blt (a b : Nat) : Bool :=
   ble a.succ b
 
 attribute [simp] Nat.zero_le
diff --git a/src/Init/Data/Nat/Bitwise/Lemmas.lean b/src/Init/Data/Nat/Bitwise/Lemmas.lean
index 9848363464..55a2c71de9 100644
--- a/src/Init/Data/Nat/Bitwise/Lemmas.lean
+++ b/src/Init/Data/Nat/Bitwise/Lemmas.lean
@@ -9,7 +9,7 @@ module
 prelude
 import Init.Data.Bool
 import Init.Data.Int.Pow
-import Init.Data.Nat.Bitwise.Basic
+import all Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.Lemmas
 import Init.Data.Nat.Simproc
 import Init.TacticsExtra
diff --git a/src/Init/Data/Nat/Compare.lean b/src/Init/Data/Nat/Compare.lean
index d72b8d5879..693a528cec 100644
--- a/src/Init/Data/Nat/Compare.lean
+++ b/src/Init/Data/Nat/Compare.lean
@@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
 module
 
 prelude
-import Init.Data.Ord
+import all Init.Data.Ord
 
 /-! # Basic lemmas about comparing natural numbers
 
diff --git a/src/Init/Data/Nat/Div/Basic.lean b/src/Init/Data/Nat/Div/Basic.lean
index 8ff23086ec..c8a3361f91 100644
--- a/src/Init/Data/Nat/Div/Basic.lean
+++ b/src/Init/Data/Nat/Div/Basic.lean
@@ -10,6 +10,8 @@ import Init.WF
 import Init.WFTactics
 import Init.Data.Nat.Basic
 
+@[expose] section
+
 namespace Nat
 
 /--
diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean
index cf8bcc5b4c..76a4a92aeb 100644
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -6,8 +6,9 @@ Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro, Floris van Doorn
 module
 
 prelude
+import all Init.Data.Nat.Bitwise.Basic
 import Init.Data.Nat.MinMax
-import Init.Data.Nat.Log2
+import all Init.Data.Nat.Log2
 import Init.Data.Nat.Power2
 import Init.Data.Nat.Mod
 
diff --git a/src/Init/Data/Nat/Linear.lean b/src/Init/Data/Nat/Linear.lean
index 0771c84227..1c9861ecc9 100644
--- a/src/Init/Data/Nat/Linear.lean
+++ b/src/Init/Data/Nat/Linear.lean
@@ -10,6 +10,8 @@ import Init.ByCases
 import Init.Data.Prod
 import Init.Data.RArray
 
+@[expose] section
+
 namespace Nat.Linear
 
 /-!
@@ -255,15 +257,8 @@ theorem Poly.denote_cons (ctx : Context) (k : Nat) (v : Var) (p : Poly) : denote
 
 attribute [local simp] Poly.denote_cons
 
-theorem Poly.denote_reverseAux (ctx : Context) (p q : Poly) : denote ctx (List.reverseAux p q) = denote ctx (p ++ q) := by
-  match p with
-  | [] => simp [List.reverseAux]
-  | (k, v) :: p => simp [List.reverseAux, denote_reverseAux]
-
-attribute [local simp] Poly.denote_reverseAux
-
 theorem Poly.denote_reverse (ctx : Context) (p : Poly) : denote ctx (List.reverse p) = denote ctx p := by
-  simp [List.reverse]
+  induction p <;> simp [*]
 
 attribute [local simp] Poly.denote_reverse
 
diff --git a/src/Init/Data/Option/Attach.lean b/src/Init/Data/Option/Attach.lean
index 6b9a2f9daf..8b71a9062b 100644
--- a/src/Init/Data/Option/Attach.lean
+++ b/src/Init/Data/Option/Attach.lean
@@ -136,11 +136,11 @@ theorem mem_attach : ∀ (o : Option α) (x : {x // o = some x}), x ∈ o.attach
 
 theorem toList_attach (o : Option α) :
     o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by
-  cases o <;> simp
+  cases o <;> simp [toList]
 
 @[simp, grind =] theorem attach_toList (o : Option α) :
     o.toList.attach = (o.attach.map fun ⟨a, h⟩ => ⟨a, by simpa using h⟩).toList := by
-  cases o <;> simp
+  cases o <;> simp [toList]
 
 theorem attach_map {o : Option α} (f : α → β) :
     (o.map f).attach = o.attach.map (fun ⟨x, h⟩ => ⟨f x, map_eq_some_iff.2 ⟨_, h, rfl⟩⟩) := by
@@ -193,7 +193,7 @@ theorem attach_filter {o : Option α} {p : α → Bool} :
   cases o with
   | none => simp
   | some a =>
-    simp only [filter_some, attach_some]
+    simp only [Option.filter, attach_some]
     ext
     simp only [attach_eq_some_iff, ite_none_right_eq_some, some.injEq, bind_some,
       dite_none_right_eq_some]
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index 377a8bdba4..68cd76c9ba 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -8,6 +8,8 @@ module
 prelude
 import Init.Control.Basic
 
+@[expose] section
+
 namespace Option
 
 deriving instance DecidableEq for Option
diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean
index 46a7c4c2ce..fdafd99911 100644
--- a/src/Init/Data/Option/Lemmas.lean
+++ b/src/Init/Data/Option/Lemmas.lean
@@ -6,8 +6,8 @@ Authors: Mario Carneiro
 module
 
 prelude
-import Init.Data.Option.BasicAux
-import Init.Data.Option.Instances
+import all Init.Data.Option.BasicAux
+import all Init.Data.Option.Instances
 import Init.Data.BEq
 import Init.Classical
 import Init.Ext
@@ -1047,8 +1047,8 @@ theorem pmap_eq_map (p : α → Prop) (f : α → β) (o : Option α) (H) :
 theorem pmap_or {p : α → Prop} {f : ∀ (a : α), p a → β} {o o' : Option α} {h} :
     (or o o').pmap f h =
       match o with
-      | none => o'.pmap f (fun a h' => h a h')
-      | some a => some (f a (h a rfl)) := by
+      | none => o'.pmap f (fun a h' => h a (by simp [h']))
+      | some a => some (f a (h a (by simp))) := by
   cases o <;> simp
 
 theorem pmap_pred_congr {α : Type u}
diff --git a/src/Init/Data/Option/List.lean b/src/Init/Data/Option/List.lean
index 2ea2bbfded..07bb828a32 100644
--- a/src/Init/Data/Option/List.lean
+++ b/src/Init/Data/Option/List.lean
@@ -7,6 +7,8 @@ module
 
 prelude
 import Init.Data.List.Lemmas
+import all Init.Data.List.Control
+import all Init.Data.Option.Instances
 
 namespace Option
 
diff --git a/src/Init/Data/Option/Monadic.lean b/src/Init/Data/Option/Monadic.lean
index 6d1ccc95f5..ff8cf88ef2 100644
--- a/src/Init/Data/Option/Monadic.lean
+++ b/src/Init/Data/Option/Monadic.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 
+import all Init.Data.Option.Instances
 import Init.Data.Option.Attach
 import Init.Control.Lawful.Basic
 
@@ -39,7 +40,7 @@ namespace Option
   rw [map_eq_pure_bind]
   congr
   funext x
-  split <;> rfl
+  split <;> simp
 
 @[simp, grind] theorem forIn_none [Monad m] (b : β) (f : α → β → m (ForInStep β)) :
     forIn none b f = pure b := by
@@ -51,7 +52,7 @@ namespace Option
   rw [map_eq_pure_bind]
   congr
   funext x
-  split <;> rfl
+  split <;> simp
 
 @[congr] theorem forIn'_congr [Monad m] [LawfulMonad m] {as bs : Option α} (w : as = bs)
     {b b' : β} (hb : b = b')
diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index 378c08c893..4948f3db0e 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -10,7 +10,7 @@ prelude
 import Init.Data.String.Basic
 import Init.Data.Array.Basic
 import Init.Data.SInt.Basic
-import Init.Data.Vector.Basic
+import all Init.Data.Vector.Basic
 
 /--
 The result of a comparison according to a total order.
@@ -768,7 +768,7 @@ def lexOrd [Ord α] [Ord β] : Ord (α × β) where
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare` is
 `Ordering.lt`.
 -/
-def ltOfOrd [Ord α] : LT α where
+@[expose] def ltOfOrd [Ord α] : LT α where
   lt a b := compare a b = Ordering.lt
 
 instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
@@ -778,7 +778,7 @@ instance [Ord α] : DecidableRel (@LT.lt α ltOfOrd) :=
 Constructs an `LT` instance from an `Ord` instance that asserts that the result of `compare`
 satisfies `Ordering.isLE`.
 -/
-def leOfOrd [Ord α] : LE α where
+@[expose] def leOfOrd [Ord α] : LE α where
   le a b := (compare a b).isLE
 
 instance [Ord α] : DecidableRel (@LE.le α leOfOrd) :=
@@ -795,7 +795,7 @@ protected def toBEq (ord : Ord α) : BEq α where
 /--
 Constructs an `LT` instance from an `Ord` instance.
 -/
-protected def toLT (ord : Ord α) : LT α :=
+@[expose] protected def toLT (ord : Ord α) : LT α :=
   ltOfOrd
 
 instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
@@ -804,7 +804,7 @@ instance [i : Ord α] : DecidableRel (@LT.lt _ (Ord.toLT i)) :=
 /--
 Constructs an `LE` instance from an `Ord` instance.
 -/
-protected def toLE (ord : Ord α) : LE α :=
+@[expose] protected def toLE (ord : Ord α) : LE α :=
   leOfOrd
 
 instance [i : Ord α] : DecidableRel (@LE.le _ (Ord.toLE i)) :=
diff --git a/src/Init/Data/RArray.lean b/src/Init/Data/RArray.lean
index 9df883e6ac..f82cda43dc 100644
--- a/src/Init/Data/RArray.lean
+++ b/src/Init/Data/RArray.lean
@@ -9,6 +9,8 @@ module
 prelude
 import Init.PropLemmas
 
+@[expose] section
+
 namespace Lean
 
 /--
diff --git a/src/Init/Data/Range/Lemmas.lean b/src/Init/Data/Range/Lemmas.lean
index cb81db818a..3dcbae4197 100644
--- a/src/Init/Data/Range/Lemmas.lean
+++ b/src/Init/Data/Range/Lemmas.lean
@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Range.Basic
+import all Init.Data.Range.Basic
 import Init.Data.List.Range
 import Init.Data.List.Monadic
 import Init.Data.Nat.Div.Lemmas
diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index d461c8bf09..dff6d0fe9b 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -211,7 +211,7 @@ private def reprArray : Array String := Id.run do
   List.range 128 |>.map (·.toUSize.repr) |> Array.mk
 
 private def reprFast (n : Nat) : String :=
-  if h : n < 128 then Nat.reprArray.getInternal n h else
+  if h : n < Nat.reprArray.size then Nat.reprArray.getInternal n h else
   if h : n < USize.size then (USize.ofNatLT n h).repr
   else (toDigits 10 n).asString
 
diff --git a/src/Init/Data/SInt/Bitwise.lean b/src/Init/Data/SInt/Bitwise.lean
index b45b56dc95..db3c998b73 100644
--- a/src/Init/Data/SInt/Bitwise.lean
+++ b/src/Init/Data/SInt/Bitwise.lean
@@ -6,7 +6,11 @@ Authors: Markus Himmel
 module
 
 prelude
+import all Init.Data.UInt.Basic
 import Init.Data.UInt.Bitwise
+import all Init.Data.BitVec.Basic
+import all Init.Data.BitVec.Lemmas
+import all Init.Data.SInt.Basic
 import Init.Data.SInt.Lemmas
 
 set_option hygiene false in
diff --git a/src/Init/Data/SInt/Lemmas.lean b/src/Init/Data/SInt/Lemmas.lean
index ffe040a0a9..ee1b1a63cc 100644
--- a/src/Init/Data/SInt/Lemmas.lean
+++ b/src/Init/Data/SInt/Lemmas.lean
@@ -6,9 +6,13 @@ Authors: Markus Himmel
 module
 
 prelude
-import Init.Data.SInt.Basic
+import all Init.Data.Nat.Bitwise.Basic
+import all Init.Data.SInt.Basic
+import all Init.Data.BitVec.Basic
 import Init.Data.BitVec.Bitblast
+import all Init.Data.BitVec.Lemmas
 import Init.Data.Int.LemmasAux
+import all Init.Data.UInt.Basic
 import Init.Data.UInt.Lemmas
 import Init.System.Platform
 
@@ -1455,16 +1459,16 @@ theorem ISize.toInt64_ofIntLE {n : Int} (h₁ h₂) :
   ISize.toInt64_ofNat' (by rw [toInt_maxValue]; cases System.Platform.numBits_eq <;> simp_all <;> omega)
 
 @[simp] theorem Int8.ofIntLE_bitVecToInt (n : BitVec 8) :
-    Int8.ofIntLE n.toInt n.le_toInt n.toInt_le = Int8.ofBitVec n :=
+    Int8.ofIntLE n.toInt (by exact n.le_toInt) (by exact n.toInt_le) = Int8.ofBitVec n :=
   Int8.toBitVec.inj (by simp)
 @[simp] theorem Int16.ofIntLE_bitVecToInt (n : BitVec 16) :
-    Int16.ofIntLE n.toInt n.le_toInt n.toInt_le = Int16.ofBitVec n :=
+    Int16.ofIntLE n.toInt (by exact n.le_toInt) (by exact n.toInt_le) = Int16.ofBitVec n :=
   Int16.toBitVec.inj (by simp)
 @[simp] theorem Int32.ofIntLE_bitVecToInt (n : BitVec 32) :
-    Int32.ofIntLE n.toInt n.le_toInt n.toInt_le = Int32.ofBitVec n :=
+    Int32.ofIntLE n.toInt (by exact n.le_toInt) (by exact n.toInt_le) = Int32.ofBitVec n :=
   Int32.toBitVec.inj (by simp)
 @[simp] theorem Int64.ofIntLE_bitVecToInt (n : BitVec 64) :
-    Int64.ofIntLE n.toInt n.le_toInt n.toInt_le = Int64.ofBitVec n :=
+    Int64.ofIntLE n.toInt (by exact n.le_toInt) (by exact n.toInt_le) = Int64.ofBitVec n :=
   Int64.toBitVec.inj (by simp)
 @[simp] theorem ISize.ofIntLE_bitVecToInt (n : BitVec System.Platform.numBits) :
     ISize.ofIntLE n.toInt (toInt_minValue ▸ n.le_toInt)
diff --git a/src/Init/Data/String/Basic.lean b/src/Init/Data/String/Basic.lean
index a48b5c2ac6..b9ecafff36 100644
--- a/src/Init/Data/String/Basic.lean
+++ b/src/Init/Data/String/Basic.lean
@@ -41,7 +41,7 @@ Non-strict inequality on strings, typically used via the `≤` operator.
 
 `a ≤ b` is defined to mean `¬ b < a`.
 -/
-@[reducible] protected def le (a b : String) : Prop := ¬ b < a
+@[expose, reducible] protected def le (a b : String) : Prop := ¬ b < a
 
 instance : LE String :=
   ⟨String.le⟩
diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
index 6104d9bd17..196990ee78 100644
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -6,7 +6,8 @@ Author: Leonardo de Moura
 module
 
 prelude
-import Init.Data.ByteArray
+import all Init.Data.ByteArray.Basic
+import all Init.Data.String.Basic
 import Init.Data.UInt.Lemmas
 
 namespace String
diff --git a/src/Init/Data/Sum/Lemmas.lean b/src/Init/Data/Sum/Lemmas.lean
index 9235fffebc..73064b8db0 100644
--- a/src/Init/Data/Sum/Lemmas.lean
+++ b/src/Init/Data/Sum/Lemmas.lean
@@ -6,7 +6,7 @@ Authors: Mario Carneiro, Yury G. Kudryashov
 module
 
 prelude
-import Init.Data.Sum.Basic
+import all Init.Data.Sum.Basic
 import Init.Ext
 
 /-!
diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean
index 801e9c5f70..c41c39ba40 100644
--- a/src/Init/Data/UInt/Basic.lean
+++ b/src/Init/Data/UInt/Basic.lean
@@ -567,12 +567,14 @@ protected def UInt32.shiftRight (a b : UInt32) : UInt32 := ⟨a.toBitVec >>> (UI
 Strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
 natural numbers. Usually accessed via the `<` operator.
 -/
-protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
+-- These need to be exposed as `Init.Prelude` already has an instance for bootstrapping puproses and
+-- they should be defeq
+@[expose] protected def UInt32.lt (a b : UInt32) : Prop := a.toBitVec < b.toBitVec
 /--
 Non-strict inequality of 32-bit unsigned integers, defined as inequality of the corresponding
 natural numbers. Usually accessed via the `≤` operator.
 -/
-protected def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
+@[expose] protected def UInt32.le (a b : UInt32) : Prop := a.toBitVec ≤ b.toBitVec
 
 instance : Add UInt32       := ⟨UInt32.add⟩
 instance : Sub UInt32       := ⟨UInt32.sub⟩
diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean
index f8096c1cc5..d469c03b16 100644
--- a/src/Init/Data/UInt/BasicAux.lean
+++ b/src/Init/Data/UInt/BasicAux.lean
@@ -9,6 +9,8 @@ prelude
 import Init.Data.Fin.Basic
 import Init.Data.BitVec.BasicAux
 
+@[expose] section
+
 set_option linter.missingDocs true
 
 /-!
diff --git a/src/Init/Data/UInt/Bitwise.lean b/src/Init/Data/UInt/Bitwise.lean
index de644ce49e..a9db699480 100644
--- a/src/Init/Data/UInt/Bitwise.lean
+++ b/src/Init/Data/UInt/Bitwise.lean
@@ -6,6 +6,8 @@ Authors: Markus Himmel, Mac Malone
 module
 
 prelude
+import all Init.Data.BitVec.Basic
+import all Init.Data.UInt.Basic
 import Init.Data.UInt.Lemmas
 import Init.Data.Fin.Bitwise
 
diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean
index 84e29067d6..fdadef52b0 100644
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -6,9 +6,12 @@ Authors: Leonardo de Moura, François G. Dorais, Mario Carneiro, Mac Malone, Mar
 module
 
 prelude
-import Init.Data.UInt.Basic
+import all Init.Data.UInt.Basic
+import all Init.Data.UInt.BasicAux
 import Init.Data.Fin.Lemmas
-import Init.Data.Fin.Bitwise
+import all Init.Data.Fin.Bitwise
+import all Init.Data.BitVec.Basic
+import all Init.Data.BitVec.BasicAux
 import Init.Data.BitVec.Lemmas
 import Init.Data.BitVec.Bitblast
 import Init.Data.Nat.Div.Lemmas
@@ -434,17 +437,17 @@ theorem USize.size_dvd_uInt64Size : USize.size ∣ UInt64.size := by cases USize
 
 @[simp] theorem UInt32.toUInt64_mod_4294967296 (n : UInt32) : n.toUInt64 % 4294967296 = n.toUInt64 := UInt64.toNat.inj (by simp)
 
-@[simp] theorem Fin.mk_uInt8ToNat (n : UInt8) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
-@[simp] theorem Fin.mk_uInt16ToNat (n : UInt16) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
-@[simp] theorem Fin.mk_uInt32ToNat (n : UInt32) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
-@[simp] theorem Fin.mk_uInt64ToNat (n : UInt64) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
-@[simp] theorem Fin.mk_uSizeToNat (n : USize) : Fin.mk n.toNat n.toFin.isLt = n.toFin := rfl
+@[simp] theorem Fin.mk_uInt8ToNat (n : UInt8) : Fin.mk n.toNat (by exact n.toFin.isLt) = n.toFin := rfl
+@[simp] theorem Fin.mk_uInt16ToNat (n : UInt16) : Fin.mk n.toNat (by exact n.toFin.isLt) = n.toFin := rfl
+@[simp] theorem Fin.mk_uInt32ToNat (n : UInt32) : Fin.mk n.toNat (by exact n.toFin.isLt) = n.toFin := rfl
+@[simp] theorem Fin.mk_uInt64ToNat (n : UInt64) : Fin.mk n.toNat (by exact n.toFin.isLt) = n.toFin := rfl
+@[simp] theorem Fin.mk_uSizeToNat (n : USize) : Fin.mk n.toNat (by exact n.toFin.isLt) = n.toFin := rfl
 
-@[simp] theorem BitVec.ofNatLT_uInt8ToNat (n : UInt8) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
-@[simp] theorem BitVec.ofNatLT_uInt16ToNat (n : UInt16) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
-@[simp] theorem BitVec.ofNatLT_uInt32ToNat (n : UInt32) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
-@[simp] theorem BitVec.ofNatLT_uInt64ToNat (n : UInt64) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
-@[simp] theorem BitVec.ofNatLT_uSizeToNat (n : USize) : BitVec.ofNatLT n.toNat n.toFin.isLt = n.toBitVec := rfl
+@[simp] theorem BitVec.ofNatLT_uInt8ToNat (n : UInt8) : BitVec.ofNatLT n.toNat (by exact n.toFin.isLt) = n.toBitVec := rfl
+@[simp] theorem BitVec.ofNatLT_uInt16ToNat (n : UInt16) : BitVec.ofNatLT n.toNat (by exact n.toFin.isLt) = n.toBitVec := rfl
+@[simp] theorem BitVec.ofNatLT_uInt32ToNat (n : UInt32) : BitVec.ofNatLT n.toNat (by exact n.toFin.isLt) = n.toBitVec := rfl
+@[simp] theorem BitVec.ofNatLT_uInt64ToNat (n : UInt64) : BitVec.ofNatLT n.toNat (by exact n.toFin.isLt) = n.toBitVec := rfl
+@[simp] theorem BitVec.ofNatLT_uSizeToNat (n : USize) : BitVec.ofNatLT n.toNat (by exact n.toFin.isLt) = n.toBitVec := rfl
 
 @[simp] theorem BitVec.ofFin_uInt8ToFin (n : UInt8) : BitVec.ofFin n.toFin = n.toBitVec := rfl
 @[simp] theorem BitVec.ofFin_uInt16ToFin (n : UInt16) : BitVec.ofFin n.toFin = n.toBitVec := rfl
diff --git a/src/Init/Data/Vector/Attach.lean b/src/Init/Data/Vector/Attach.lean
index f00db1eda0..7634318acb 100644
--- a/src/Init/Data/Vector/Attach.lean
+++ b/src/Init/Data/Vector/Attach.lean
@@ -7,7 +7,7 @@ module
 
 prelude
 import Init.Data.Vector.Lemmas
-import Init.Data.Array.Attach
+import all Init.Data.Array.Attach
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index b481cc7616..68b4454ee5 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -71,7 +71,7 @@ def elimAsList {motive : Vector α n → Sort u}
   | ⟨⟨xs⟩, ha⟩ => mk xs ha
 
 /-- Make an empty vector with pre-allocated capacity. -/
-@[inline] def emptyWithCapacity (capacity : Nat) : Vector α 0 := ⟨.mkEmpty capacity, rfl⟩
+@[inline] def emptyWithCapacity (capacity : Nat) : Vector α 0 := ⟨.emptyWithCapacity capacity, by simp⟩
 
 @[deprecated emptyWithCapacity (since := "2025-03-12"), inherit_doc emptyWithCapacity]
 abbrev mkEmpty := @emptyWithCapacity
diff --git a/src/Init/Data/Vector/Count.lean b/src/Init/Data/Vector/Count.lean
index c3cf4e002a..9f4d15ef7d 100644
--- a/src/Init/Data/Vector/Count.lean
+++ b/src/Init/Data/Vector/Count.lean
@@ -6,7 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Array.Count
+import all Init.Data.Array.Count
+import all Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
 
 /-!
diff --git a/src/Init/Data/Vector/Find.lean b/src/Init/Data/Vector/Find.lean
index 9ace879a79..09a329543f 100644
--- a/src/Init/Data/Vector/Find.lean
+++ b/src/Init/Data/Vector/Find.lean
@@ -6,6 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
+import all Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
 import Init.Data.Vector.Attach
 import Init.Data.Vector.Range
diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean
index f4bbe7d6b9..4acb3c832d 100644
--- a/src/Init/Data/Vector/Lemmas.lean
+++ b/src/Init/Data/Vector/Lemmas.lean
@@ -6,7 +6,8 @@ Authors: Shreyas Srinivas, Francois Dorais, Kim Morrison
 module
 
 prelude
-import Init.Data.Vector.Basic
+import all Init.Data.Array.Basic
+import all Init.Data.Vector.Basic
 import Init.Data.Array.Attach
 import Init.Data.Array.Find
 
@@ -651,12 +652,12 @@ theorem toList_swap {xs : Vector α n} {i j} (hi hj) :
   simp
 
 @[simp] theorem finIdxOf?_toList [BEq α] {a : α} {xs : Vector α n} :
-    xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast xs.size_toArray.symm) := by
+    xs.toList.finIdxOf? a = (xs.finIdxOf? a).map (Fin.cast (by exact xs.size_toArray.symm)) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
 @[simp] theorem findFinIdx?_toList {p : α → Bool} {xs : Vector α n} :
-    xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast xs.size_toArray.symm) := by
+    xs.toList.findFinIdx? p = (xs.findFinIdx? p).map (Fin.cast (by exact xs.size_toArray.symm)) := by
   rcases xs with ⟨xs, rfl⟩
   simp
 
diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean
index df09759e6e..c89a50b3d0 100644
--- a/src/Init/Data/Vector/Lex.lean
+++ b/src/Init/Data/Vector/Lex.lean
@@ -6,8 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Data.Vector.Basic
+import all Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
+import all Init.Data.Array.Lex.Basic
 import Init.Data.Array.Lex.Lemmas
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
diff --git a/src/Init/Data/Vector/MapIdx.lean b/src/Init/Data/Vector/MapIdx.lean
index 54640cef11..2dd4b7b9bd 100644
--- a/src/Init/Data/Vector/MapIdx.lean
+++ b/src/Init/Data/Vector/MapIdx.lean
@@ -7,6 +7,8 @@ module
 
 prelude
 import Init.Data.Array.MapIdx
+import all Init.Data.Array.Basic
+import all Init.Data.Vector.Basic
 import Init.Data.Vector.Attach
 import Init.Data.Vector.Lemmas
 
diff --git a/src/Init/Data/Vector/Monadic.lean b/src/Init/Data/Vector/Monadic.lean
index 9805a7b4df..24df9338dd 100644
--- a/src/Init/Data/Vector/Monadic.lean
+++ b/src/Init/Data/Vector/Monadic.lean
@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
 import Init.Data.Vector.Attach
 import Init.Data.Array.Monadic
diff --git a/src/Init/Data/Vector/OfFn.lean b/src/Init/Data/Vector/OfFn.lean
index 02bc7cd8df..ed8d96f957 100644
--- a/src/Init/Data/Vector/OfFn.lean
+++ b/src/Init/Data/Vector/OfFn.lean
@@ -6,6 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
 import Init.Data.Array.OfFn
 
diff --git a/src/Init/Data/Vector/Perm.lean b/src/Init/Data/Vector/Perm.lean
index beb0592ab2..7e8f9f6852 100644
--- a/src/Init/Data/Vector/Perm.lean
+++ b/src/Init/Data/Vector/Perm.lean
@@ -6,7 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Perm
+import all Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
 
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
diff --git a/src/Init/Data/Vector/Range.lean b/src/Init/Data/Vector/Range.lean
index 14dea9bc37..362ac1008f 100644
--- a/src/Init/Data/Vector/Range.lean
+++ b/src/Init/Data/Vector/Range.lean
@@ -6,6 +6,8 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
+import all Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
 import Init.Data.Vector.Zip
 import Init.Data.Vector.MapIdx
@@ -78,7 +80,7 @@ theorem range'_append {s m n step : Nat} :
     range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1)
 
 theorem range'_concat {s n : Nat} : range' s (n + 1) step = range' s n step ++ #v[s + step * n] := by
-  simpa using range'_append.symm
+  simp [← range'_append]
 
 theorem range'_1_concat {s n : Nat} : range' s (n + 1) = range' s n ++ #v[s + n] := by
   simp [range'_concat]
diff --git a/src/Init/Data/Vector/Zip.lean b/src/Init/Data/Vector/Zip.lean
index 6c54433105..b3349b1ec6 100644
--- a/src/Init/Data/Vector/Zip.lean
+++ b/src/Init/Data/Vector/Zip.lean
@@ -6,7 +6,9 @@ Authors: Kim Morrison
 module
 
 prelude
+import all Init.Data.Array.Basic
 import Init.Data.Array.Zip
+import all Init.Data.Vector.Basic
 import Init.Data.Vector.Lemmas
 
 /-!
diff --git a/src/Init/Dynamic.lean b/src/Init/Dynamic.lean
index d02295a105..1451eee40d 100644
--- a/src/Init/Dynamic.lean
+++ b/src/Init/Dynamic.lean
@@ -67,7 +67,7 @@ value from `Dynamic` if it has some expected type.
 -/
 def Dynamic : Type := DynamicPointed.type
 
-instance : Nonempty Dynamic := DynamicPointed.property
+instance : Nonempty Dynamic := by exact DynamicPointed.property
 
 private unsafe def Dynamic.typeNameImpl (any : Dynamic) : Name :=
   (unsafeCast any : Name × NonScalar).1
diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean
index f069139a22..bdaf5fe17c 100644
--- a/src/Init/GetElem.lean
+++ b/src/Init/GetElem.lean
@@ -8,6 +8,8 @@ module
 prelude
 import Init.Util
 
+@[expose] section
+
 @[never_extract]
 def outOfBounds [Inhabited α] : α :=
   panic! "index out of bounds"
@@ -224,7 +226,7 @@ instance [GetElem? cont Nat elem dom] [h : LawfulGetElem cont Nat elem dom] :
 @[simp] theorem getElem_fin [GetElem Cont Nat Elem Dom] (a : Cont) (i : Fin n) (h : Dom a i) :
     a[i] = a[i.1] := rfl
 
-@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[i.1]? := by rfl
+@[simp] theorem getElem?_fin [h : GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) : a[i]? = a[i.1]? := rfl
 
 @[simp] theorem getElem!_fin [GetElem? Cont Nat Elem Dom] (a : Cont) (i : Fin n) [Inhabited Elem] : a[i]! = a[i.1]! := rfl
 
diff --git a/src/Init/Grind/CommRing/BitVec.lean b/src/Init/Grind/CommRing/BitVec.lean
index e853c0fff5..24e6bf20bc 100644
--- a/src/Init/Grind/CommRing/BitVec.lean
+++ b/src/Init/Grind/CommRing/BitVec.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Grind.CommRing.Basic
+import all Init.Data.BitVec.Basic
 import Init.Data.BitVec.Lemmas
 
 namespace Lean.Grind
diff --git a/src/Init/Grind/CommRing/Fin.lean b/src/Init/Grind/CommRing/Fin.lean
index db81adcb76..3675b5a3b6 100644
--- a/src/Init/Grind/CommRing/Fin.lean
+++ b/src/Init/Grind/CommRing/Fin.lean
@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 module
 
 prelude
+import all Init.Data.Zero
 import Init.Grind.CommRing.Basic
 import Init.Data.Fin.Lemmas
 
@@ -96,8 +97,8 @@ instance (n : Nat) [NeZero n] : CommRing (Fin n) where
   mul_one := Fin.mul_one
   left_distrib := Fin.left_distrib
   zero_mul := Fin.zero_mul
-  pow_zero _ := rfl
-  pow_succ _ _ := rfl
+  pow_zero _ := by rfl
+  pow_succ _ _ := by rfl
   ofNat_succ := Fin.ofNat_succ
   sub_eq_add_neg := Fin.sub_eq_add_neg
   intCast_neg := Fin.intCast_neg
diff --git a/src/Init/Grind/CommRing/Int.lean b/src/Init/Grind/CommRing/Int.lean
index 915a50d18e..a79e911ff4 100644
--- a/src/Init/Grind/CommRing/Int.lean
+++ b/src/Init/Grind/CommRing/Int.lean
@@ -24,9 +24,9 @@ instance : CommRing Int where
   right_distrib := Int.add_mul
   zero_mul := Int.zero_mul
   mul_zero := Int.mul_zero
-  pow_zero _ := rfl
-  pow_succ _ _ := rfl
-  ofNat_succ _ := rfl
+  pow_zero _ := by rfl
+  pow_succ _ _ := by rfl
+  ofNat_succ _ := by rfl
   sub_eq_add_neg _ _ := Int.sub_eq_add_neg
 
 instance : IsCharP Int 0 where
diff --git a/src/Init/Grind/CommRing/Poly.lean b/src/Init/Grind/CommRing/Poly.lean
index 330c62ab21..8e5f873a61 100644
--- a/src/Init/Grind/CommRing/Poly.lean
+++ b/src/Init/Grind/CommRing/Poly.lean
@@ -8,7 +8,7 @@ module
 prelude
 import Init.Data.Nat.Lemmas
 import Init.Data.Hashable
-import Init.Data.Ord
+import all Init.Data.Ord
 import Init.Data.RArray
 import Init.Grind.CommRing.Basic
 
diff --git a/src/Init/Grind/CommRing/SInt.lean b/src/Init/Grind/CommRing/SInt.lean
index f004617e1f..f5bff29224 100644
--- a/src/Init/Grind/CommRing/SInt.lean
+++ b/src/Init/Grind/CommRing/SInt.lean
@@ -7,6 +7,8 @@ module
 
 prelude
 import Init.Grind.CommRing.Basic
+import all Init.Data.BitVec.Basic
+import all Init.Data.SInt.Basic
 import Init.Data.SInt.Lemmas
 
 namespace Lean.Grind
diff --git a/src/Init/Grind/CommRing/UInt.lean b/src/Init/Grind/CommRing/UInt.lean
index 691ed10d4f..4412d499a9 100644
--- a/src/Init/Grind/CommRing/UInt.lean
+++ b/src/Init/Grind/CommRing/UInt.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 import Init.Grind.CommRing.Basic
+import all Init.Data.UInt.Basic
 import Init.Data.UInt.Lemmas
 
 namespace UInt8
diff --git a/src/Init/Internal/Order/Basic.lean b/src/Init/Internal/Order/Basic.lean
index c085a67850..bb6409c400 100644
--- a/src/Init/Internal/Order/Basic.lean
+++ b/src/Init/Internal/Order/Basic.lean
@@ -9,6 +9,7 @@ prelude
 
 import Init.ByCases
 import Init.RCases
+import all Init.Control.Except  -- for `MonoBind` instance
 
 /-!
 This module contains some basic definitions and results from domain theory, intended to be used as
@@ -167,7 +168,7 @@ A function is monotone if it maps related elements to related elements.
 
 This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
-def monotone (f : α → β) : Prop := ∀ x y, x ⊑ y → f x ⊑ f y
+@[expose] def monotone (f : α → β) : Prop := ∀ x y, x ⊑ y → f x ⊑ f y
 
 theorem monotone_const (c : β) : monotone (fun (_ : α) => c) :=
   fun _ _ _ => PartialOrder.rel_refl
@@ -707,7 +708,7 @@ set_option linter.unusedVariables false in
 
 This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
-def FlatOrder {α : Sort u} (b : α) := α
+@[expose] def FlatOrder {α : Sort u} (b : α) := α
 
 variable {b : α}
 
@@ -842,7 +843,7 @@ end mono_bind
 
 section implication_order
 -- Partial order on `Prop` given by implication
-def ImplicationOrder := Prop
+@[expose] def ImplicationOrder := Prop
 
 instance ImplicationOrder.instOrder : PartialOrder ImplicationOrder where
   rel x y := x → y
@@ -897,7 +898,7 @@ end implication_order
 
 section reverse_implication_order
 
-def ReverseImplicationOrder := Prop
+@[expose] def ReverseImplicationOrder := Prop
 
 -- Partial order on `Prop` given by reverse implication
 instance ReverseImplicationOrder.instOrder : PartialOrder ReverseImplicationOrder where
diff --git a/src/Init/Internal/Order/Lemmas.lean b/src/Init/Internal/Order/Lemmas.lean
index 71b87b462e..20b3599619 100644
--- a/src/Init/Internal/Order/Lemmas.lean
+++ b/src/Init/Internal/Order/Lemmas.lean
@@ -8,8 +8,9 @@ module
 
 prelude
 
-import Init.Data.List.Control
-import Init.Data.Array.Basic
+import all Init.Data.List.Control
+import all Init.Data.Option.Basic
+import all Init.Data.Array.Basic
 import Init.Internal.Order.Basic
 
 /-!
diff --git a/src/Init/Omega/Coeffs.lean b/src/Init/Omega/Coeffs.lean
index c7f511cb84..b6edd70f62 100644
--- a/src/Init/Omega/Coeffs.lean
+++ b/src/Init/Omega/Coeffs.lean
@@ -6,7 +6,7 @@ Authors: Kim Morrison
 module
 
 prelude
-import Init.Omega.IntList
+import all Init.Omega.IntList
 
 /-!
 # `Coeffs` as a wrapper for `IntList`
diff --git a/src/Init/Omega/Constraint.lean b/src/Init/Omega/Constraint.lean
index 95add3f820..d8c1a74dce 100644
--- a/src/Init/Omega/Constraint.lean
+++ b/src/Init/Omega/Constraint.lean
@@ -14,6 +14,9 @@ A `Constraint` consists of an optional lower and upper bound (inclusive),
 constraining a value to a set of the form `∅`, `{x}`, `[x, y]`, `[x, ∞)`, `(-∞, y]`, or `(-∞, ∞)`.
 -/
 
+-- most defs used in proofs by reflection
+@[expose] section
+
 namespace Lean.Omega
 
 /-- An optional lower bound on a integer. -/
diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean
index 68ad776f29..d6539d97db 100644
--- a/src/Init/Omega/IntList.lean
+++ b/src/Init/Omega/IntList.lean
@@ -10,6 +10,8 @@ import Init.Data.List.Zip
 import Init.Data.Int.DivMod.Bootstrap
 import Init.Data.Nat.Gcd
 
+@[expose] section
+
 namespace Lean.Omega
 
 /--
diff --git a/src/Init/Omega/LinearCombo.lean b/src/Init/Omega/LinearCombo.lean
index e03d820efb..0a0f42b794 100644
--- a/src/Init/Omega/LinearCombo.lean
+++ b/src/Init/Omega/LinearCombo.lean
@@ -16,6 +16,9 @@ We use this data structure while processing hypotheses.
 
 -/
 
+-- most defs used in proofs by reflection
+@[expose] section
+
 namespace Lean.Omega
 
 /-- Internal representation of a linear combination of atoms, and a constant term. -/
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index 9cd2379d52..48027853b5 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -7,6 +7,7 @@ module
 
 prelude -- Don't import Init, because we're in Init itself
 set_option linter.missingDocs true -- keep it documented
+@[expose] section  -- Expose all defs
 
 /-!
 # Init.Prelude
@@ -70,7 +71,10 @@ despite the fact it is marked `irreducible`.
 For metaprogramming, the function `Lean.Expr.letFun?` can be used to recognize a `let_fun` expression
 to extract its parts as if it were a `let` expression.
 -/
-@[irreducible] def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) : β v := f v
+def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) : β v := f v
+-- We need to export the body of `letFun`, which is suppressed if `[irreducible]` is set directly.
+-- We can work around this rare case by applying the attribute after the fact.
+attribute [irreducible] letFun
 
 set_option checkBinderAnnotations false in
 /--
@@ -2758,7 +2762,7 @@ instance : Inhabited Substring where
 /--
 The number of bytes used by the string's UTF-8 encoding.
 -/
-@[inline] def Substring.bsize : Substring → Nat
+@[inline, expose] def Substring.bsize : Substring → Nat
   | ⟨_, b, e⟩ => e.byteIdx.sub b.byteIdx
 
 /--
@@ -5108,7 +5112,7 @@ private opaque MethodsRefPointed : NonemptyType.{0}
 
 private def MethodsRef : Type := MethodsRefPointed.type
 
-instance : Nonempty MethodsRef := MethodsRefPointed.property
+private instance : Nonempty MethodsRef := MethodsRefPointed.property
 
 /-- The read-only context for the `MacroM` monad. -/
 structure Context where
diff --git a/src/Init/PropLemmas.lean b/src/Init/PropLemmas.lean
index 0f925e5b08..85b1d278ce 100644
--- a/src/Init/PropLemmas.lean
+++ b/src/Init/PropLemmas.lean
@@ -598,7 +598,7 @@ and `decide` will not work. -/
 
 /-- Transfer decidability of `b` to decidability of `a`, if the propositions are equivalent.
 This is the same as `decidable_of_iff` but the iff is flipped. -/
-@[inline] def decidable_of_iff' (b : Prop) (h : a ↔ b) [Decidable b] : Decidable a :=
+@[inline, expose] def decidable_of_iff' (b : Prop) (h : a ↔ b) [Decidable b] : Decidable a :=
   decidable_of_decidable_of_iff h.symm
 
 instance Decidable.predToBool (p : α → Prop) [DecidablePred p] :
diff --git a/src/Init/SizeOfLemmas.lean b/src/Init/SizeOfLemmas.lean
index 9e67080a3e..3a07463454 100644
--- a/src/Init/SizeOfLemmas.lean
+++ b/src/Init/SizeOfLemmas.lean
@@ -6,8 +6,9 @@ Authors: Leonardo de Moura
 module
 
 prelude
+import all Init.Data.Char.Basic
 import Init.Meta
-import Init.SizeOf
+import all Init.SizeOf
 import Init.Data.Nat.Linear
 
 @[simp] protected theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1 := by
diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index cf4dfeea1f..7680af1a4d 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -37,7 +37,7 @@ A monad that can have side effects on the external world or throw exceptions of
    def getWorld : IO (IO.RealWorld) := get
    ```
 -/
-def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld
+@[expose] def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld
 
 instance : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))
 instance : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EStateM ε IO.RealWorld))
@@ -48,7 +48,7 @@ instance [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (E
 /--
 An `IO` monad that cannot throw exceptions.
 -/
-def BaseIO := EIO Empty
+@[expose] def BaseIO := EIO Empty
 
 instance : Monad BaseIO := inferInstanceAs (Monad (EIO Empty))
 instance : MonadFinally BaseIO := inferInstanceAs (MonadFinally (EIO Empty))
diff --git a/src/Init/System/Mutex.lean b/src/Init/System/Mutex.lean
index e383e48aac..fdcff97926 100644
--- a/src/Init/System/Mutex.lean
+++ b/src/Init/System/Mutex.lean
@@ -24,7 +24,7 @@ If you want to guard shared state, use `Mutex α` instead.
 @[deprecated "Use Std.BaseMutex from Std.Sync.Mutex instead" (since := "2024-12-02")]
 def BaseMutex : Type := BaseMutexImpl.type
 
-instance : Nonempty BaseMutex := BaseMutexImpl.property
+instance : Nonempty BaseMutex := by exact BaseMutexImpl.property
 
 /-- Creates a new `BaseMutex`. -/
 @[extern "lean_io_basemutex_new", deprecated "Use Std.BaseMutex.new from Std.Sync.Mutex instead" (since := "2024-12-02")]
@@ -54,7 +54,7 @@ private opaque CondvarImpl : NonemptyType.{0}
 @[deprecated "Use Std.Condvar from Std.Sync.Mutex instead" (since := "2024-12-02")]
 def Condvar : Type := CondvarImpl.type
 
-instance : Nonempty Condvar := CondvarImpl.property
+instance : Nonempty Condvar := by exact CondvarImpl.property
 
 /-- Creates a new condition variable. -/
 @[extern "lean_io_condvar_new", deprecated "Use Std.Condvar.new from Std.Sync.Mutex instead" (since := "2024-12-02")]
diff --git a/src/Init/System/Promise.lean b/src/Init/System/Promise.lean
index 15d37e3445..59c97351b8 100644
--- a/src/Init/System/Promise.lean
+++ b/src/Init/System/Promise.lean
@@ -34,7 +34,7 @@ See `Promise.result!/resultD` for other ways to handle this case.
 def Promise (α : Type) : Type := PromiseImpl α
 
 instance [s : Nonempty α] : Nonempty (Promise α) :=
-  Nonempty.intro { prom := Classical.choice PromisePointed.property, h := s }
+  by exact Nonempty.intro { prom := Classical.choice PromisePointed.property, h := s }
 
 /-- Creates a new `Promise`. -/
 @[extern "lean_io_promise_new"]
diff --git a/src/Init/System/ST.lean b/src/Init/System/ST.lean
index c8a317c3c0..3f16e86ddb 100644
--- a/src/Init/System/ST.lean
+++ b/src/Init/System/ST.lean
@@ -15,7 +15,7 @@ A restricted version of `IO` in which mutable state and exceptions are the only
 
 It is possible to run `EST` computations in a non-monadic context using `runEST`.
 -/
-def EST (ε : Type) (σ : Type) : Type → Type := EStateM ε σ
+@[expose] def EST (ε : Type) (σ : Type) : Type → Type := EStateM ε σ
 
 /--
 A restricted version of `IO` in which mutable state is the only side effect.
diff --git a/src/Init/Util.lean b/src/Init/Util.lean
index 69ba0eecfb..e47a87f436 100644
--- a/src/Init/Util.lean
+++ b/src/Init/Util.lean
@@ -35,13 +35,13 @@ def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
 @[noinline] private def mkPanicMessage (modName : String) (line col : Nat) (msg : String) : String :=
   "PANIC at " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
 
-@[never_extract, inline] def panicWithPos {α : Sort u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=
+@[never_extract, inline, expose] def panicWithPos {α : Sort u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=
   panic (mkPanicMessage modName line col msg)
 
-@[noinline] private def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
+@[noinline, expose] private def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
   "PANIC at " ++ declName ++ " " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
 
-@[never_extract, inline] def panicWithPosWithDecl {α : Sort u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α :=
+@[never_extract, inline, expose] def panicWithPosWithDecl {α : Sort u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α :=
   panic (mkPanicMessageWithDecl modName declName line col msg)
 
 /--
diff --git a/src/Init/WF.lean b/src/Init/WF.lean
index e9cc7cfa08..e16ff3475c 100644
--- a/src/Init/WF.lean
+++ b/src/Init/WF.lean
@@ -10,6 +10,8 @@ import Init.SizeOf
 import Init.BinderNameHint
 import Init.Data.Nat.Basic
 
+@[expose] section
+
 universe u v
 
 /--
diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index ad172ed588..3c5306dbcc 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -90,7 +90,6 @@ def addDecl (decl : Declaration) : CoreM Unit := do
   -- convert `Declaration` to `ConstantInfo` to use as a preliminary value in the environment until
   -- kernel checking has finished; not all cases are supported yet
   let mut exportedInfo? := none
-  let mut exportedKind? := none
   let (name, info, kind) ← match decl with
     | .thmDecl thm =>
       let exportProof := !(← getEnv).header.isModule ||
@@ -101,21 +100,23 @@ def addDecl (decl : Declaration) : CoreM Unit := do
         looksLikeRelevantTheoremProofType thm.type
       if !exportProof then
         exportedInfo? := some <| .axiomInfo { thm with isUnsafe := false }
-        exportedKind? := some .axiom
       pure (thm.name, .thmInfo thm, .thm)
-    | .defnDecl defn => pure (defn.name, .defnInfo defn, .defn)
-    | .mutualDefnDecl [defn] => pure (defn.name, .defnInfo defn, .defn)
+    | .defnDecl defn | .mutualDefnDecl [defn] =>
+      if (← getEnv).header.isModule && !(← getEnv).isExporting then
+        exportedInfo? := some <| .axiomInfo { defn with isUnsafe := defn.safety == .unsafe }
+      pure (defn.name, .defnInfo defn, .defn)
     | .axiomDecl ax => pure (ax.name, .axiomInfo ax, .axiom)
     | _ => return (← addSynchronously)
 
   -- preserve original constant kind in extension if different from exported one
-  if exportedKind?.isSome then
+  if exportedInfo?.isSome then
     modifyEnv (privateConstKindsExt.insert · name kind)
 
   -- no environment extension changes to report after kernel checking; ensures we do not
   -- accidentally wait for this snapshot when querying extension states
   let env ← getEnv
-  let async ← env.addConstAsync (reportExts := false) name kind (exportedKind?.getD kind)
+  let async ← env.addConstAsync (reportExts := false) name kind
+    (exportedKind := exportedInfo?.map (.ofConstantInfo) |>.getD kind)
   -- report preliminary constant info immediately
   async.commitConst async.asyncEnv (some info) exportedInfo?
   setEnv async.mainEnv
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 1df5cf852c..f025e85a16 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/src/Lean/Elab/BuiltinCommand.lean
@@ -540,4 +540,10 @@ where
           lines := lines.push cmd
     return if lines.isEmpty then none else MessageData.joinSep lines.toList "\n"
 
+@[builtin_command_elab Parser.Command.withExporting] def elabWithExporting : CommandElab
+  | `(Parser.Command.withExporting| #with_exporting $cmd) =>
+    withExporting do
+      elabCommand cmd
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Command
diff --git a/src/Lean/Elab/ComputedFields.lean b/src/Lean/Elab/ComputedFields.lean
index 8194b8cca6..47f9de4006 100644
--- a/src/Lean/Elab/ComputedFields.lean
+++ b/src/Lean/Elab/ComputedFields.lean
@@ -125,8 +125,11 @@ def overrideConstructors : M Unit := do
   for ctor in ctors do
     forallTelescope (← inferType (mkAppN (mkConst ctor lparams) params)) fun fields retTy => do
     let ctorTerm := mkAppN (mkConst ctor lparams) (params ++ fields)
-    let computedFieldVals ← if ← isScalarField ctor then pure #[] else
-      compFields.mapM (getComputedFieldValue · ctorTerm)
+    let computedFieldVals ←
+      -- elaborating a non-exposed def body
+      withoutExporting do
+        if ← isScalarField ctor then pure #[] else
+          compFields.mapM (getComputedFieldValue · ctorTerm)
     addDecl <| .defnDecl {
       name := ctor ++ `_override
       levelParams
@@ -146,13 +149,16 @@ def overrideComputedFields : M Unit := do
     if isExtern (← getEnv) cfn then
       compileDecls [cfn]
       continue
-    let cases ← ctors.toArray.mapM fun ctor => do
-      forallTelescope (← inferType (mkAppN (mkConst ctor lparams) params)) fun fields _ => do
-      if ← isScalarField ctor then
-        mkLambdaFVars fields <|
-          ← getComputedFieldValue cfn (mkAppN (mkConst ctor lparams) (params ++ fields))
-      else
-        mkLambdaFVars (compFieldVars ++ fields) cf
+    let cases ←
+      -- elaborating a non-exposed def body
+      withoutExporting do
+        ctors.toArray.mapM fun ctor => do
+          forallTelescope (← inferType (mkAppN (mkConst ctor lparams) params)) fun fields _ => do
+            if ← isScalarField ctor then
+              mkLambdaFVars fields <|
+                ← getComputedFieldValue cfn (mkAppN (mkConst ctor lparams) (params ++ fields))
+            else
+              mkLambdaFVars (compFieldVars ++ fields) cf
     addDecl <| .defnDecl {
       name := cfn ++ `_override
       levelParams
diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index 5e9cb3cc5b..981fa71f3e 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -101,9 +101,9 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do
     body ← mkLet letDecls body
   let binders    := header.binders
   if ctx.usePartial then
-    `(private partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term)
+    `(partial def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term)
   else
-    `(private def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term)
+    `(@[expose] def $(mkIdent auxFunName):ident $binders:bracketedBinder* : Bool := $body:term)
 
 def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
   let mut auxDefs := #[]
@@ -122,7 +122,7 @@ private def mkBEqInstanceCmds (declName : Name) : TermElabM (Array Syntax) := do
 
 private def mkBEqEnumFun (ctx : Context) (name : Name) : TermElabM Syntax := do
   let auxFunName := ctx.auxFunNames[0]!
-  `(private def $(mkIdent auxFunName):ident  (x y : $(mkIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx)
+  `(@[expose] def $(mkIdent auxFunName):ident  (x y : $(mkIdent name)) : Bool := x.toCtorIdx == y.toCtorIdx)
 
 private def mkBEqEnumCmd (name : Name): TermElabM (Array Syntax) := do
   let ctx ← mkContext "beq" name
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 3e453c8703..8bdca7cc25 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -24,16 +24,12 @@ open Language
 
 builtin_initialize
   registerTraceClass `Meta.instantiateMVars
-
-private builtin_initialize exposeAttr : TagAttribute ←
-  registerTagAttribute
-    `expose
-    "(module system) Make bodies of definitions available to importing modules."
-    (validate := fun c => do
-      if let some info := (← getEnv).setExporting false |>.findAsync? c then
-        if info.kind == .defn then
-          return
-      throwError "Invalid use of `expose` attribute, it can only be used on definitions")
+  registerBuiltinAttribute {
+    name := `expose
+    descr := "(module system) Make bodies of definitions available to importing modules."
+    add := fun _ _ _ => do
+      throwError "Invalid attribute 'expose', must be used when declaring `def`"
+  }
 
 def instantiateMVarsProfiling (e : Expr) : MetaM Expr := do
   profileitM Exception s!"instantiate metavars" (← getOptions) do
@@ -1094,8 +1090,7 @@ where
         try
           isDefEq lhs rhs
         catch _ => pure false
-    withExporting (isExporting := rflPublic) do
-      finishElab headers
+    finishElab (isExporting := rflPublic) headers
     processDeriving headers
   elabAsync header view declId := do
     let env ← getEnv
@@ -1138,8 +1133,7 @@ where
         (cancelTk? := cancelTk) fun _ => do profileitM Exception "elaboration" (← getOptions) do
       setEnv async.asyncEnv
       try
-        withoutExporting do
-          finishElab #[header]
+        finishElab (isExporting := false) #[header]
       finally
         reportDiag
         -- must introduce node to fill `infoHole` with multiple info trees
@@ -1157,7 +1151,14 @@ where
     Core.logSnapshotTask { stx? := none, task := (← BaseIO.asTask (act ())), cancelTk? := cancelTk }
     applyAttributesAt declId.declName view.modifiers.attrs .afterTypeChecking
     applyAttributesAt declId.declName view.modifiers.attrs .afterCompilation
-  finishElab headers := withFunLocalDecls headers fun funFVars => do
+  finishElab headers (isExporting := false) := withFunLocalDecls headers fun funFVars => withExporting
+    (isExporting := isExporting ||
+      (headers.all (·.kind == .def) && sc.attrs.any (· matches `(attrInstance| expose))) ||
+      headers.all fun header =>
+        !header.modifiers.isPrivate &&
+        (header.kind matches .abbrev | .instance || header.modifiers.attrs.any (·.name == `expose))) do
+    let headers := headers.map fun header =>
+      { header with modifiers.attrs := header.modifiers.attrs.filter (·.name != `expose) }
     for view in views, funFVar in funFVars do
       addLocalVarInfo view.declId funFVar
     let values ← try
diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean
index 6a84822096..6f2935db77 100644
--- a/src/Lean/Elab/PreDefinition/WF/Fix.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -204,7 +204,9 @@ def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Arr
     r := r.modify funidx (·.push goal)
   return r
 
-def solveDecreasingGoals (funNames : Array Name) (argsPacker : ArgsPacker) (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr := do
+def solveDecreasingGoals (funNames : Array Name) (argsPacker : ArgsPacker) (decrTactics : Array (Option DecreasingBy)) (value : Expr) : MetaM Expr :=
+  -- entering proof
+  withoutExporting do
   let goals ← getMVarsNoDelayed value
   let goals ← assignSubsumed goals
   let goalss ← groupGoalsByFunction argsPacker decrTactics.size goals
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index 844ee13a04..1eda38b7aa 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -341,6 +341,11 @@ mutual
   If `report := false`, then `runTactic` will not capture exceptions nor will report unsolved goals. Unsolved goals become exceptions.
   -/
   partial def runTactic (mvarId : MVarId) (tacticCode : Syntax) (kind : TacticMVarKind) (report := true) : TermElabM Unit := withoutAutoBoundImplicit do
+    -- exit exporting context if entering proof
+    let isExporting ← pure (← getEnv).isExporting <&&> do
+      mvarId.withContext do
+        return !(← isProp (← mvarId.getType))
+    withExporting (isExporting := isExporting) do
     instantiateMVarDeclMVars mvarId
     /-
     TODO: consider using `runPendingTacticsAt` at `mvarId` local context and target type.
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 28ba80209e..7040effbdd 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -1815,22 +1815,66 @@ private def findOLeanParts (mod : Name) : IO (Array System.FilePath) := do
   return fnames
 
 partial def importModulesCore
-    (imports : Array Import) (forceImportAll := true) (arts : NameMap ModuleArtifacts := {}) :
-    ImportStateM Unit := go
-where go := do
+    (imports : Array Import) (isModule := false) (arts : NameMap ModuleArtifacts := {}) :
+    ImportStateM Unit := go imports (importAll := true) (isExported := isModule)
+/-
+When the module system is disabled for the root, we import all transitively referenced modules and
+ignore any module sytem annotations on the way.
+
+When the module system is enabled for the root, each module may need to be imported at one of the
+following levels:
+
+* all: import public information into public scope and private information into private scope
+* public: import public information into public scope
+* privateAll: import public and private information into private scope
+* private: import public information into private scope
+* none: do not import
+
+These levels form a lattice in the following way:
+
+* all > public > private > none
+* all > privateAll > private > none
+
+The level at which a module then is to be imported based on the given `import` relations is
+determined by the least fixed point of the following rules:
+
+* Root ≥ all
+* A ≥ privateAll ∧ A `(private)? import all` B → B ≥ privateAll
+* A ≥ private ∧ A `import (all)?` B → B ≥ private
+* A ≥ public ∧ A `import (all)?` B → B ≥ public
+* A ≥ privateAll ∧ A `private import` B → B ≥ private
+
+As imports are a DAG, we may need to visit the same module multiple times until its minimum
+necessary level is established.
+
+For implementation purposes, we represent elements in the lattice using two flags as follows:
+
+* all = isExported && importAll
+* privateAll = !isExported && importAll
+* private = !isExported && !importAll
+* public = isExported && !importAll
+
+`none` then is represented by not visiting a module at all.
+-/
+where go (imports : Array Import) (importAll : Bool) (isExported : Bool) := do
   for i in imports do
-    -- import private info if (transitively) used by a non-`module` on any import path, or with
-    -- `import all` (non-transitively)
-    let importAll := forceImportAll || i.importAll
+    -- `B = none`?
+    if !(i.isExported || importAll) then
+      continue
+    -- `B ≥ privateAll`?
+    let importAll := !isModule || (importAll && i.importAll)
+    -- `B ≥ public`?
+    let isExported := isExported && i.isExported
+    let goRec imports := do
+      go (importAll := importAll) (isExported := isExported) imports
     if let some mod := (← get).moduleNameMap[i.module]? then
-      -- when module is already imported, bump `importPrivate`
-      if importAll && !mod.importAll then
+      -- when module is already imported, bump flags
+      if importAll && !mod.importAll || isExported && !mod.isExported then
         modify fun s => { s with moduleNameMap := s.moduleNameMap.insert i.module { mod with
-          importAll := true }}
-        if forceImportAll then
-          -- bump entire closure
-          if let some mod := mod.mainModule? then
-            importModulesCore (forceImportAll := true) mod.imports
+          importAll, isExported }}
+        -- bump entire closure
+        if let some mod := mod.mainModule? then
+          goRec mod.imports
       continue
     let fnames ←
       if let some arts := arts.find? i.module then
@@ -1843,16 +1887,14 @@ where go := do
     let parts ← readModuleDataParts fnames
     -- `imports` is identical for each part
     let some (baseMod, _) := parts[0]? | unreachable!
-    -- exclude `private import`s from transitive importing, except through `import all`
-    let imports := baseMod.imports.filter (·.isExported || importAll)
-    importModulesCore (forceImportAll := forceImportAll || !baseMod.isModule) imports
-    if baseMod.isModule && !forceImportAll then
+    goRec baseMod.imports
+    if baseMod.isModule && isModule then
       for i' in imports do
         if let some mod := (← get).moduleNameMap[i'.module]?.bind (·.mainModule?) then
           if !mod.isModule then
             throw <| IO.userError s!"cannot import non`-module` {i'.module} from `module` {i.module}"
     modify fun s => { s with
-      moduleNameMap := s.moduleNameMap.insert i.module { i with importAll, parts }
+      moduleNameMap := s.moduleNameMap.insert i.module { i with importAll, isExported, parts }
       moduleNames := s.moduleNames.push i.module
     }
 
@@ -2018,7 +2060,7 @@ def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32
       throw <| IO.userError "import failed, trying to import module with anonymous name"
   withImporting do
     plugins.forM Lean.loadPlugin
-    let (_, s) ← importModulesCore (forceImportAll := level == .private) imports arts |>.run
+    let (_, s) ← importModulesCore (isModule := level != .private) imports arts |>.run
     finalizeImport (leakEnv := leakEnv) (loadExts := loadExts) (level := level)
       s imports opts trustLevel
 
diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index 2f2525a304..374e849ef3 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -284,7 +284,7 @@ structure SetupImportsResult where
   /-- Module name of the file being processed. -/
   mainModuleName : Name
   /-- Whether the file is participating in the module system. -/
-  isModule : Bool := false
+  isModule : Bool
   /-- Direct imports of the file being processed. -/
   imports : Array Import
   /-- Options provided outside of the file content, e.g. on the cmdline or in the lakefile. -/
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 1dcc55d9bd..9e5b7ed281 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -782,7 +782,9 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
       result.type result.value .abbrev)
     trace[Meta.Match.debug] "{name} : {result.type} := {result.value}"
     let addMatcher : MatcherInfo → MetaM Unit := fun mi => do
-      addDecl decl
+      -- matcher bodies should always be exported, if not private anyway
+      withExporting do
+        addDecl decl
       modifyEnv fun env => matcherExt.modifyState env fun s => s.insert (result.value, compile) name
       addMatcherInfo name mi
       setInlineAttribute name
diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
index b7f0c95747..b41aa132d1 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean
@@ -542,6 +542,10 @@ def SimpTheorems.unfoldEvenWithEqns (declName : Name) : CoreM Bool := do
   return false
 
 def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM SimpTheorems := do
+  -- NOTE: the latter condition is only to preserve previous behavior where simp accepts even things
+  -- that neither theorems nor unfoldable. This should likely be tightened up in the future.
+  if !(← getConstInfo declName).isDefinition && getOriginalConstKind? (← getEnv) declName == some .defn then
+    throwError "invalid 'simp', definition with exposed body expected: {.ofConstName declName}"
   if (← ignoreEquations declName) then
     return d.addDeclToUnfoldCore declName
   else if let some eqns ← getEqnsFor? declName then
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 4581d664a3..76f99c5f7c 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -517,6 +517,12 @@ and options set with `set_option`.
 /-- Shows the current Lean version. Prints `Lean.versionString`. -/
 @[builtin_command_parser] def version        := leading_parser
   "#version"
+/--
+Debugging command. Runs the following command in an exported context just like elaboration of
+declaration signatures.
+-/
+@[builtin_command_parser] def withExporting  := leading_parser
+  "#with_exporting " >> commandParser
 @[builtin_command_parser] def «init_quot»    := leading_parser
   "init_quot"
 def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit
diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 5984689812..5b9d28f64e 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -417,6 +417,7 @@ def setupImports
 
   return .ok {
     mainModuleName := meta.mod
+    isModule := Elab.HeaderSyntax.isModule stx
     imports
     opts
     plugins := fileSetupResult.plugins
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index ba121ba7a0..abebe4c08c 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -78,49 +78,57 @@
     tags: [fast]
   run_config:
     <<: *time
-    cmd: lean -Dexperimental.module=true ../../src/Init/Prelude.lean
+    cwd: ../../src
+    cmd: lean -Dexperimental.module=true Init/Prelude.lean
 - attributes:
     description: Init.Data.List.Sublist async
     tags: [fast]
   run_config:
     <<: *time
-    cmd: lean -Dexperimental.module=true ../../src/Init/Data/List/Sublist.lean
+    cwd: ../../src
+    cmd: lean -Dexperimental.module=true Init/Data/List/Sublist.lean
 - attributes:
     description: Std.Data.Internal.List.Associative
     tags: [fast]
   run_config:
     <<: *time
-    cmd: lean -Dexperimental.module=true ../../src/Std/Data/Internal/List/Associative.lean
+    cwd: ../../src
+    cmd: lean -Dexperimental.module=true Std/Data/Internal/List/Associative.lean
 - attributes:
     description: Std.Data.DHashMap.Internal.RawLemmas
     tags: [fast]
   run_config:
     <<: *time
-    cmd: lean -Dexperimental.module=true ../../src/Std/Data/DHashMap/Internal/RawLemmas.lean
+    cwd: ../../src
+    cmd: lean -Dexperimental.module=true Std/Data/DHashMap/Internal/RawLemmas.lean
 - attributes:
     description: Init.Data.BitVec.Lemmas
     tags: [fast]
   run_config:
     <<: *time
-    cmd: lean -Dexperimental.module=true ../../src/Init/Data/BitVec/Lemmas.lean
+    cwd: ../../src
+    cmd: lean -Dexperimental.module=true Init/Data/BitVec/Lemmas.lean
 - attributes:
     description: Init.Data.List.Sublist re-elab -j4
   run_config:
     <<: *time
-    cmd: lean --run ../../script/benchReelabRss.lean lean ../../src/Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true
+    cwd: ../../src
+    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/List/Sublist.lean 10 -j4 -Dexperimental.module=true
     max_runs: 2
 - attributes:
     description: Init.Data.BitVec.Lemmas re-elab
   run_config:
     <<: *time
-    cmd: lean --run ../../script/benchReelabRss.lean lean ../../src/Init/Data/BitVec/Lemmas.lean 2 -j4 -Dexperimental.module=true
+    cwd: ../../src
+    cmd: lean --run ../script/benchReelabRss.lean lean Init/Data/BitVec/Lemmas.lean 2 -j4 -Dexperimental.module=true
     max_runs: 2
 - attributes:
     description: import Lean
     tags: [fast]
   run_config:
     <<: *time
-    cmd: lean ../../src/Lean.lean
+    cwd: ../../src
+    cmd: lean Lean.lean
 - attributes:
     description: tests/compiler
     tags: [deterministic, slow]
diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean
index 4a74d8918a..e401762f33 100644
--- a/tests/pkg/module/Module/Basic.lean
+++ b/tests/pkg/module/Module/Basic.lean
@@ -9,3 +9,5 @@ def f := 1
 theorem t : f = 1 := sorry
 
 theorem trfl : f = 1 := rfl
+
+@[expose] def fexp := 1
diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean
index e612235e55..c7c475f512 100644
--- a/tests/pkg/module/Module/ImportedAll.lean
+++ b/tests/pkg/module/Module/ImportedAll.lean
@@ -1,9 +1,9 @@
 module
 
 prelude
-private import all Module.Basic
+import all Module.Basic
 
-/-! `import all` should uncover theorem bodies. -/
+/-! `import all` should import private information, privately. -/
 
 /--
 info: theorem t : f = 1 :=
@@ -11,3 +11,14 @@ sorry
 -/
 #guard_msgs in
 #print t
+
+/--
+error: type mismatch
+  y
+has type
+  Vector Unit 1 : Type
+but is expected to have type
+  Vector Unit f : Type
+-/
+#guard_msgs in
+theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := sorry
diff --git a/tests/pkg/module/Module/ImportedImportedAll.lean b/tests/pkg/module/Module/ImportedImportedAll.lean
new file mode 100644
index 0000000000..6a7da3d15b
--- /dev/null
+++ b/tests/pkg/module/Module/ImportedImportedAll.lean
@@ -0,0 +1,13 @@
+module
+
+prelude
+import Module.ImportedAll
+
+/-! `import all` should not transitively expose private info. -/
+
+/--
+info: def f : Nat :=
+<not imported>
+-/
+#guard_msgs in
+#print f
diff --git a/tests/pkg/module/Module/PrivateImported.lean b/tests/pkg/module/Module/PrivateImported.lean
index 388788e85a..e9a9cc791d 100644
--- a/tests/pkg/module/Module/PrivateImported.lean
+++ b/tests/pkg/module/Module/PrivateImported.lean
@@ -4,19 +4,13 @@ private import Module.Basic
 
 /-! `private import` should allow only private access to imported decls. -/
 
-/--
-error: type mismatch
-  f
-has type
-  Nat : Type
-but is expected to have type
-  True : Prop
--/
-#guard_msgs in
-theorem g : True := f
+def g := f
 
-/- FIXME: visibility for def bodies is wrong
 /-- error: unknown identifier 'f' -/
 #guard_msgs in
-@[reducible] def h : True := f
--/
+set_option autoImplicit false in
+theorem t2 : f = 1 := sorry
+
+/-- error: unknown identifier 'f' -/
+#guard_msgs in
+@[expose] def h : True := f