initial exploration for a ExtHashMapD

This PR corrects some `Array` lemmas to be about `Array` not `List`.

Discovered [on
Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/duplicate.20declarations/near/518942094)

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

src/CMakeLists.txt

@@ -689,7 +689,7 @@ add_custom_target(make_stdlib ALL
   # The actual rule is in a separate makefile because we want to prefix it with '+' to use the Make job server
   # for a parallelized nested build, but CMake doesn't let us do that.
   # We use `lean` from the previous stage, but `leanc`, headers, etc. from the current stage
-  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean
+  COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Init Std Lean Leanc
   VERBATIM)
 
 # if we have LLVM enabled, then build `lean.h.bc` which has the LLVM bitcode
@@ -768,7 +768,7 @@ if(${STAGE} GREATER 0 AND EXISTS ${LEAN_SOURCE_DIR}/Leanc.lean AND NOT ${CMAKE_S
   add_custom_target(leanc ALL
     WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/leanc
     DEPENDS leanshared
-    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make Leanc
+    COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make leanc
     VERBATIM)
 endif()
 
@@ -823,7 +823,6 @@ endif()
 
 # Escape for `make`. Yes, twice.
 string(REPLACE "$" "\\\$$" CMAKE_EXE_LINKER_FLAGS_MAKE "${CMAKE_EXE_LINKER_FLAGS}")
-string(REPLACE "$" "$$" CMAKE_EXE_LINKER_FLAGS_MAKE_MAKE "${CMAKE_EXE_LINKER_FLAGS_MAKE}")
 configure_file(${LEAN_SOURCE_DIR}/stdlib.make.in ${CMAKE_BINARY_DIR}/stdlib.make)
 
 # hacky

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

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 ε α)
 
 /--

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
 

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 :=

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

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 α)
 
 /--

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

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
 

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`. -/
 

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
 
 /--

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.

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.

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
 

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]

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
 

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

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

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

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

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?]

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
 
@@ -22,9 +23,9 @@ namespace Array
 @[simp, grind =] theorem lt_toList [LT α] {xs ys : Array α} : xs.toList < ys.toList ↔ xs < ys := Iff.rfl
 @[simp, grind =] theorem le_toList [LT α] {xs ys : Array α} : xs.toList ≤ ys.toList ↔ xs ≤ ys := Iff.rfl
 
-protected theorem not_lt_iff_ge [LT α] {l₁ l₂ : List α} : ¬ l₁ < l₂ ↔ l₂ ≤ l₁ := Iff.rfl
-protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {l₁ l₂ : List α} :
-    ¬ l₁ ≤ l₂ ↔ l₂ < l₁ :=
+protected theorem not_lt_iff_ge [LT α] {xs ys : Array α} : ¬ xs < ys ↔ ys ≤ xs := Iff.rfl
+protected theorem not_le_iff_gt [DecidableEq α] [LT α] [DecidableLT α] {xs ys : Array α} :
+    ¬ xs ≤ ys ↔ ys < xs :=
   Decidable.not_not
 
 @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by

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.

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

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
 
@@ -25,12 +26,11 @@ theorem ofFn_succ {f : Fin (n+1) → α} :
     ofFn f = (ofFn (fun (i : Fin n) => f i.castSucc)).push (f ⟨n, by omega⟩) := by
   ext i h₁ h₂
   · simp
-  · simp [getElem_push]
-    split <;> rename_i h₃
-    · rfl
-    · congr
-      simp at h₁ h₂
-      omega
+  · simp only [getElem_ofFn, getElem_push, size_ofFn, Fin.castSucc_mk, left_eq_dite_iff,
+      Nat.not_lt]
+    simp only [size_ofFn] at h₁
+    intro h₃
+    simp only [show i = n by omega]
 
 @[simp] theorem _root_.List.toArray_ofFn {f : Fin n → α} : (List.ofFn f).toArray = Array.ofFn f := by
   ext <;> simp

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.

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]

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
 
 /-

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
 

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
 

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
 

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

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

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
 
@@ -2260,7 +2261,7 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
   ext i
-  simp [getElem_sshiftRight, getLsbD_sshiftRight, Nat.add_assoc]
+  simp only [getElem_sshiftRight, Nat.add_assoc, msb_sshiftRight, dite_eq_ite]
   by_cases h₂ : n + i < w
   · simp [h₂]
   · simp only [h₂, ↓reduceIte]
@@ -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
@@ -3731,6 +3732,10 @@ theorem mul_add {x y z : BitVec w} :
   rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat),
     ← Nat.mul_mod, Nat.mul_add]
 
+theorem add_mul {x y z : BitVec w} :
+    (x + y) * z = x * z + y * z := by
+  rw [BitVec.mul_comm, mul_add, BitVec.mul_comm z, BitVec.mul_comm z]
+
 theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [mul_add]
 theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add]
 
@@ -4162,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} :
@@ -5345,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

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 -/

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
 

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
 

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⟩

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

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)⟩
 
 /--

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

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]

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
 

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

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

src/Init/Data/Int/DivMod/Basic.lean

@@ -8,6 +8,8 @@ module
 prelude
 import Init.Data.Int.Basic
 
+@[expose] section
+
 open Nat
 
 namespace Int

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

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
 

src/Init/Data/Int/Order.lean

@@ -166,6 +166,9 @@ protected theorem lt_or_le (a b : Int) : a < b ∨ b ≤ a := by rw [← Int.not
 protected theorem le_of_not_gt {a b : Int} (h : ¬ a > b) : a ≤ b :=
   Int.not_lt.mp h
 
+protected theorem not_lt_of_ge {a b : Int} (h : b ≤ a) : ¬a < b :=
+  Int.not_lt.mpr h
+
 protected theorem lt_trichotomy (a b : Int) : a < b ∨ a = b ∨ b < a :=
   if eq : a = b then .inr <| .inl eq else
   if le : a ≤ b then .inl <| Int.lt_iff_le_and_ne.2 ⟨le, eq⟩ else
@@ -1181,6 +1184,54 @@ protected theorem nonpos_of_mul_nonpos_right {a b : Int}
     (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0 :=
   Int.le_of_not_gt fun hb : b > 0 => Int.not_le_of_gt (Int.mul_pos ha hb) h
 
+protected theorem nonneg_of_mul_nonpos_left {a b : Int}
+    (h : a * b ≤ 0) (hb : b < 0) : 0 ≤ a :=
+  Int.le_of_not_gt fun ha => Int.not_le_of_gt (Int.mul_pos_of_neg_of_neg ha hb) h
+
+protected theorem nonneg_of_mul_nonpos_right {a b : Int}
+    (h : a * b ≤ 0) (ha : a < 0) : 0 ≤ b :=
+  Int.le_of_not_gt fun hb => Int.not_le_of_gt (Int.mul_pos_of_neg_of_neg ha hb) h
+
+protected theorem nonpos_of_mul_nonneg_left {a b : Int}
+    (h : 0 ≤ a * b) (hb : b < 0) : a ≤ 0 :=
+  Int.le_of_not_gt fun ha : a > 0 => Int.not_le_of_gt (Int.mul_neg_of_pos_of_neg ha hb) h
+
+protected theorem nonpos_of_mul_nonneg_right {a b : Int}
+    (h : 0 ≤ a * b) (ha : a < 0) : b ≤ 0 :=
+  Int.le_of_not_gt fun hb : b > 0 => Int.not_le_of_gt (Int.mul_neg_of_neg_of_pos ha hb) h
+
+protected theorem pos_of_mul_pos_left {a b : Int}
+    (h : 0 < a * b) (hb : 0 < b) : 0 < a :=
+  Int.lt_of_not_ge fun ha => Int.not_lt_of_ge (Int.mul_nonpos_of_nonpos_of_nonneg ha (Int.le_of_lt hb)) h
+
+protected theorem pos_of_mul_pos_right {a b : Int}
+    (h : 0 < a * b) (ha : 0 < a) : 0 < b :=
+  Int.lt_of_not_ge fun hb => Int.not_lt_of_ge (Int.mul_nonpos_of_nonneg_of_nonpos (Int.le_of_lt ha) hb) h
+
+protected theorem neg_of_mul_neg_left {a b : Int}
+    (h : a * b < 0) (hb : 0 < b) : a < 0 :=
+  Int.lt_of_not_ge fun ha => Int.not_lt_of_ge (Int.mul_nonneg ha (Int.le_of_lt hb)) h
+
+protected theorem neg_of_mul_neg_right {a b : Int}
+    (h : a * b < 0) (ha : 0 < a) : b < 0 :=
+  Int.lt_of_not_ge fun hb => Int.not_lt_of_ge (Int.mul_nonneg (Int.le_of_lt ha) hb) h
+
+protected theorem pos_of_mul_neg_left {a b : Int}
+    (h : a * b < 0) (hb : b < 0) : 0 < a :=
+  Int.lt_of_not_ge fun ha => Int.not_lt_of_ge (Int.mul_nonneg_of_nonpos_of_nonpos ha (Int.le_of_lt hb)) h
+
+protected theorem pos_of_mul_neg_right {a b : Int}
+    (h : a * b < 0) (ha : a < 0) : 0 < b :=
+  Int.lt_of_not_ge fun hb => Int.not_lt_of_ge (Int.mul_nonneg_of_nonpos_of_nonpos (Int.le_of_lt ha) hb) h
+
+protected theorem neg_of_mul_pos_left {a b : Int}
+    (h : 0 < a * b) (hb : b < 0) : a < 0 :=
+  Int.lt_of_not_ge fun ha => Int.not_lt_of_ge (Int.mul_nonpos_of_nonneg_of_nonpos ha (Int.le_of_lt hb)) h
+
+protected theorem neg_of_mul_pos_right {a b : Int}
+    (h : 0 < a * b) (ha : a < 0) : b < 0 :=
+  Int.lt_of_not_ge fun hb => Int.not_lt_of_ge (Int.mul_nonpos_of_nonpos_of_nonneg (Int.le_of_lt ha) hb) h
+
 /- ## sign -/
 
 @[simp] theorem sign_zero : sign 0 = 0 := rfl

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")]

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`.
 

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]

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

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]

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

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 β)} :

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

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 _ _

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

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
 
 /-!

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
 

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

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`.
 

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

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

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
 

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
 
 /--

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
 

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
 

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]

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

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}

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
 

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')

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.
@@ -88,7 +88,7 @@ Ordering.gt
 Ordering.lt
 ```
 -/
-@[macro_inline] def «then» (a b : Ordering) : Ordering :=
+@[macro_inline, expose] def «then» (a b : Ordering) : Ordering :=
   match a with
   | .eq => b
   | a => a
@@ -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)) :=

src/Init/Data/RArray.lean

@@ -9,6 +9,8 @@ module
 prelude
 import Init.PropLemmas
 
+@[expose] section
+
 namespace Lean
 
 /--

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

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
 

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

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)

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⟩

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

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
 
 /-!

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⟩

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
 
 /-!

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
 

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

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.

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

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
 
 /-!

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

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
 

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.

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
 

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

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
 

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.

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]

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
 
 /-!