diff --git a/.github/workflows/docs-release.yml b/.github/workflows/docs-release.yml
index 2926a31340..2c8a5c57f6 100644
--- a/.github/workflows/docs-release.yml
+++ b/.github/workflows/docs-release.yml
@@ -40,6 +40,8 @@ jobs:
       - name: Release Docs
         uses: softprops/action-gh-release@v2
         with:
+          prerelease: ${{ contains(github.ref, 'rc') }}
+          make_latest: ${{ !contains(github.ref, 'rc') }}
           files: |
             docs/docs-${{ github.ref_name }}.tar.gz
             docs/docs-${{ github.ref_name }}.zip
diff --git a/Batteries.lean b/Batteries.lean
index 6c24d239bc..f39cd3f6d6 100644
--- a/Batteries.lean
+++ b/Batteries.lean
@@ -93,7 +93,6 @@ import Batteries.Tactic.ShowUnused
 import Batteries.Tactic.SqueezeScope
 import Batteries.Tactic.Trans
 import Batteries.Tactic.Unreachable
-import Batteries.Tactic.Where
 import Batteries.Util.Cache
 import Batteries.Util.ExtendedBinder
 import Batteries.Util.LibraryNote
diff --git a/Batteries/Data/UInt.lean b/Batteries/Data/UInt.lean
index 3f9b495629..007a57d75d 100644
--- a/Batteries/Data/UInt.lean
+++ b/Batteries/Data/UInt.lean
@@ -10,11 +10,6 @@ import Batteries.Classes.Order
 @[ext] theorem UInt8.ext : {x y : UInt8} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt8.val_val_eq_toNat (x : UInt8) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt8.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt8).toNat = n % UInt8.size := rfl
-
 theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt
 
 @[simp] theorem UInt8.toUInt16_toNat (x : UInt8) : x.toUInt16.toNat = x.toNat := rfl
@@ -23,19 +18,6 @@ theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.val.isLt
 
 @[simp] theorem UInt8.toUInt64_toNat (x : UInt8) : x.toUInt64.toNat = x.toNat := rfl
 
-theorem UInt8.toNat_add (x y : UInt8) : (x + y).toNat = (x.toNat + y.toNat) % UInt8.size := rfl
-
-theorem UInt8.toNat_sub (x y : UInt8) :
-    (x - y).toNat = (UInt8.size - y.toNat + x.toNat) % UInt8.size := rfl
-
-theorem UInt8.toNat_mul (x y : UInt8) : (x * y).toNat = (x.toNat * y.toNat) % UInt8.size := rfl
-
-theorem UInt8.le_antisymm_iff {x y : UInt8} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt8.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt8.le_antisymm {x y : UInt8} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt8.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt8.le_antisymm
 
@@ -44,11 +26,6 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
 @[ext] theorem UInt16.ext : {x y : UInt16} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt16.val_val_eq_toNat (x : UInt16) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt16.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt16).toNat = n % UInt16.size := rfl
-
 theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt
 
 @[simp] theorem UInt16.toUInt8_toNat (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -57,19 +34,6 @@ theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.val.isLt
 
 @[simp] theorem UInt16.toUInt64_toNat (x : UInt16) : x.toUInt64.toNat = x.toNat := rfl
 
-theorem UInt16.toNat_add (x y : UInt16) : (x + y).toNat = (x.toNat + y.toNat) % UInt16.size := rfl
-
-theorem UInt16.toNat_sub (x y : UInt16) :
-    (x - y).toNat = (UInt16.size - y.toNat + x.toNat) % UInt16.size := rfl
-
-theorem UInt16.toNat_mul (x y : UInt16) : (x * y).toNat = (x.toNat * y.toNat) % UInt16.size := rfl
-
-theorem UInt16.le_antisymm_iff {x y : UInt16} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt16.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt16.le_antisymm {x y : UInt16} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt16.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt16.le_antisymm
 
@@ -78,11 +42,6 @@ instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
 @[ext] theorem UInt32.ext : {x y : UInt32} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt32.val_val_eq_toNat (x : UInt32) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt32.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt32).toNat = n % UInt32.size := rfl
-
 theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt
 
 @[simp] theorem UInt32.toUInt8_toNat (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -91,19 +50,6 @@ theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.val.isLt
 
 @[simp] theorem UInt32.toUInt64_toNat (x : UInt32) : x.toUInt64.toNat = x.toNat := rfl
 
-theorem UInt32.toNat_add (x y : UInt32) : (x + y).toNat = (x.toNat + y.toNat) % UInt32.size := rfl
-
-theorem UInt32.toNat_sub (x y : UInt32) :
-    (x - y).toNat = (UInt32.size - y.toNat + x.toNat) % UInt32.size := rfl
-
-theorem UInt32.toNat_mul (x y : UInt32) : (x * y).toNat = (x.toNat * y.toNat) % UInt32.size := rfl
-
-theorem UInt32.le_antisymm_iff {x y : UInt32} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt32.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt32.le_antisymm {x y : UInt32} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt32.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt32.le_antisymm
 
@@ -112,11 +58,6 @@ instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
 @[ext] theorem UInt64.ext : {x y : UInt64} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem UInt64.val_val_eq_toNat (x : UInt64) : x.val.val = x.toNat := rfl
-
-@[simp] theorem UInt64.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : UInt64).toNat = n % UInt64.size := rfl
-
 theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
 
 @[simp] theorem UInt64.toUInt8_toNat (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
@@ -125,19 +66,6 @@ theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.val.isLt
 
 @[simp] theorem UInt64.toUInt32_toNat (x : UInt64) : x.toUInt32.toNat = x.toNat % 2 ^ 32 := rfl
 
-theorem UInt64.toNat_add (x y : UInt64) : (x + y).toNat = (x.toNat + y.toNat) % UInt64.size := rfl
-
-theorem UInt64.toNat_sub (x y : UInt64) :
-    (x - y).toNat = (UInt64.size - y.toNat + x.toNat) % UInt64.size := rfl
-
-theorem UInt64.toNat_mul (x y : UInt64) : (x * y).toNat = (x.toNat * y.toNat) % UInt64.size := rfl
-
-theorem UInt64.le_antisymm_iff {x y : UInt64} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  UInt64.ext_iff.trans Nat.le_antisymm_iff
-
-theorem UInt64.le_antisymm {x y : UInt64} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  UInt64.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt UInt64.le_antisymm
 
@@ -146,11 +74,6 @@ instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
 @[ext] theorem USize.ext : {x y : USize} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-@[simp] theorem USize.val_val_eq_toNat (x : USize) : x.val.val = x.toNat := rfl
-
-@[simp] theorem USize.toNat_ofNat (n) :
-    (no_index (OfNat.ofNat n) : USize).toNat = n % USize.size := rfl
-
 theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by
   rw [USize.size]
 
@@ -172,18 +95,5 @@ theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits := by
 
 @[simp] theorem UInt32.toUSize_toNat (x : UInt32) : x.toUSize.toNat = x.toNat := rfl
 
-theorem USize.toNat_add (x y : USize) : (x + y).toNat = (x.toNat + y.toNat) % USize.size := rfl
-
-theorem USize.toNat_sub (x y : USize) :
-    (x - y).toNat = (USize.size - y.toNat + x.toNat) % USize.size := rfl
-
-theorem USize.toNat_mul (x y : USize) : (x * y).toNat = (x.toNat * y.toNat) % USize.size := rfl
-
-theorem USize.le_antisymm_iff {x y : USize} : x = y ↔ x ≤ y ∧ y ≤ x :=
-  USize.ext_iff.trans Nat.le_antisymm_iff
-
-theorem USize.le_antisymm {x y : USize} (h1 : x ≤ y) (h2 : y ≤ x) : x = y :=
-  USize.le_antisymm_iff.2 ⟨h1, h2⟩
-
 instance : Batteries.LawfulOrd USize := .compareOfLessAndEq
   (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt USize.le_antisymm
diff --git a/Batteries/Tactic/Where.lean b/Batteries/Tactic/Where.lean
deleted file mode 100644
index 3ef51a46c9..0000000000
--- a/Batteries/Tactic/Where.lean
+++ /dev/null
@@ -1,83 +0,0 @@
-/-
-Copyright (c) 2023 Kyle Miller. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller
--/
-import Lean.Elab.Command
-
-/-! # `#where` command
-
-The `#where` command prints information about the current location, including the namespace,
-active `open`, `universe`, and `variable` commands, and any options set with `set_option`.
--/
-
-open Lean Elab Command
-
-namespace Batteries.Tactic.Where
-
-private def describeOpenDecls (ds : List OpenDecl) : MessageData := Id.run do
-  let mut lines := #[]
-  let mut simple := #[]
-  let flush (lines simple : Array MessageData) : Array MessageData × Array MessageData :=
-    if simple.isEmpty then
-      (lines, simple)
-    else
-      (lines.push ("open " ++ MessageData.joinSep simple.toList " "), #[])
-  for d in ds do
-    match d with
-    | .explicit id decl =>
-      (lines, simple) := flush lines simple
-      lines := lines.push m!"open {id} → {decl}"
-    | .simple ns ex =>
-      if ex == [] then
-        simple := simple.push ns
-      else
-        (lines, simple) := flush lines simple
-        let ex' := ex.map toMessageData
-        lines := lines.push m!"open {ns} hiding {MessageData.joinSep ex' ", "}"
-  (lines, _) := flush lines simple
-  return MessageData.joinSep lines.toList "\n"
-
-private def describeOptions (opts : Options) : CommandElabM (Option MessageData) := do
-  let mut lines := #[]
-  let decls ← getOptionDecls
-  for (name, val) in opts do
-    match decls.find? name with
-    | some decl =>
-      if val != decl.defValue then
-        lines := lines.push m!"set_option {name} {val}"
-    | none =>
-      lines := lines.push m!"-- set_option {name} {val}  -- unknown"
-  if lines.isEmpty then
-    return none
-  else
-    return MessageData.joinSep lines.toList "\n"
-
-/-- `#where` gives a description of the global scope at this point in the module.
-This includes the namespace, `open` namespaces, `universe` and `variable` commands,
-and options set with `set_option`. -/
-elab "#where" : command => do
-  let scope ← getScope
-  let mut msg : Array MessageData := #[]
-  -- Noncomputable
-  if scope.isNoncomputable then
-    msg := msg.push m!"noncomputable section"
-  -- Namespace
-  if !scope.currNamespace.isAnonymous then
-    msg := msg.push m!"namespace {scope.currNamespace}"
-  -- Open namespaces
-  if !scope.openDecls.isEmpty then
-    msg := msg.push <| describeOpenDecls scope.openDecls.reverse
-  -- Universe levels
-  if !scope.levelNames.isEmpty then
-    let levels := scope.levelNames.reverse.map toMessageData
-    msg := msg.push <| "universe " ++ MessageData.joinSep levels " "
-  -- Variables
-  if !scope.varDecls.isEmpty then
-    msg := msg.push <| ← `(command| variable $scope.varDecls*)
-  -- Options
-  if let some m ← describeOptions scope.opts then
-    msg := msg.push m
-  if msg.isEmpty then
-    msg := #[m!"-- In root namespace with initial scope"]
-  logInfo <| m!"{MessageData.joinSep msg.toList "\n\n"}"
diff --git a/BatteriesTest/where.lean b/BatteriesTest/where.lean
index a88f1ed8e5..eb715d6ad6 100644
--- a/BatteriesTest/where.lean
+++ b/BatteriesTest/where.lean
@@ -1,4 +1,7 @@
-import Batteries.Tactic.Where
+-- None of these imports are really necessary, except to create namespace mentioned below.
+import Lean.Elab.Term
+import Lean.Elab.Command
+import Batteries.Data.UnionFind.Basic
 
 -- Return to pristine state
 set_option linter.missingDocs false
@@ -68,6 +71,6 @@ open Array renaming map -> listMap
 info: open Lean Lean.Meta
 open Lean.Elab hiding TermElabM
 open Lean.Elab.Command Batteries
-open listMap → Array.map
+open Array renaming map → listMap
 -/
 #guard_msgs in #where
diff --git a/README.md b/README.md
index e20b87c09f..36d46eee4d 100644
--- a/README.md
+++ b/README.md
@@ -13,7 +13,7 @@ Or add the following to your `lakefile.toml`:
 [[require]]
 name = "batteries"
 scope = "leanprover-community"
-version = "main"
+rev = "main"
 ```
 
 Additionally, please make sure that you're using the version of Lean that the current version of `batteries` expects. The easiest way to do this is to copy the [`lean-toolchain`](./lean-toolchain) file from this repository to your project. Once you've added the dependency declaration, the command `lake update` checks out the current version of `batteries` and writes it the Lake manifest file. Don't run this command again unless you're prepared to potentially also update your Lean compiler version, as it will retrieve the latest version of dependencies and add them to the manifest.