fix: MarkNestedProofs

feat: avoid cooper case analysis for univariate polynomials (#7351 )
This PR ensures cutsat does not have to perform case analysis in the univariate polynomial case. That it, it can close a goal whenever there is no solution for a divisibility constraint in an interval. Example of theorem that is now proved in a single step by cutsat: ```lean example (x : Int) : 100 ≤ x → x ≤ 10000 → 20000 ∣ 3*x → False := by grind ```
2026-04-11 22:54:17 +00:00 · 2025-03-05 16:27:31 -08:00 · 2025-03-05 20:37:29 +00:00 · 2025-03-05 18:15:49 +00:00 · 2025-03-05 17:58:58 +00:00 · 2025-03-05 17:12:27 +00:00
84 changed files with 940 additions and 208 deletions
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -47,10 +47,11 @@ if (NOT ${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
    if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
      string(APPEND CADICAL_CXXFLAGS " -DNUNLOCKED")
    endif()
+    string(APPEND CADICAL_CXXFLAGS " -DNCLOSEFROM")
    ExternalProject_add(cadical
      PREFIX cadical
      GIT_REPOSITORY https://github.com/arminbiere/cadical
-      GIT_TAG rel-1.9.5
+      GIT_TAG rel-2.1.2
      CONFIGURE_COMMAND ""
      # https://github.com/arminbiere/cadical/blob/master/BUILD.md#manual-build
      BUILD_COMMAND $(MAKE) -f ${CMAKE_SOURCE_DIR}/src/cadical.mk CMAKE_EXECUTABLE_SUFFIX=${CMAKE_EXECUTABLE_SUFFIX} CXX=${CADICAL_CXX} CXXFLAGS=${CADICAL_CXXFLAGS}
--- a/flake.lock
+++ b/flake.lock
@@ -36,17 +36,17 @@
    },
    "nixpkgs-cadical": {
      "locked": {
-        "lastModified": 1722221733,
-        "narHash": "sha256-sga9SrrPb+pQJxG1ttJfMPheZvDOxApFfwXCFO0H9xw=",
+        "lastModified": 1740791350,
+        "narHash": "sha256-igS2Z4tVw5W/x3lCZeeadt0vcU9fxtetZ/RyrqsCRQ0=",
        "owner": "NixOS",
        "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
+        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
        "type": "github"
      },
      "original": {
        "owner": "NixOS",
        "repo": "nixpkgs",
-        "rev": "12bf09802d77264e441f48e25459c10c93eada2e",
+        "rev": "199169a2135e6b864a888e89a2ace345703c025d",
        "type": "github"
      }
    },
--- a/flake.nix
+++ b/flake.nix
@@ -8,8 +8,8 @@
  # old nixpkgs used for portable release with older glibc (2.26)
  inputs.nixpkgs-older.url = "github:NixOS/nixpkgs/0b307aa73804bbd7a7172899e59ae0b8c347a62d";
  inputs.nixpkgs-older.flake = false;
-  # for cadical 1.9.5; sync with CMakeLists.txt
-  inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/12bf09802d77264e441f48e25459c10c93eada2e";
+  # for cadical 2.1.2; sync with CMakeLists.txt by taking commit from https://www.nixhub.io/packages/cadical
+  inputs.nixpkgs-cadical.url = "github:NixOS/nixpkgs/199169a2135e6b864a888e89a2ace345703c025d";
  inputs.flake-utils.url = "github:numtide/flake-utils";

  outputs = inputs: inputs.flake-utils.lib.eachDefaultSystem (system:
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -324,6 +324,9 @@ theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
@[simp, bitvec_to_nat] theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
  simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']

+theorem ofNatLT_eq_ofNat {w : Nat} {n : Nat} (hn) : BitVec.ofNatLT n hn = BitVec.ofNat w n :=
+  eq_of_toNat_eq (by simp [Nat.mod_eq_of_lt hn])
+
@[simp] theorem toFin_ofNat (x : Nat) : toFin (BitVec.ofNat w x) = Fin.ofNat' (2^w) x := rfl

 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -1473,6 +1473,115 @@ theorem cooper_right_split_dvd (ctx : Context) (p₁ p₂ : Poly) (k : Nat) (b :
  simp [cooper_right_split_dvd_cert, cooper_right_split]
  intros; subst b p'; simp; assumption

+private theorem one_emod_eq_one {a : Int} (h : a > 1) : 1 % a = 1 := by
+  have aux₁ := Int.ediv_add_emod 1 a
+  have : 1 / a = 0 := Int.ediv_eq_zero_of_lt (by decide) h
+  simp [this] at aux₁
+  assumption
+
+private theorem ex_of_dvd {α β a b d x : Int}
+    (h₀ : d > 1)
+    (h₁ : d ∣ a*x + b)
+    (h₂ : α * a + β * d = 1)
+    : ∃ k, x = k * d + (- α * b) % d := by
+  have ⟨k, h₁⟩ := h₁
+  have aux₁ : (α * a) % d = 1 := by
+    replace h₂ := congrArg (· % d) h₂; simp at h₂
+    rw [one_emod_eq_one h₀] at h₂
+    assumption
+  have : ((α * a) * x) % d = (- α * b) % d := by
+    replace h₁ := congrArg (α * ·) h₁; simp only at h₁
+    rw [Int.mul_add] at h₁
+    replace h₁ := congrArg (· - α * b) h₁; simp only [Int.add_sub_cancel] at h₁
+    rw [← Int.mul_assoc, Int.mul_left_comm, Int.sub_eq_add_neg] at h₁
+    replace h₁ := congrArg (· % d) h₁; simp only at h₁
+    rw [Int.add_emod, Int.mul_emod_right, Int.zero_add, Int.emod_emod, ← Int.neg_mul] at h₁
+    assumption
+  have : x % d = (- α * b) % d := by
+    rw [Int.mul_emod, aux₁, Int.one_mul, Int.emod_emod] at this
+    assumption
+  have : x = (x / d)*d + (- α * b) % d := by
+    conv => lhs; rw [← Int.ediv_add_emod x d]
+    rw [Int.mul_comm, this]
+  exists x / d
+
+private theorem cdiv_le {a d k : Int} : d > 0 → a ≤ k * d → cdiv a d ≤ k := by
+  intro h₁ h₂
+  simp [cdiv]
+  replace h₂ := Int.neg_le_neg h₂
+  rw [← Int.neg_mul] at h₂
+  replace h₂ := Int.le_ediv_of_mul_le h₁ h₂
+  replace h₂ := Int.neg_le_neg h₂
+  simp at h₂
+  assumption
+
+private theorem cooper_unsat'_helper {a b d c k x : Int}
+    (d_pos : d > 0)
+    (h₁ : x = k * d + c)
+    (h₂ : a ≤ x)
+    (h₃ : x ≤ b)
+    : ¬ b < (cdiv (a - c) d) * d + c := by
+  intro h₄
+  have aux₁ : cdiv (a - c) d ≤ k := by
+    rw [h₁] at h₂
+    replace h₂ := Int.sub_right_le_of_le_add h₂
+    exact cdiv_le d_pos h₂
+  have aux₂ : cdiv (a - c) d * d ≤ k * d := Int.mul_le_mul_of_nonneg_right aux₁ (Int.le_of_lt d_pos)
+  have aux₃ : cdiv (a - c) d * d + c ≤ k * d + c := Int.add_le_add_right aux₂ _
+  have aux₄ : cdiv (a - c) d * d + c ≤ x := by rw [←h₁] at aux₃; assumption
+  have aux₅ : cdiv (a - c) d * d + c ≤ b := Int.le_trans aux₄ h₃
+  have := Int.lt_of_le_of_lt aux₅ h₄
+  exact Int.lt_irrefl _ this
+
+private theorem cooper_unsat' {a c b d e α β x : Int}
+    (h₁ : d > 1)
+    (h₂ : d ∣ c*x + e)
+    (h₃ : α * c + β * d = 1)
+    (h₄ : (-1)*x + a ≤ 0)
+    (h₅ : x + b ≤ 0)
+    (h₆ : -b < cdiv (a - -α * e % d) d * d + -α * e % d)
+    : False := by
+  have ⟨k, h⟩ := ex_of_dvd h₁ h₂ h₃
+  have d_pos : d > 0 := Int.lt_trans (by decide) h₁
+  replace h₄ := Int.le_neg_add_of_add_le h₄; simp at h₄
+  replace h₅ := Int.neg_le_neg (Int.le_neg_add_of_add_le h₅); simp at h₅
+  have := cooper_unsat'_helper d_pos h h₄ h₅
+  exact this h₆
+
+abbrev Poly.casesOnAdd (p : Poly) (k : Int → Var → Poly → Bool) : Bool :=
+  p.casesOn (fun _  => false) k
+
+abbrev Poly.casesOnNum (p : Poly) (k : Int → Bool) : Bool :=
+  p.casesOn k (fun _ _ _ => false)
+
+def cooper_unsat_cert (p₁ p₂ p₃ : Poly) (d : Int) (α β : Int) : Bool :=
+  p₁.casesOnAdd fun k₁ x p₁ =>
+  p₂.casesOnAdd fun k₂ y p₂ =>
+  p₃.casesOnAdd fun c z p₃ =>
+  p₁.casesOnNum fun a =>
+  p₂.casesOnNum fun b =>
+  p₃.casesOnNum fun e =>
+  (k₁ == -1) |>.and (k₂ == 1) |>.and
+  (x == y) |>.and (x == z) |>.and
+  (d > 1) |>.and (α * c + β * d == 1) |>.and
+  (-b < cdiv (a - -α * e % d) d * d + -α * e % d)
+
+theorem cooper_unsat (ctx : Context) (p₁ p₂ p₃ : Poly) (d : Int) (α β : Int)
+   : cooper_unsat_cert p₁ p₂ p₃ d α β →
+     p₁.denote' ctx ≤ 0 → p₂.denote' ctx ≤ 0 → d ∣ p₃.denote' ctx → False := by
+  unfold cooper_unsat_cert <;> cases p₁ <;> cases p₂ <;> cases p₃ <;> simp only [Poly.casesOnAdd,
+    Bool.false_eq_true, Poly.denote'_add, mul_def, add_def, false_implies]
+  next k₁ x p₁ k₂ y p₂ c z p₃ =>
+  cases p₁ <;> cases p₂ <;> cases p₃ <;> simp only [Poly.casesOnNum, Int.reduceNeg,
+    Bool.and_eq_true, beq_iff_eq, decide_eq_true_eq, and_imp, Bool.false_eq_true,
+    mul_def, add_def, false_implies, Poly.denote]
+  next a b e =>
+  intro _ _ _ _; subst k₁ k₂ y z
+  intro h₁ h₃ h₆; generalize Var.denote ctx x = x'
+  intro h₄ h₅ h₂
+  rw [Int.one_mul] at h₅
+  exact cooper_unsat' h₁ h₂ h₃ h₄ h₅ h₆
+
 end Int.Linear

 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by
--- a/src/Init/Data/SInt/Lemmas.lean
+++ b/src/Init/Data/SInt/Lemmas.lean
@@ -7,6 +7,7 @@ prelude
 import Init.Data.SInt.Basic
 import Init.Data.BitVec.Bitblast
 import Init.Data.Int.LemmasAux
+import Init.Data.UInt.Lemmas

 open Lean in
 set_option hygiene false in
@@ -22,8 +23,8 @@ macro "declare_int_theorems" typeName:ident _bits:term:arg : command => do
    toBitVec_inj.symm
  @[int_toBitVec] theorem ne_iff_toBitVec_ne {a b : $typeName} : a ≠ b ↔ a.toBitVec ≠ b.toBitVec :=
    Decidable.not_iff_not.2 eq_iff_toBitVec_eq
-  @[simp] theorem toBitVec_ofNat {n : Nat} : toBitVec (ofNat n) = BitVec.ofNat _ n := rfl
-  @[simp, int_toBitVec] theorem toBitVec_ofNatOfNat {n : Nat} : toBitVec (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+  @[simp] theorem toBitVec_ofNat' {n : Nat} : toBitVec (ofNat n) = BitVec.ofNat _ n := rfl
+  @[simp, int_toBitVec] theorem toBitVec_ofNat {n : Nat} : toBitVec (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl

  end $typeName
  )
@@ -349,7 +350,6 @@ theorem ISize.toNatClampNeg_lt (x : ISize) : x.toNatClampNeg < 2 ^ 63 := (Int.to
@[simp] theorem Int64.toInt64_toUInt64 (x : Int64) : x.toUInt64.toInt64 = x := rfl
@[simp] theorem ISize.toISize_toUSize (x : ISize) : x.toUSize.toISize = x := rfl

-- TODO: possibly good simp lemmas in the reverse direction?
 theorem Int8.toNat_toBitVec (x : Int8) : x.toBitVec.toNat = x.toUInt8.toNat := rfl
 theorem Int16.toNat_toBitVec (x : Int16) : x.toBitVec.toNat = x.toUInt16.toNat := rfl
 theorem Int32.toNat_toBitVec (x : Int32) : x.toBitVec.toNat = x.toUInt32.toNat := rfl
@@ -378,7 +378,6 @@ theorem Int64.toNat_toUInt64_of_le {x : Int64} (hx : 0 ≤ x) : x.toUInt64.toNat
 theorem ISize.toNat_toUISize_of_le {x : ISize} (hx : 0 ≤ x) : x.toUSize.toNat = x.toNatClampNeg := by
  rw [← toNat_toBitVec, toNat_toBitVec_of_le hx]

-- TODO: possibly good simp lemmas in the reverse direction?
 theorem Int8.toFin_toBitVec (x : Int8) : x.toBitVec.toFin = x.toUInt8.toFin := rfl
 theorem Int16.toFin_toBitVec (x : Int16) : x.toBitVec.toFin = x.toUInt16.toFin := rfl
 theorem Int32.toFin_toBitVec (x : Int32) : x.toBitVec.toFin = x.toUInt32.toFin := rfl
@@ -837,3 +836,32 @@ theorem ISize.ofNat_int32ToNatClampNeg (x : Int32) (hx : 0 ≤ x) : ISize.ofNat

@[simp] theorem ISize.toISize_toInt64 (n : ISize) : n.toInt64.toISize = n :=
  ISize.toInt.inj (by simp)
+
+theorem UInt8.toInt8_ofNatLT {n : Nat} (hn) : (UInt8.ofNatLT n hn).toInt8 = Int8.ofNat n :=
+  Int8.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat])
+theorem UInt16.toInt16_ofNatLT {n : Nat} (hn) : (UInt16.ofNatLT n hn).toInt16 = Int16.ofNat n :=
+  Int16.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat])
+theorem UInt32.toInt32_ofNatLT {n : Nat} (hn) : (UInt32.ofNatLT n hn).toInt32 = Int32.ofNat n :=
+  Int32.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat])
+theorem UInt64.toInt64_ofNatLT {n : Nat} (hn) : (UInt64.ofNatLT n hn).toInt64 = Int64.ofNat n :=
+  Int64.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat])
+theorem USize.toISize_ofNatLT {n : Nat} (hn) : (USize.ofNatLT n hn).toISize = ISize.ofNat n :=
+  ISize.toBitVec.inj (by simp [BitVec.ofNatLT_eq_ofNat])
+
+@[simp] theorem UInt8.toInt8_ofNat' {n : Nat} : (UInt8.ofNat n).toInt8 = Int8.ofNat n := rfl
+@[simp] theorem UInt16.toInt16_ofNat' {n : Nat} : (UInt16.ofNat n).toInt16 = Int16.ofNat n := rfl
+@[simp] theorem UInt32.toInt32_ofNat' {n : Nat} : (UInt32.ofNat n).toInt32 = Int32.ofNat n := rfl
+@[simp] theorem UInt64.toInt64_ofNat' {n : Nat} : (UInt64.ofNat n).toInt64 = Int64.ofNat n := rfl
+@[simp] theorem USize.toISize_ofNat' {n : Nat} : (USize.ofNat n).toISize = ISize.ofNat n := rfl
+
+@[simp] theorem UInt8.toInt8_ofNat {n : Nat} : toInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+@[simp] theorem UInt16.toInt16_ofNat {n : Nat} : toInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+@[simp] theorem UInt32.toInt32_ofNat {n : Nat} : toInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+@[simp] theorem UInt64.toInt64_ofNat {n : Nat} : toInt64 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+@[simp] theorem USize.toISize_ofNat {n : Nat} : toISize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := rfl
+
+@[simp] theorem UInt8.toInt8_ofBitVec (b) : (UInt8.ofBitVec b).toInt8 = Int8.ofBitVec b := rfl
+@[simp] theorem UInt16.toInt16_ofBitVec (b) : (UInt16.ofBitVec b).toInt16 = Int16.ofBitVec b := rfl
+@[simp] theorem UInt32.toInt32_ofBitVec (b) : (UInt32.ofBitVec b).toInt32 = Int32.ofBitVec b := rfl
+@[simp] theorem UInt64.toInt64_ofBitVec (b) : (UInt64.ofBitVec b).toInt64 = Int64.ofBitVec b := rfl
+@[simp] theorem USize.toInt8_ofBitVec (b) : (USize.ofBitVec b).toISize = ISize.ofBitVec b := rfl
--- a/src/Init/Data/UInt/Lemmas.lean
+++ b/src/Init/Data/UInt/Lemmas.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura, François G. Dorais, Mario Carneiro, Mac Malone
+Authors: Leonardo de Moura, François G. Dorais, Mario Carneiro, Mac Malone, Markus Himmel
 -/
 prelude
 import Init.Data.UInt.Basic
@@ -27,7 +27,10 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
  @[deprecated toNat_ofBitVec (since := "2025-02-12")]
  theorem toNat_mk : (ofBitVec a).toNat = a.toNat := rfl

-  @[simp] theorem toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ $bits := BitVec.toNat_ofNat ..
+  @[simp] theorem toNat_ofNat' {n : Nat} : (ofNat n).toNat = n % 2 ^ $bits := BitVec.toNat_ofNat ..
+
+  -- Not `simp` because we have simprocs which will avoid the modulo.
+  theorem toNat_ofNat {n : Nat} : toNat (no_index (OfNat.ofNat n)) = n % 2 ^ $bits := toNat_ofNat'

  @[simp] theorem toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT ..

@@ -55,11 +58,16 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
  theorem mk_toBitVec_eq : ∀ (a : $typeName), ofBitVec a.toBitVec = a
    | ⟨_, _⟩ => rfl

+  @[deprecated "Use `toNat_toBitVec` and `toNat_ofNat_of_lt`." (since := "2025-03-05")]
  theorem toBitVec_eq_of_lt {a : Nat} : a < size → (ofNat a).toBitVec.toNat = a :=
    Nat.mod_eq_of_lt

-  theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
-    rw [toNat, toBitVec_eq_of_lt h]
+  theorem toBitVec_ofNat' (n : Nat) : (ofNat n).toBitVec = BitVec.ofNat _ n := rfl
+
+  theorem toNat_ofNat_of_lt' {n : Nat} (h : n < size) : (ofNat n).toNat = n := by
+    rw [toNat, toBitVec_ofNat', BitVec.toNat_ofNat, Nat.mod_eq_of_lt h]
+  theorem toNat_ofNat_of_lt {n : Nat} (h : n < size) : toNat (OfNat.ofNat n) = n :=
+    toNat_ofNat_of_lt' h

  @[int_toBitVec] theorem le_def {a b : $typeName} : a ≤ b ↔ a.toBitVec ≤ b.toBitVec := .rfl

@@ -151,10 +159,10 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do
  protected theorem toNat_lt_size (a : $typeName) : a.toNat < size := a.toBitVec.isLt

  open $typeName (toNat_mod toNat_lt_size) in
-  protected theorem toNat_mod_lt {m : Nat} : ∀ (u : $typeName), m > 0 → toNat (u % ofNat m) < m := by
+  protected theorem toNat_mod_lt {m : Nat} : ∀ (u : $typeName), 0 < m → toNat (u % ofNat m) < m := by
    intro u h1
    by_cases h2 : m < size
-    · rw [toNat_mod, toNat_ofNat_of_lt h2]
+    · rw [toNat_mod, toNat_ofNat_of_lt' h2]
      apply Nat.mod_lt _ h1
    · apply Nat.lt_of_lt_of_le
      · apply toNat_lt_size
@@ -258,16 +266,20 @@ theorem USize.toNat_ofNat_of_lt_32 {n : Nat} (h : n < 4294967296) : toNat (ofNat
  toNat_ofNat_of_lt (Nat.lt_of_lt_of_le h USize.le_size)

 theorem UInt32.toNat_lt_of_lt {n : UInt32} {m : Nat} (h : m < size) : n < ofNat m → n.toNat < m := by
-  simp [-toNat_toBitVec, lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  rw [lt_def, BitVec.lt_def, toNat_toBitVec, toNat_toBitVec, toNat_ofNat_of_lt' h]
+  exact id

 theorem UInt32.lt_toNat_of_lt {n : UInt32} {m : Nat} (h : m < size) : ofNat m < n → m < n.toNat := by
-  simp [-toNat_toBitVec, lt_def, BitVec.lt_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  rw [lt_def, BitVec.lt_def, toNat_toBitVec, toNat_toBitVec, toNat_ofNat_of_lt' h]
+  exact id

 theorem UInt32.toNat_le_of_le {n : UInt32} {m : Nat} (h : m < size) : n ≤ ofNat m → n.toNat ≤ m := by
-  simp [-toNat_toBitVec, le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  rw [le_def, BitVec.le_def, toNat_toBitVec, toNat_toBitVec, toNat_ofNat_of_lt' h]
+  exact id

 theorem UInt32.le_toNat_of_le {n : UInt32} {m : Nat} (h : m < size) : ofNat m ≤ n → m ≤ n.toNat := by
-  simp [-toNat_toBitVec, le_def, BitVec.le_def, UInt32.toNat, toBitVec_eq_of_lt h]
+  rw [le_def, BitVec.le_def, toNat_toBitVec, toNat_toBitVec, toNat_ofNat_of_lt' h]
+  exact id

@[simp] theorem UInt8.toNat_lt (n : UInt8) : n.toNat < 2 ^ 8 := n.toFin.isLt
@[simp] theorem UInt16.toNat_lt (n : UInt16) : n.toNat < 2 ^ 16 := n.toFin.isLt
@@ -311,6 +323,15 @@ theorem USize.size_dvd_uInt64Size : USize.size ∣ UInt64.size := by cases USize
@[simp] theorem mod_uInt64Size_uSizeSize (n : Nat) : n % UInt64.size % USize.size = n % USize.size :=
  Nat.mod_mod_of_dvd _ USize.size_dvd_uInt64Size

+@[simp] theorem USize.size_sub_one_mod_uint8Size : (USize.size - 1) % UInt8.size = UInt8.size - 1 := by
+  cases USize.size_eq <;> simp_all +decide
+@[simp] theorem USize.size_sub_one_mod_uint16Size : (USize.size - 1) % UInt16.size = UInt16.size - 1 := by
+  cases USize.size_eq <;> simp_all +decide
+@[simp] theorem USize.size_sub_one_mod_uint32Size : (USize.size - 1) % UInt32.size = UInt32.size - 1 := by
+  cases USize.size_eq <;> simp_all +decide
+@[simp] theorem UInt64.size_sub_one_mod_uSizeSize : 18446744073709551615 % USize.size = USize.size - 1 := by
+  cases USize.size_eq <;> simp_all +decide
+
@[simp] theorem UInt8.toNat_mod_size (n : UInt8) : n.toNat % UInt8.size = n.toNat := Nat.mod_eq_of_lt n.toNat_lt
@[simp] theorem UInt8.toNat_mod_uInt16Size (n : UInt8) : n.toNat % UInt16.size = n.toNat := Nat.mod_eq_of_lt (Nat.lt_trans n.toNat_lt (by decide))
@[simp] theorem UInt8.toNat_mod_uInt32Size (n : UInt8) : n.toNat % UInt32.size = n.toNat := Nat.mod_eq_of_lt (Nat.lt_trans n.toNat_lt (by decide))
@@ -785,3 +806,402 @@ theorem USize.ofNatTruncate_eq_ofNat (n : Nat) (hn : n < USize.size) :
 -- @[simp] theorem UInt64.toUSize_toUInt32 (n : UInt64) : n.toUInt32.toUSize = ? :=
 -- @[simp] theorem USize.toUInt64_toUInt32 (n : USize) : n.toUInt32.toUInt64 = ? :=
 -- @[simp] theorem USize.toUSize_toUInt32 (n : USize) : n.toInt32.toUSize = ? :=
+
+@[simp] theorem UInt8.toNat_ofFin (x : Fin UInt8.size) : (UInt8.ofFin x).toNat = x.val := rfl
+@[simp] theorem UInt16.toNat_ofFin (x : Fin UInt16.size) : (UInt16.ofFin x).toNat = x.val := rfl
+@[simp] theorem UInt32.toNat_ofFin (x : Fin UInt32.size) : (UInt32.ofFin x).toNat = x.val := rfl
+@[simp] theorem UInt64.toNat_ofFin (x : Fin UInt64.size) : (UInt64.ofFin x).toNat = x.val := rfl
+@[simp] theorem USize.toNat_ofFin (x : Fin USize.size) : (USize.ofFin x).toNat = x.val := rfl
+
+theorem UInt8.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt8.size) :
+    (UInt8.ofNatTruncate n).toNat = n := by rw [UInt8.ofNatTruncate, dif_pos hn, toNat_ofNatLT]
+theorem UInt16.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt16.size) :
+    (UInt16.ofNatTruncate n).toNat = n := by rw [UInt16.ofNatTruncate, dif_pos hn, toNat_ofNatLT]
+theorem UInt32.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt32.size) :
+    (UInt32.ofNatTruncate n).toNat = n := by rw [UInt32.ofNatTruncate, dif_pos hn, toNat_ofNatLT]
+theorem UInt64.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt64.size) :
+    (UInt64.ofNatTruncate n).toNat = n := by rw [UInt64.ofNatTruncate, dif_pos hn, toNat_ofNatLT]
+theorem USize.toNat_ofNatTruncate_of_lt {n : Nat} (hn : n < USize.size) :
+    (USize.ofNatTruncate n).toNat = n := by rw [USize.ofNatTruncate, dif_pos hn, toNat_ofNatLT]
+
+theorem UInt8.toNat_ofNatTruncate_of_le {n : Nat} (hn : UInt8.size ≤ n) :
+    (UInt8.ofNatTruncate n).toNat = UInt8.size - 1 := by rw [ofNatTruncate, dif_neg (by omega), toNat_ofNatLT]
+theorem UInt16.toNat_ofNatTruncate_of_le {n : Nat} (hn : UInt16.size ≤ n) :
+    (UInt16.ofNatTruncate n).toNat = UInt16.size - 1 := by rw [ofNatTruncate, dif_neg (by omega), toNat_ofNatLT]
+theorem UInt32.toNat_ofNatTruncate_of_le {n : Nat} (hn : UInt32.size ≤ n) :
+    (UInt32.ofNatTruncate n).toNat = UInt32.size - 1 := by rw [ofNatTruncate, dif_neg (by omega), toNat_ofNatLT]
+theorem UInt64.toNat_ofNatTruncate_of_le {n : Nat} (hn : UInt64.size ≤ n) :
+    (UInt64.ofNatTruncate n).toNat = UInt64.size - 1 := by rw [ofNatTruncate, dif_neg (by omega), toNat_ofNatLT]
+theorem USize.toNat_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
+    (USize.ofNatTruncate n).toNat = USize.size - 1 := by rw [ofNatTruncate, dif_neg (by omega), toNat_ofNatLT]
+
+@[simp] theorem UInt8.toFin_ofNatLT {n : Nat} (hn) : (UInt8.ofNatLT n hn).toFin = ⟨n, hn⟩ := rfl
+@[simp] theorem UInt16.toFin_ofNatLT {n : Nat} (hn) : (UInt16.ofNatLT n hn).toFin = ⟨n, hn⟩ := rfl
+@[simp] theorem UInt32.toFin_ofNatLT {n : Nat} (hn) : (UInt32.ofNatLT n hn).toFin = ⟨n, hn⟩ := rfl
+@[simp] theorem UInt64.toFin_ofNatLT {n : Nat} (hn) : (UInt64.ofNatLT n hn).toFin = ⟨n, hn⟩ := rfl
+@[simp] theorem USize.toFin_ofNatLT {n : Nat} (hn) : (USize.ofNatLT n hn).toFin = ⟨n, hn⟩ := rfl
+
+@[simp] theorem UInt8.toFin_ofNat' {n : Nat} : (UInt8.ofNat n).toFin = Fin.ofNat' _ n := rfl
+@[simp] theorem UInt16.toFin_ofNat' {n : Nat} : (UInt16.ofNat n).toFin = Fin.ofNat' _ n := rfl
+@[simp] theorem UInt32.toFin_ofNat' {n : Nat} : (UInt32.ofNat n).toFin = Fin.ofNat' _ n := rfl
+@[simp] theorem UInt64.toFin_ofNat' {n : Nat} : (UInt64.ofNat n).toFin = Fin.ofNat' _ n := rfl
+@[simp] theorem USize.toFin_ofNat' {n : Nat} : (USize.ofNat n).toFin = Fin.ofNat' _ n := rfl
+
+@[simp] theorem UInt8.toFin_ofBitVec {b} : (UInt8.ofBitVec b).toFin = b.toFin := rfl
+@[simp] theorem UInt16.toFin_ofBitVec {b} : (UInt16.ofBitVec b).toFin = b.toFin := rfl
+@[simp] theorem UInt32.toFin_ofBitVec {b} : (UInt32.ofBitVec b).toFin = b.toFin := rfl
+@[simp] theorem UInt64.toFin_ofBitVec {b} : (UInt64.ofBitVec b).toFin = b.toFin := rfl
+@[simp] theorem USize.toFin_ofBitVec {b} : (USize.ofBitVec b).toFin = b.toFin := rfl
+
+theorem UInt8.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt8.size) :
+    (UInt8.ofNatTruncate n).toFin = ⟨n, hn⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt16.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt16.size) :
+    (UInt16.ofNatTruncate n).toFin = ⟨n, hn⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt32.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt32.size) :
+    (UInt32.ofNatTruncate n).toFin = ⟨n, hn⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt64.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt64.size) :
+    (UInt64.ofNatTruncate n).toFin = ⟨n, hn⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem USize.toFin_ofNatTruncate_of_lt {n : Nat} (hn : n < USize.size) :
+    (USize.ofNatTruncate n).toFin = ⟨n, hn⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_lt hn])
+
+theorem UInt8.toFin_ofNatTruncate_of_le {n : Nat} (hn : UInt8.size ≤ n) :
+    (UInt8.ofNatTruncate n).toFin = ⟨UInt8.size - 1, by decide⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt16.toFin_ofNatTruncate_of_le {n : Nat} (hn : UInt16.size ≤ n) :
+    (UInt16.ofNatTruncate n).toFin = ⟨UInt16.size - 1, by decide⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt32.toFin_ofNatTruncate_of_le {n : Nat} (hn : UInt32.size ≤ n) :
+    (UInt32.ofNatTruncate n).toFin = ⟨UInt32.size - 1, by decide⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt64.toFin_ofNatTruncate_of_le {n : Nat} (hn : UInt64.size ≤ n) :
+    (UInt64.ofNatTruncate n).toFin = ⟨UInt64.size - 1, by decide⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_le hn])
+theorem USize.toFin_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
+    (USize.ofNatTruncate n).toFin = ⟨USize.size - 1, by cases USize.size_eq <;> simp_all⟩ :=
+  Fin.val_inj.1 (by simp [toNat_ofNatTruncate_of_le hn])
+
+@[simp] theorem UInt8.toBitVec_ofNatLT {n : Nat} (hn : n < UInt8.size) :
+    (UInt8.ofNatLT n hn).toBitVec = BitVec.ofNatLT n hn := rfl
+@[simp] theorem UInt16.toBitVec_ofNatLT {n : Nat} (hn : n < UInt16.size) :
+    (UInt16.ofNatLT n hn).toBitVec = BitVec.ofNatLT n hn := rfl
+@[simp] theorem UInt32.toBitVec_ofNatLT {n : Nat} (hn : n < UInt32.size) :
+    (UInt32.ofNatLT n hn).toBitVec = BitVec.ofNatLT n hn := rfl
+@[simp] theorem UInt64.toBitVec_ofNatLT {n : Nat} (hn : n < UInt64.size) :
+    (UInt64.ofNatLT n hn).toBitVec = BitVec.ofNatLT n hn := rfl
+@[simp] theorem USize.toBitVec_ofNatLT {n : Nat} (hn : n < USize.size) :
+    (USize.ofNatLT n hn).toBitVec = BitVec.ofNatLT n hn := rfl
+
+@[simp] theorem UInt8.toBitVec_ofFin (n : Fin UInt8.size) : (UInt8.ofFin n).toBitVec = BitVec.ofFin n := rfl
+@[simp] theorem UInt16.toBitVec_ofFin (n : Fin UInt16.size) : (UInt16.ofFin n).toBitVec = BitVec.ofFin n := rfl
+@[simp] theorem UInt32.toBitVec_ofFin (n : Fin UInt32.size) : (UInt32.ofFin n).toBitVec = BitVec.ofFin n := rfl
+@[simp] theorem UInt64.toBitVec_ofFin (n : Fin UInt64.size) : (UInt64.ofFin n).toBitVec = BitVec.ofFin n := rfl
+@[simp] theorem USize.toBitVec_ofFin (n : Fin USize.size) : (USize.ofFin n).toBitVec = BitVec.ofFin n := rfl
+
+@[simp] theorem UInt8.toBitVec_ofBitVec (n) : (UInt8.ofBitVec n).toBitVec = n := rfl
+@[simp] theorem UInt16.toBitVec_ofBitVec (n) : (UInt16.ofBitVec n).toBitVec = n := rfl
+@[simp] theorem UInt32.toBitVec_ofBitVec (n) : (UInt32.ofBitVec n).toBitVec = n := rfl
+@[simp] theorem UInt64.toBitVec_ofBitVec (n) : (UInt64.ofBitVec n).toBitVec = n := rfl
+@[simp] theorem USize.toBitVec_ofBitVec (n) : (USize.ofBitVec n).toBitVec = n := rfl
+
+theorem UInt8.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt8.size) :
+    (UInt8.ofNatTruncate n).toBitVec = BitVec.ofNatLT n hn :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt16.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt16.size) :
+    (UInt16.ofNatTruncate n).toBitVec = BitVec.ofNatLT n hn :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt32.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt32.size) :
+    (UInt32.ofNatTruncate n).toBitVec = BitVec.ofNatLT n hn :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt64.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt64.size) :
+    (UInt64.ofNatTruncate n).toBitVec = BitVec.ofNatLT n hn :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem USize.toBitVec_ofNatTruncate_of_lt {n : Nat} (hn : n < USize.size) :
+    (USize.ofNatTruncate n).toBitVec = BitVec.ofNatLT n hn :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_lt hn])
+
+theorem UInt8.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : UInt8.size ≤ n) :
+    (UInt8.ofNatTruncate n).toBitVec = BitVec.ofNatLT (UInt8.size - 1) (by decide) :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt16.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : UInt16.size ≤ n) :
+    (UInt16.ofNatTruncate n).toBitVec = BitVec.ofNatLT (UInt16.size - 1) (by decide) :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt32.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : UInt32.size ≤ n) :
+    (UInt32.ofNatTruncate n).toBitVec = BitVec.ofNatLT (UInt32.size - 1) (by decide) :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt64.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : UInt64.size ≤ n) :
+    (UInt64.ofNatTruncate n).toBitVec = BitVec.ofNatLT (UInt64.size - 1) (by decide) :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_le hn])
+theorem USize.toBitVec_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
+    (USize.ofNatTruncate n).toBitVec = BitVec.ofNatLT (USize.size - 1) (by cases USize.size_eq <;> simp_all) :=
+  BitVec.eq_of_toNat_eq (by simp [toNat_ofNatTruncate_of_le hn])
+
+@[simp] theorem UInt16.toUInt8_ofNatLT {n : Nat} (hn) : (UInt16.ofNatLT n hn).toUInt8 = UInt8.ofNat n := rfl
+@[simp] theorem UInt32.toUInt8_ofNatLT {n : Nat} (hn) : (UInt32.ofNatLT n hn).toUInt8 = UInt8.ofNat n := rfl
+@[simp] theorem UInt64.toUInt8_ofNatLT {n : Nat} (hn) : (UInt64.ofNatLT n hn).toUInt8 = UInt8.ofNat n := rfl
+@[simp] theorem USize.toUInt8_ofNatLT {n : Nat} (hn) : (USize.ofNatLT n hn).toUInt8 = UInt8.ofNat n := rfl
+
+@[simp] theorem UInt16.toUInt8_ofFin (n) : (UInt16.ofFin n).toUInt8 = UInt8.ofNat n.val := rfl
+@[simp] theorem UInt32.toUInt8_ofFin (n) : (UInt32.ofFin n).toUInt8 = UInt8.ofNat n.val := rfl
+@[simp] theorem UInt64.toUInt8_ofFin (n) : (UInt64.ofFin n).toUInt8 = UInt8.ofNat n.val := rfl
+@[simp] theorem USize.toUInt8_ofFin (n) : (USize.ofFin n).toUInt8 = UInt8.ofNat n.val := rfl
+
+@[simp] theorem UInt16.toUInt8_ofBitVec (b) : (UInt16.ofBitVec b).toUInt8 = UInt8.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem UInt32.toUInt8_ofBitVec (b) : (UInt32.ofBitVec b).toUInt8 = UInt8.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem UInt64.toUInt8_ofBitVec (b) : (UInt64.ofBitVec b).toUInt8 = UInt8.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem USize.toUInt8_ofBitVec (b) : (USize.ofBitVec b).toUInt8 = UInt8.ofBitVec (b.setWidth _) :=
+  UInt8.toNat.inj (by simp)
+
+@[simp] theorem UInt16.toUInt8_ofNat' (n : Nat) : (UInt16.ofNat n).toUInt8 = UInt8.ofNat n := UInt8.toNat.inj (by simp)
+@[simp] theorem UInt32.toUInt8_ofNat' (n : Nat) : (UInt32.ofNat n).toUInt8 = UInt8.ofNat n := UInt8.toNat.inj (by simp)
+@[simp] theorem UInt64.toUInt8_ofNat' (n : Nat) : (UInt64.ofNat n).toUInt8 = UInt8.ofNat n := UInt8.toNat.inj (by simp)
+@[simp] theorem USize.toUInt8_ofNat' (n : Nat) : (USize.ofNat n).toUInt8 = UInt8.ofNat n := UInt8.toNat.inj (by simp)
+
+@[simp] theorem UInt16.toUInt8_ofNat {n : Nat} : toUInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toUInt8_ofNat' _
+@[simp] theorem UInt32.toUInt8_ofNat {n : Nat} : toUInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toUInt8_ofNat' _
+@[simp] theorem UInt64.toUInt8_ofNat {n : Nat} : toUInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toUInt8_ofNat' _
+@[simp] theorem USize.toUInt8_ofNat {n : Nat} : toUInt8 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := toUInt8_ofNat' _
+
+theorem UInt16.toUInt8_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt16.size) :
+    (UInt16.ofNatTruncate n).toUInt8 = UInt8.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUInt8_ofNatLT]
+theorem UInt32.toUInt8_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt32.size) :
+    (UInt32.ofNatTruncate n).toUInt8 = UInt8.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUInt8_ofNatLT]
+theorem UInt64.toUInt8_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt64.size) :
+    (UInt64.ofNatTruncate n).toUInt8 = UInt8.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUInt8_ofNatLT]
+theorem USize.toUInt8_ofNatTruncate_of_lt {n : Nat} (hn : n < USize.size) :
+    (USize.ofNatTruncate n).toUInt8 = UInt8.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUInt8_ofNatLT]
+
+theorem UInt16.toUInt8_ofNatTruncate_of_le {n : Nat} (hn : UInt16.size ≤ n) :
+    (UInt16.ofNatTruncate n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) (by decide) :=
+  UInt8.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt32.toUInt8_ofNatTruncate_of_le {n : Nat} (hn : UInt32.size ≤ n) :
+    (UInt32.ofNatTruncate n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) (by decide) :=
+  UInt8.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt64.toUInt8_ofNatTruncate_of_le {n : Nat} (hn : UInt64.size ≤ n) :
+    (UInt64.ofNatTruncate n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) (by decide) :=
+  UInt8.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem USize.toUInt8_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
+    (USize.ofNatTruncate n).toUInt8 = UInt8.ofNatLT (UInt8.size - 1) (by decide) :=
+  UInt8.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+
+@[simp] theorem UInt32.toUInt16_ofNatLT {n : Nat} (hn) : (UInt32.ofNatLT n hn).toUInt16 = UInt16.ofNat n := rfl
+@[simp] theorem UInt64.toUInt16_ofNatLT {n : Nat} (hn) : (UInt64.ofNatLT n hn).toUInt16 = UInt16.ofNat n := rfl
+@[simp] theorem USize.toUInt16_ofNatLT {n : Nat} (hn) : (USize.ofNatLT n hn).toUInt16 = UInt16.ofNat n := rfl
+
+@[simp] theorem UInt32.toUInt16_ofFin (n) : (UInt32.ofFin n).toUInt16 = UInt16.ofNat n.val := rfl
+@[simp] theorem UInt64.toUInt16_ofFin (n) : (UInt64.ofFin n).toUInt16 = UInt16.ofNat n.val := rfl
+@[simp] theorem USize.toUInt16_ofFin (n) : (USize.ofFin n).toUInt16 = UInt16.ofNat n.val := rfl
+
+@[simp] theorem UInt32.toUInt16_ofBitVec (b) : (UInt32.ofBitVec b).toUInt16 = UInt16.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem UInt64.toUInt16_ofBitVec (b) : (UInt64.ofBitVec b).toUInt16 = UInt16.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem USize.toUInt16_ofBitVec (b) : (USize.ofBitVec b).toUInt16 = UInt16.ofBitVec (b.setWidth _) :=
+  UInt16.toNat.inj (by simp)
+
+@[simp] theorem UInt32.toUInt16_ofNat' (n : Nat) : (UInt32.ofNat n).toUInt16 = UInt16.ofNat n := UInt16.toNat.inj (by simp)
+@[simp] theorem UInt64.toUInt16_ofNat' (n : Nat) : (UInt64.ofNat n).toUInt16 = UInt16.ofNat n := UInt16.toNat.inj (by simp)
+@[simp] theorem USize.toUInt16_ofNat' (n : Nat) : (USize.ofNat n).toUInt16 = UInt16.ofNat n := UInt16.toNat.inj (by simp)
+
+@[simp] theorem UInt32.toUInt16_ofNat {n : Nat} : toUInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := UInt32.toUInt16_ofNat' _
+@[simp] theorem UInt64.toUInt16_ofNat {n : Nat} : toUInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := UInt64.toUInt16_ofNat' _
+@[simp] theorem USize.toUInt16_ofNat {n : Nat} : toUInt16 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := USize.toUInt16_ofNat' _
+
+theorem UInt32.toUInt16_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt32.size) :
+    (UInt32.ofNatTruncate n).toUInt16 = UInt16.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUInt16_ofNatLT]
+theorem UInt64.toUInt16_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt64.size) :
+    (UInt64.ofNatTruncate n).toUInt16 = UInt16.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUInt16_ofNatLT]
+theorem USize.toUInt16_ofNatTruncate_of_lt {n : Nat} (hn : n < USize.size) :
+    (USize.ofNatTruncate n).toUInt16 = UInt16.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUInt16_ofNatLT]
+
+theorem UInt32.toUInt16_ofNatTruncate_of_le {n : Nat} (hn : UInt32.size ≤ n) :
+    (UInt32.ofNatTruncate n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) (by decide) :=
+  UInt16.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt64.toUInt16_ofNatTruncate_of_le {n : Nat} (hn : UInt64.size ≤ n) :
+    (UInt64.ofNatTruncate n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) (by decide) :=
+  UInt16.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem USize.toUInt16_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
+    (USize.ofNatTruncate n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) (by decide) :=
+  UInt16.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+
+@[simp] theorem UInt64.toUInt32_ofNatLT {n : Nat} (hn) : (UInt64.ofNatLT n hn).toUInt32 = UInt32.ofNat n := rfl
+@[simp] theorem USize.toUInt32_ofNatLT {n : Nat} (hn) : (USize.ofNatLT n hn).toUInt32 = UInt32.ofNat n := rfl
+
+@[simp] theorem UInt64.toUInt32_ofFin (n) : (UInt64.ofFin n).toUInt32 = UInt32.ofNat n.val := rfl
+@[simp] theorem USize.toUInt32_ofFin (n) : (USize.ofFin n).toUInt32 = UInt32.ofNat n.val := rfl
+
+@[simp] theorem UInt64.toUInt32_ofBitVec (b) : (UInt64.ofBitVec b).toUInt32 = UInt32.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem USize.toUInt32_ofBitVec (b) : (USize.ofBitVec b).toUInt32 = UInt32.ofBitVec (b.setWidth _) :=
+  UInt32.toNat.inj (by simp)
+
+@[simp] theorem UInt64.toUInt32_ofNat' (n : Nat) : (UInt64.ofNat n).toUInt32 = UInt32.ofNat n := UInt32.toNat.inj (by simp)
+@[simp] theorem USize.toUInt32_ofNat' (n : Nat) : (USize.ofNat n).toUInt32 = UInt32.ofNat n := UInt32.toNat.inj (by simp)
+
+@[simp] theorem UInt64.toUInt32_ofNat {n : Nat} : toUInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := UInt64.toUInt32_ofNat' _
+@[simp] theorem USize.toUInt32_ofNat {n : Nat} : toUInt32 (no_index (OfNat.ofNat n)) = OfNat.ofNat n := USize.toUInt32_ofNat' _
+
+theorem UInt64.toUInt32_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt64.size) :
+    (UInt64.ofNatTruncate n).toUInt32 = UInt32.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUInt32_ofNatLT]
+theorem USize.toUInt32_ofNatTruncate_of_lt {n : Nat} (hn : n < USize.size) :
+    (USize.ofNatTruncate n).toUInt32 = UInt32.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUInt32_ofNatLT]
+
+theorem UInt64.toUInt32_ofNatTruncate_of_le {n : Nat} (hn : UInt64.size ≤ n) :
+    (UInt64.ofNatTruncate n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) (by decide) :=
+  UInt32.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem USize.toUInt32_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
+    (USize.ofNatTruncate n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) (by decide) :=
+  UInt32.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+
+@[simp] theorem UInt64.toUSize_ofNatLT {n : Nat} (hn) : (UInt64.ofNatLT n hn).toUSize = USize.ofNat n := rfl
+
+@[simp] theorem UInt64.toUSize_ofFin (n) : (UInt64.ofFin n).toUSize = USize.ofNat n.val := rfl
+
+@[simp] theorem UInt64.toUSize_ofBitVec (b) : (UInt64.ofBitVec b).toUSize = USize.ofBitVec (b.setWidth _) :=
+  USize.toNat.inj (by simp)
+
+@[simp] theorem UInt64.toUSize_ofNat' (n : Nat) : (UInt64.ofNat n).toUSize = USize.ofNat n := USize.toNat.inj (by simp)
+
+@[simp] theorem UInt64.toUSize_ofNat {n : Nat} : toUSize (no_index (OfNat.ofNat n)) = OfNat.ofNat n := UInt64.toUSize_ofNat' _
+
+theorem UInt64.toUSize_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt64.size) :
+    (UInt64.ofNatTruncate n).toUSize = USize.ofNat n := by rw [ofNatTruncate, dif_pos hn, toUSize_ofNatLT]
+
+theorem UInt64.toUSize_ofNatTruncate_of_le {n : Nat} (hn : UInt64.size ≤ n) :
+    (UInt64.ofNatTruncate n).toUSize = USize.ofNatLT (USize.size - 1) (by cases USize.size_eq <;> simp_all) :=
+  USize.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+
+theorem UInt8.toUInt16_ofNatLT {n : Nat} (h) :
+    (UInt8.ofNatLT n h).toUInt16 = UInt16.ofNatLT n (Nat.lt_of_lt_of_le h (by decide)) := rfl
+theorem UInt8.toUInt32_ofNatLT {n : Nat} (h) :
+    (UInt8.ofNatLT n h).toUInt32 = UInt32.ofNatLT n (Nat.lt_of_lt_of_le h (by decide)) := rfl
+theorem UInt8.toUInt64_ofNatLT {n : Nat} (h) :
+    (UInt8.ofNatLT n h).toUInt64 = UInt64.ofNatLT n (Nat.lt_of_lt_of_le h (by decide)) := rfl
+theorem UInt8.toUSize_ofNatLT {n : Nat} (h) :
+    (UInt8.ofNatLT n h).toUSize = USize.ofNatLT n (Nat.lt_of_lt_of_le h size_le_usizeSize) := rfl
+
+theorem UInt8.toUInt16_ofFin {n} :
+  (UInt8.ofFin n).toUInt16 = UInt16.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt (by decide)) := rfl
+theorem UInt8.toUInt32_ofFin {n} :
+  (UInt8.ofFin n).toUInt32 = UInt32.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt (by decide)) := rfl
+theorem UInt8.toUInt64_ofFin {n} :
+  (UInt8.ofFin n).toUInt64 = UInt64.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt (by decide)) := rfl
+theorem UInt8.toUSize_ofFin {n} :
+  (UInt8.ofFin n).toUSize = USize.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt size_le_usizeSize) := rfl
+
+@[simp] theorem UInt8.toUInt16_ofBitVec {b} : (UInt8.ofBitVec b).toUInt16 = UInt16.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem UInt8.toUInt32_ofBitVec {b} : (UInt8.ofBitVec b).toUInt32 = UInt32.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem UInt8.toUInt64_ofBitVec {b} : (UInt8.ofBitVec b).toUInt64 = UInt64.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem UInt8.toUSize_ofBitVec {b} : (UInt8.ofBitVec b).toUSize = USize.ofBitVec (b.setWidth _) :=
+  USize.toBitVec_inj.1 (by simp)
+
+theorem UInt8.toUInt16_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt8.size) :
+    (UInt8.ofNatTruncate n).toUInt16 = UInt16.ofNatLT n (Nat.lt_of_lt_of_le hn (by decide)) :=
+  UInt16.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt8.toUInt32_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt8.size) :
+    (UInt8.ofNatTruncate n).toUInt32 = UInt32.ofNatLT n (Nat.lt_of_lt_of_le hn (by decide)) :=
+  UInt32.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt8.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt8.size) :
+    (UInt8.ofNatTruncate n).toUInt64 = UInt64.ofNatLT n (Nat.lt_of_lt_of_le hn (by decide)) :=
+  UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt8.toUSize_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt8.size) :
+    (UInt8.ofNatTruncate n).toUSize = USize.ofNatLT n (Nat.lt_of_lt_of_le hn size_le_usizeSize) :=
+  USize.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+
+theorem UInt8.toUInt16_ofNatTruncate_of_le {n : Nat} (hn : UInt8.size ≤ n) :
+    (UInt8.ofNatTruncate n).toUInt16 = UInt16.ofNatLT (UInt8.size - 1) (by decide) :=
+  UInt16.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt8.toUInt32_ofNatTruncate_of_le {n : Nat} (hn : UInt8.size ≤ n) :
+    (UInt8.ofNatTruncate n).toUInt32 = UInt32.ofNatLT (UInt8.size - 1) (by decide) :=
+  UInt32.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt8.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : UInt8.size ≤ n) :
+    (UInt8.ofNatTruncate n).toUInt64 = UInt64.ofNatLT (UInt8.size - 1) (by decide) :=
+  UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt8.toUSize_ofNatTruncate_of_le {n : Nat} (hn : UInt8.size ≤ n) :
+    (UInt8.ofNatTruncate n).toUSize = USize.ofNatLT (UInt8.size - 1) (Nat.lt_of_lt_of_le (by decide) size_le_usizeSize) :=
+  USize.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+
+theorem UInt16.toUInt32_ofNatLT {n : Nat} (h) :
+    (UInt16.ofNatLT n h).toUInt32 = UInt32.ofNatLT n (Nat.lt_of_lt_of_le h (by decide)) := rfl
+theorem UInt16.toUInt64_ofNatLT {n : Nat} (h) :
+    (UInt16.ofNatLT n h).toUInt64 = UInt64.ofNatLT n (Nat.lt_of_lt_of_le h (by decide)) := rfl
+theorem UInt16.toUSize_ofNatLT {n : Nat} (h) :
+    (UInt16.ofNatLT n h).toUSize = USize.ofNatLT n (Nat.lt_of_lt_of_le h size_le_usizeSize) := rfl
+
+theorem UInt16.toUInt32_ofFin {n} :
+  (UInt16.ofFin n).toUInt32 = UInt32.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt (by decide)) := rfl
+theorem UInt16.toUInt64_ofFin {n} :
+  (UInt16.ofFin n).toUInt64 = UInt64.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt (by decide)) := rfl
+theorem UInt16.toUSize_ofFin {n} :
+  (UInt16.ofFin n).toUSize = USize.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt size_le_usizeSize) := rfl
+
+@[simp] theorem UInt16.toUInt32_ofBitVec {b} : (UInt16.ofBitVec b).toUInt32 = UInt32.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem UInt16.toUInt64_ofBitVec {b} : (UInt16.ofBitVec b).toUInt64 = UInt64.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem UInt16.toUSize_ofBitVec {b} : (UInt16.ofBitVec b).toUSize = USize.ofBitVec (b.setWidth _) :=
+  USize.toBitVec_inj.1 (by simp)
+
+theorem UInt16.toUInt32_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt16.size) :
+    (UInt16.ofNatTruncate n).toUInt32 = UInt32.ofNatLT n (Nat.lt_of_lt_of_le hn (by decide)) :=
+  UInt32.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt16.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt16.size) :
+    (UInt16.ofNatTruncate n).toUInt64 = UInt64.ofNatLT n (Nat.lt_of_lt_of_le hn (by decide)) :=
+  UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt16.toUSize_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt16.size) :
+    (UInt16.ofNatTruncate n).toUSize = USize.ofNatLT n (Nat.lt_of_lt_of_le hn size_le_usizeSize) :=
+  USize.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+
+theorem UInt16.toUInt32_ofNatTruncate_of_le {n : Nat} (hn : UInt16.size ≤ n) :
+    (UInt16.ofNatTruncate n).toUInt32 = UInt32.ofNatLT (UInt16.size - 1) (by decide) :=
+  UInt32.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt16.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : UInt16.size ≤ n) :
+    (UInt16.ofNatTruncate n).toUInt64 = UInt64.ofNatLT (UInt16.size - 1) (by decide) :=
+  UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt16.toUSize_ofNatTruncate_of_le {n : Nat} (hn : UInt16.size ≤ n) :
+    (UInt16.ofNatTruncate n).toUSize = USize.ofNatLT (UInt16.size - 1) (Nat.lt_of_lt_of_le (by decide) size_le_usizeSize) :=
+  USize.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+
+theorem UInt32.toUInt64_ofNatLT {n : Nat} (h) :
+    (UInt32.ofNatLT n h).toUInt64 = UInt64.ofNatLT n (Nat.lt_of_lt_of_le h (by decide)) := rfl
+theorem UInt32.toUSize_ofNatLT {n : Nat} (h) :
+    (UInt32.ofNatLT n h).toUSize = USize.ofNatLT n (Nat.lt_of_lt_of_le h size_le_usizeSize) := rfl
+
+theorem UInt32.toUInt64_ofFin {n} :
+  (UInt32.ofFin n).toUInt64 = UInt64.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt (by decide)) := rfl
+theorem UInt32.toUSize_ofFin {n} :
+  (UInt32.ofFin n).toUSize = USize.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt size_le_usizeSize) := rfl
+
+@[simp] theorem UInt32.toUInt64_ofBitVec {b} : (UInt32.ofBitVec b).toUInt64 = UInt64.ofBitVec (b.setWidth _) := rfl
+@[simp] theorem UInt32.toUSize_ofBitVec {b} : (UInt32.ofBitVec b).toUSize = USize.ofBitVec (b.setWidth _) :=
+  USize.toBitVec_inj.1 (by simp)
+
+theorem UInt32.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt32.size) :
+    (UInt32.ofNatTruncate n).toUInt64 = UInt64.ofNatLT n (Nat.lt_of_lt_of_le hn (by decide)) :=
+  UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+theorem UInt32.toUSize_ofNatTruncate_of_lt {n : Nat} (hn : n < UInt32.size) :
+    (UInt32.ofNatTruncate n).toUSize = USize.ofNatLT n (Nat.lt_of_lt_of_le hn size_le_usizeSize) :=
+  USize.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+
+theorem UInt32.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : UInt32.size ≤ n) :
+    (UInt32.ofNatTruncate n).toUInt64 = UInt64.ofNatLT (UInt32.size - 1) (by decide) :=
+  UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+theorem UInt32.toUSize_ofNatTruncate_of_le {n : Nat} (hn : UInt32.size ≤ n) :
+    (UInt32.ofNatTruncate n).toUSize = USize.ofNatLT (UInt32.size - 1) (Nat.lt_of_lt_of_le (by decide) size_le_usizeSize) :=
+  USize.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
+
+theorem USize.toUInt64_ofNatLT {n : Nat} (h) :
+    (USize.ofNatLT n h).toUInt64 = UInt64.ofNatLT n (Nat.lt_of_lt_of_le h size_le_uint64Size) := rfl
+
+theorem USize.toUInt64_ofFin {n} :
+  (USize.ofFin n).toUInt64 = UInt64.ofNatLT n.val (Nat.lt_of_lt_of_le n.isLt size_le_uint64Size) := rfl
+
+@[simp] theorem USize.toUInt64_ofBitVec {b} : (USize.ofBitVec b).toUInt64 = UInt64.ofBitVec (b.setWidth _) :=
+  UInt64.toBitVec_inj.1 (by simp)
+
+theorem USize.toUInt64_ofNatTruncate_of_lt {n : Nat} (hn : n < USize.size) :
+    (USize.ofNatTruncate n).toUInt64 = UInt64.ofNatLT n (Nat.lt_of_lt_of_le hn size_le_uint64Size) :=
+  UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_lt hn])
+
+theorem USize.toUInt64_ofNatTruncate_of_le {n : Nat} (hn : USize.size ≤ n) :
+    (USize.ofNatTruncate n).toUInt64 = UInt64.ofNatLT (USize.size - 1) (by cases USize.size_eq <;> simp_all +decide) :=
+  UInt64.toNat.inj (by simp [toNat_ofNatTruncate_of_le hn])
--- a/src/Init/System/Promise.lean
+++ b/src/Init/System/Promise.lean
@@ -75,3 +75,10 @@ Like `Promise.result`, but resolves to `dflt` if the promise is dropped without
 -/
@[macro_inline] def Promise.resultD (promise : Promise α) (dflt : α) : Task α :=
  promise.result?.map (sync := true) (·.getD dflt)
+
+/--
+Checks whether the promise has already been resolved, i.e. whether access to `result*` will return
+immediately.
+-/
+def Promise.isResolved (promise : Promise α) : BaseIO Bool :=
+  IO.hasFinished promise.result?
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -46,9 +46,9 @@ where go env
 def addDecl (decl : Declaration) : CoreM Unit := do
  -- register namespaces for newly added constants; this used to be done by the kernel itself
  -- but that is incompatible with moving it to a separate task
+  -- NOTE: we do not use `getTopLevelNames` here so that inductive types are registered as
+  -- namespaces
  modifyEnv (decl.getNames.foldl registerNamePrefixes)
-  if let .inductDecl _ _ types _ := decl then
-    modifyEnv (types.foldl (registerNamePrefixes · <| ·.name ++ `rec))

  if !Elab.async.get (← getOptions) then
    return (← doAdd)
@@ -79,7 +79,7 @@ def addDecl (decl : Declaration) : CoreM Unit := do
  Core.logSnapshotTask { stx? := none, reportingRange? := endRange?, task := t, cancelTk? := cancelTk }
 where doAdd := do
  profileitM Exception "type checking" (← getOptions) do
-    withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getNames}") do
+    withTraceNode `Kernel (fun _ => return m!"typechecking declarations {decl.getTopLevelNames}") do
      if !(← MonadLog.hasErrors) && decl.hasSorry then
        logWarning m!"declaration uses 'sorry'"
      let env ← (← getEnv).addDeclAux (← getOptions) decl (← read).cancelTk?
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -194,8 +194,22 @@ def Declaration.definitionVal! : Declaration → DefinitionVal
  | _ => panic! "Expected a `Declaration.defnDecl`."

 /--
-Returns all top-level names to be defined by adding this declaration to the environment. This does
-not include auxiliary definitions such as projections.
+Returns all top-level names to be defined by adding this declaration to the environment, i.e.
+excluding nested helper declarations generated automatically.
+-/
+def Declaration.getTopLevelNames : Declaration → List Name
+  | .axiomDecl val          => [val.name]
+  | .defnDecl val           => [val.name]
+  | .thmDecl val            => [val.name]
+  | .opaqueDecl val         => [val.name]
+  | .quotDecl               => [``Quot]
+  | .mutualDefnDecl defns   => defns.map (·.name)
+  | .inductDecl _ _ types _ => types.map (·.name)
+
+/--
+Returns all names to be defined by adding this declaration to the environment. This does not include
+auxiliary definitions such as projections added by the elaborator, nor auxiliary recursors computed
+by the kernel for nested inductive types.
 -/
 def Declaration.getNames : Declaration → List Name
  | .axiomDecl val          => [val.name]
@@ -204,7 +218,7 @@ def Declaration.getNames : Declaration → List Name
  | .opaqueDecl val         => [val.name]
  | .quotDecl               => [``Quot, ``Quot.mk, ``Quot.lift, ``Quot.ind]
  | .mutualDefnDecl defns   => defns.map (·.name)
-  | .inductDecl _ _ types _ => types.map (·.name)
+  | .inductDecl _ _ types _ => types.flatMap fun t => t.name :: (t.name.appendCore `rec) :: t.ctors.map (·.name)

@[specialize] def Declaration.foldExprM {α} {m : Type → Type} [Monad m] (d : Declaration) (f : α → Expr → m α) (a : α) : m α :=
  match d with
--- a/src/Lean/Elab/MutualInductive.lean
+++ b/src/Lean/Elab/MutualInductive.lean
@@ -910,6 +910,24 @@ private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep
          let decl := Declaration.inductDecl levelParams numParams indTypes isUnsafe
          Term.ensureNoUnassignedMVars decl
          addDecl decl
+
+          -- For nested inductive types, the kernel adds a variable number of auxiliary recursors.
+          -- Let the elaborator know about them as well. (Other auxiliaries have already been
+          -- registered by `addDecl` via `Declaration.getNames`.)
+          -- NOTE: If we want to make inductive elaboration parallel, this should switch to using
+          -- reserved names.
+          for indType in indTypes do
+            let mut i := 1
+            while true do
+              let auxRecName := indType.name ++ `rec |>.appendIndexAfter i
+              let env ← getEnv
+              let some const := env.toKernelEnv.find? auxRecName | break
+              let res ← env.addConstAsync auxRecName .recursor
+              res.commitConst res.asyncEnv (info? := const)
+              res.commitCheckEnv res.asyncEnv
+              setEnv res.mainEnv
+              i := i + 1
+
          let replaceIndFVars (e : Expr) : MetaM Expr := do
            let indFVar2Const := mkIndFVar2Const views indFVars levelParams
            return (← instantiateMVars e).replace fun e' =>
--- a/src/Lean/Elab/PreDefinition/EqUnfold.lean
+++ b/src/Lean/Elab/PreDefinition/EqUnfold.lean
@@ -22,32 +22,36 @@ Returns the "const unfold" theorem (`f.eq_unfold`) for the given declaration.
 This is not extensible, and always builds on the unfold theorem (`f.eq_def`).
 -/
 def getConstUnfoldEqnFor? (declName : Name) : MetaM (Option Name) := do
-  let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) declName | return none
-  let info ← getConstInfo unfoldEqnName
-  let type ← forallTelescope info.type fun xs eq => do
-    let some (_, lhs, rhs) := eq.eq? | throwError "Unexpected unfold theorem type {info.type}"
-    unless lhs.getAppFn.isConstOf declName do
-     throwError "Unexpected unfold theorem type {info.type}"
-    unless lhs.getAppArgs == xs do
-     throwError "Unexpected unfold theorem type {info.type}"
-    let type ← mkEq lhs.getAppFn (← mkLambdaFVars xs rhs)
-    return type
-  let value ← withNewMCtxDepth do
-    let main ← mkFreshExprSyntheticOpaqueMVar type
-    if (← tryURefl main.mvarId!) then -- try to make a rfl lemma if possible
-      instantiateMVars main
-    else forallTelescope info.type fun xs _eq => do
-      let mut proof ← mkConstWithLevelParams unfoldEqnName
-      proof := mkAppN proof xs
-      for x in xs.reverse do
-        proof ← mkLambdaFVars #[x] proof
-        proof ← mkAppM ``funext #[proof]
-      return proof
+  if (← getUnfoldEqnFor? (nonRec := true) declName).isNone then
+    return none
  let name := .str declName eqUnfoldThmSuffix
-  addDecl <| Declaration.thmDecl {
-    name, type, value
-    levelParams := info.levelParams
-  }
+  realizeConst declName name do
+    -- we have to call `getUnfoldEqnFor?` again to make `unfoldEqnName` available in this context
+    let some unfoldEqnName ← getUnfoldEqnFor? (nonRec := true) declName | unreachable!
+    let info ← getConstInfo unfoldEqnName
+    let type ← forallTelescope info.type fun xs eq => do
+      let some (_, lhs, rhs) := eq.eq? | throwError "Unexpected unfold theorem type {info.type}"
+      unless lhs.getAppFn.isConstOf declName do
+        throwError "Unexpected unfold theorem type {info.type}"
+      unless lhs.getAppArgs == xs do
+        throwError "Unexpected unfold theorem type {info.type}"
+      let type ← mkEq lhs.getAppFn (← mkLambdaFVars xs rhs)
+      return type
+    let value ← withNewMCtxDepth do
+      let main ← mkFreshExprSyntheticOpaqueMVar type
+      if (← tryURefl main.mvarId!) then -- try to make a rfl lemma if possible
+        instantiateMVars main
+      else forallTelescope info.type fun xs _eq => do
+        let mut proof ← mkConstWithLevelParams unfoldEqnName
+        proof := mkAppN proof xs
+        for x in xs.reverse do
+          proof ← mkLambdaFVars #[x] proof
+          proof ← mkAppM ``funext #[proof]
+        return proof
+    addDecl <| Declaration.thmDecl {
+      name, type, value
+      levelParams := info.levelParams
+    }
  return some name


--- a/src/Lean/Elab/PreDefinition/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Eqns.lean
@@ -416,13 +416,18 @@ def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (
    trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}"
    let name := (Name.str declName eqnThmSuffixBase).appendIndexAfter (i+1)
    thmNames := thmNames.push name
+    -- determinism: `type` should be independent of the environment changes since `baseName` was
+    -- added
+    realizeConst declName name (doRealize name info type)
+  return thmNames
+where
+  doRealize name info type := withOptions (tactic.hygienic.set · false) do
    let value ← mkEqnProof declName type tryRefl
    let (type, value) ← removeUnusedEqnHypotheses type value
    addDecl <| Declaration.thmDecl {
      name, type, value
      levelParams := info.levelParams
    }
-  return thmNames

 /--
  Auxiliary method for `mkUnfoldEq`. The structure is based on `mkEqnTypes`.
@@ -465,9 +470,12 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
  go mvarId

 /-- Generate the "unfold" lemma for `declName`. -/
-def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {} {} do
-  withOptions (tactic.hygienic.set · false) do
-    let baseName := declName
+def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := do
+  let name := Name.str declName unfoldThmSuffix
+  realizeConst declName name (doRealize name)
+  return name
+where
+  doRealize name := withOptions (tactic.hygienic.set · false) do
    lambdaTelescope info.value fun xs body => do
      let us := info.levelParams.map mkLevelParam
      let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -475,12 +483,10 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
      mkUnfoldProof declName goal.mvarId!
      let type ← mkForallFVars xs type
      let value ← mkLambdaFVars xs (← instantiateMVars goal)
-      let name := Name.str baseName unfoldThmSuffix
      addDecl <| Declaration.thmDecl {
        name, type, value
        levelParams := info.levelParams
      }
-      return name

 def getUnfoldFor? (declName : Name) (getInfo? : Unit → Option EqnInfoCore) : MetaM (Option Name) := do
  if let some info := getInfo? () then
--- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean
@@ -68,9 +68,12 @@ private def rwFixEq (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
  return mvarNew.mvarId!

 /-- Generate the "unfold" lemma for `declName`. -/
-def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := withLCtx {} {} do
-  withOptions (tactic.hygienic.set · false) do
-    let baseName := declName
+def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := do
+  let name := Name.str declName unfoldThmSuffix
+  realizeConst declName name (doRealize name)
+  return name
+where
+  doRealize name := withOptions (tactic.hygienic.set · false) do
    lambdaTelescope info.value fun xs body => do
      let us := info.levelParams.map mkLevelParam
      let type ← mkEq (mkAppN (Lean.mkConst declName us) xs) body
@@ -92,12 +95,10 @@ def mkUnfoldEq (declName : Name) (info : EqnInfo) : MetaM Name := withLCtx {} {}
          throwError "failed to generate unfold theorem for '{declName}':\n{e.toMessageData}"
      let type ← mkForallFVars xs type
      let value ← mkLambdaFVars xs goal
-      let name := Name.str baseName unfoldThmSuffix
      addDecl <| Declaration.thmDecl {
        name, type, value
        levelParams := info.levelParams
      }
-      return name

 def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
  let name := Name.str declName unfoldThmSuffix
--- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean
@@ -75,13 +75,18 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
    trace[Elab.definition.structural.eqns] "eqnType {i}: {type}"
    let name := (Name.str baseName eqnThmSuffixBase).appendIndexAfter (i+1)
    thmNames := thmNames.push name
+    -- determinism: `type` should be independent of the environment changes since `baseName` was
+    -- added
+    realizeConst baseName name (doRealize name type)
+  return thmNames
+where
+  doRealize name type := withOptions (tactic.hygienic.set · false) do
    let value ← mkProof info.declName type
    let (type, value) ← removeUnusedEqnHypotheses type value
    addDecl <| Declaration.thmDecl {
      name, type, value
      levelParams := info.levelParams
    }
-  return thmNames

 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension

--- a/src/Lean/Elab/PreDefinition/TerminationMeasure.lean
+++ b/src/Lean/Elab/PreDefinition/TerminationMeasure.lean
@@ -52,7 +52,6 @@ Elaborates a `TerminationBy` to an `TerminationMeasure`.
 def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams : Nat)
    (hint : TerminationBy) : TermElabM TerminationMeasure := withDeclName funName do
  assert! extraParams ≤ arity
-
  if h : hint.vars.size > extraParams then
    let mut msg := m!"{parameters hint.vars.size} bound in `termination_by`, but the body of " ++
      m!"{funName} only binds {parameters extraParams}."
@@ -64,7 +63,7 @@ def TerminationMeasure.elab (funName : Name) (type : Expr) (arity extraParams :

  -- Bring parameters before the colon into scope
  let r ← withoutErrToSorry <|
-    forallBoundedTelescope type (arity - extraParams) fun ys type' => do
+    forallBoundedTelescope (cleanupAnnotations := true) type (arity - extraParams) fun ys type' => do
      -- Bring the variables bound by `termination_by` into scope.
      elabFunBinders hint.vars (some type') fun xs type' => do
        -- Elaborate the body in this local environment
--- a/src/Lean/Elab/PreDefinition/WF/Unfold.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Unfold.lean
@@ -75,8 +75,9 @@ private partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Un
        throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}"

 def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessProof : Simp.Result) : MetaM Unit := do
+  let baseName := preDef.declName
+  let name := Name.str baseName unfoldThmSuffix
  withOptions (tactic.hygienic.set · false) do
-    let baseName := preDef.declName
    lambdaTelescope preDef.value fun xs body => do
      let us := preDef.levelParams.map mkLevelParam
      let lhs := mkAppN (Lean.mkConst preDef.declName us) xs
@@ -93,7 +94,6 @@ def mkUnfoldEq (preDef : PreDefinition) (unaryPreDefName : Name) (wfPreprocessPr
      let value ← instantiateMVars main
      let type ← mkForallFVars xs type
      let value ← mkLambdaFVars xs value
-      let name := Name.str baseName unfoldThmSuffix
      addDecl <| Declaration.thmDecl {
        name, type, value
        levelParams := preDef.levelParams
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean
@@ -33,13 +33,7 @@ structure TacticContext where
  config : BVDecideConfig

 def TacticContext.new (lratPath : System.FilePath) (config : BVDecideConfig) :
-    Lean.Elab.TermElabM TacticContext := do
-  -- Account for: https://github.com/arminbiere/cadical/issues/112
-  let config :=
-    if System.Platform.isWindows then
-      { config with binaryProofs := false }
-    else
-      config
+    TermElabM TacticContext := do
  let exprDef ← Lean.Elab.Term.mkAuxName `_expr_def
  let certDef ← Lean.Elab.Term.mkAuxName `_cert_def
  let reflectionDef ← Lean.Elab.Term.mkAuxName `_reflection_def
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1820,42 +1820,24 @@ def addAutoBoundImplicitsInlayHint (autos : Array Expr) (inlayHintPos : String.P
    return
  let autoNames ← autos.mapM (·.fvarId!.getUserName)
  let formattedHint := s!" \{{" ".intercalate <| Array.toList <| autoNames.map toString}}"
-  let autoLabelParts : List (InlayHintLabelPart × Option Expr) := Array.toList <| ← autos.mapM fun auto => do
-    let name := toString <| ← auto.fvarId!.getUserName
-    return ({ value := name }, some auto)
-  let p value : InlayHintLabelPart × Option Expr := ({ value }, none)
-  let labelParts := [p " ", p "{"] ++ [p " "].intercalate (autoLabelParts.map ([·])) ++ [p "}"]
-  let labelParts := labelParts.toArray
  let deferredResolution ih := do
-    let .parts ps := ih.label
-      | return ih
-    let mut ps' := #[]
-    for h : i in [:ps.size] do
-      let p := ps[i]
-      let some (part, some auto) := labelParts[i]?
-        | ps' := ps'.push p
-          continue
+    let description := "Automatically-inserted implicit parameters:"
+    let codeBlockStart := "```lean"
+    let typeInfos ← autos.mapM fun auto => do
+      let name := toString <| ← auto.fvarId!.getUserName
      let type := toString <| ← Meta.ppExpr <| ← instantiateMVars (← inferType auto)
-      let tooltip := s!"{part.value} : {type}"
-      ps' := ps'.push { p with tooltip? := tooltip }
-      let some separatorPart := ps'[ps'.size - 2]?
-        | continue
-      -- We assign the leading `{` and the separation spaces the same tooltip as the auto-implicit
-      -- following it. The reason for this is that VS Code does not display a text cursor
-      -- on auto-implicits, but a regular cursor, and hitting single character auto-implicits
-      -- with that cursor can be a bit tricky. Adding the leading space or the opening `{` to the
-      -- tooltip area makes this much easier.
-      ps' := ps'.set! (ps'.size - 2) { separatorPart with tooltip? := tooltip }
-    return { ih with label := .parts ps' }
+      return s!"{name} : {type}"
+    let codeBlockEnd := "```"
+    let tooltip := "\n".intercalate <| description :: codeBlockStart :: typeInfos.toList ++ [codeBlockEnd]
+    return { ih with tooltip? := tooltip }
  pushInfoLeaf <| .ofCustomInfo {
      position := inlayHintPos
-      label := .parts <| labelParts.map (·.1)
+      label := .name formattedHint
      textEdits := #[{
        range := ⟨inlayHintPos, inlayHintPos⟩,
        newText := formattedHint
      }]
      kind? := some .parameter
-      tooltip? := "Automatically-inserted implicit parameters"
      lctx := ← getLCtx
      deferredResolution
      : InlayHint
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -420,13 +420,18 @@ private def AsyncContext.mayContain (ctx : AsyncContext) (n : Name) : Bool :=
 /--
 Constant info and environment extension states eventually resulting from async elaboration.
 -/
-structure AsyncConst where
+private structure AsyncConst where
  constInfo : AsyncConstantInfo
  /--
  Reported extension state eventually fulfilled by promise; may be missing for tasks (e.g. kernel
  checking) that can eagerly guarantee they will not report any state.
  -/
  exts?     : Option (Task (Array EnvExtensionState))
+  /--
+  `Task AsyncConsts` except for problematic recursion. The set of nested constants created while
+  elaborating this constant.
+  -/
+  consts    : Task Dynamic

 /-- Data structure holding a sequence of `AsyncConst`s optimized for efficient access. -/
 private structure AsyncConsts where
@@ -436,7 +441,7 @@ private structure AsyncConsts where
  map : NameMap AsyncConst
  /-- Trie of declaration names without private name prefixes for fast longest-prefix access. -/
  normalizedTrie : NameTrie AsyncConst
-deriving Inhabited
+deriving Inhabited, TypeName

 private def AsyncConsts.add (aconsts : AsyncConsts) (aconst : AsyncConst) : AsyncConsts :=
  let normalizedName := privateToUserName aconst.constInfo.name
@@ -459,6 +464,17 @@ private def AsyncConsts.findPrefix? (aconsts : AsyncConsts) (declName : Name) :
  -- `findLongestPrefix?`
  aconsts.normalizedTrie.findLongestPrefix? (privateToUserName declName)

+/--
+Finds constants including from other elaboration branches by recursively looking up longest
+prefixes (which is sufficient by `AsyncContext.mayContain`).
+-/
+private partial def AsyncConsts.findRec? (aconsts : AsyncConsts) (declName : Name) : Option AsyncConst := do
+  let c ← aconsts.findPrefix? declName
+  if c.constInfo.name == declName then
+    return c
+  let aconsts ← c.consts.get.get? AsyncConsts
+  AsyncConsts.findRec? aconsts declName
+
 /-- Context for `realizeConst` established by `enableRealizationsForConst`. -/
 private structure RealizationContext where
  /--
@@ -487,23 +503,23 @@ structure Environment where
  -/
  private mk ::
  /--
-  Kernel environment not containing any asynchronously elaborated declarations. Also stores
-  environment extension state for the current branch of the environment.
+  Kernel environment containing imported constants. Also stores environment extension state for the
+  current branch of the environment.

-  Ignoring extension state, this is guaranteed to be some prior version of `checked` that is eagerly
-  available. Thus we prefer taking information from it instead of `checked` whenever possible.
+  As `base` is eagerly available, we prefer taking information from it instead of `checked` whenever
+  possible.
  -/
-  checkedWithoutAsync : Kernel.Environment
+  base : Kernel.Environment
  /--
  Kernel environment task that is fulfilled when all asynchronously elaborated declarations are
  finished, containing the resulting environment. Also collects the environment extension state of
  all environment branches that contributed contained declarations.
  -/
-  checked             : Task Kernel.Environment := .pure checkedWithoutAsync
+  checked             : Task Kernel.Environment := .pure base
  /--
  Container of asynchronously elaborated declarations. For consistency, `updateBaseAfterKernelAdd`
-  makes sure this contains constants added even synchronously, i.e. this is a superset of
-  `checkedWithoutAsync` except for imported constants.
+  makes sure this contains constants added even synchronously, i.e. `base ⨃ asyncConsts` is the set
+  of constants known on the current environment branch, which is a subset of `checked`.
  -/
  private asyncConsts : AsyncConsts := default
  /-- Information about this asynchronous branch of the environment, if any. -/
@@ -526,7 +542,7 @@ namespace Environment
 -- used only when the kernel calls into the interpreter, and in `Lean.Kernel.Exception.mkCtx`
@[export lean_elab_environment_of_kernel_env]
 def ofKernelEnv (env : Kernel.Environment) : Environment :=
-  { checkedWithoutAsync := env, realizedImportedConsts? := none }
+  { base := env, realizedImportedConsts? := none }

@[export lean_elab_environment_to_kernel_env]
 def toKernelEnv (env : Environment) : Kernel.Environment :=
@@ -534,11 +550,11 @@ def toKernelEnv (env : Environment) : Kernel.Environment :=

 /-- Consistently updates synchronous and asynchronous parts of the environment without blocking. -/
 private def modifyCheckedAsync (env : Environment) (f : Kernel.Environment → Kernel.Environment) : Environment :=
-  { env with checked := env.checked.map (sync := true) f, checkedWithoutAsync := f env.checkedWithoutAsync }
+  { env with checked := env.checked.map (sync := true) f, base := f env.base }

 /-- Sets synchronous and asynchronous parts of the environment to the given kernel environment. -/
 private def setCheckedSync (env : Environment) (newChecked : Kernel.Environment) : Environment :=
-  { env with checked := .pure newChecked, checkedWithoutAsync := newChecked }
+  { env with checked := .pure newChecked, base := newChecked }

 /-- True while inside `realizeConst`'s `realize`. -/
 def isRealizing (env : Environment) : Bool :=
@@ -574,7 +590,7 @@ def addDeclCore (env : Environment) (maxHeartbeats : USize) (decl : @& Declarati
    (cancelTk? : @& Option IO.CancelToken) (doCheck := true) :
    Except Kernel.Exception Environment := do
  if let some ctx := env.asyncCtx? then
-    if let some n := decl.getNames.find? (!ctx.mayContain ·) then
+    if let some n := decl.getTopLevelNames.find? (!ctx.mayContain ·) then
      throw <| .other s!"cannot add declaration {n} to environment as it is restricted to the \
        prefix {ctx.declPrefix}"
  if doCheck then
@@ -593,7 +609,12 @@ def const2ModIdx (env : Environment) : Std.HashMap Name ModuleIdx :=
 -- only needed for the lakefile.lean cache
@[export lake_environment_add]
 private def lakeAdd (env : Environment) (cinfo : ConstantInfo) : Environment :=
-  env.setCheckedSync <| env.checked.get.add cinfo
+  let env := env.setCheckedSync <| env.checked.get.add cinfo
+  { env with asyncConsts := env.asyncConsts.add {
+    constInfo := .ofConstantInfo cinfo
+    exts? := none
+    consts := .pure <| .mk (α := AsyncConsts) default
+  } }

 /--
 Save an extra constant name that is used to populate `const2ModIdx` when we import
@@ -606,48 +627,44 @@ def addExtraName (env : Environment) (name : Name) : Environment :=
  else
    env.modifyCheckedAsync fun env => { env with extraConstNames := env.extraConstNames.insert name }

-/-- Find base case: name did not match any asynchronous declaration. -/
-private def findNoAsync (env : Environment) (n : Name) : Option ConstantInfo := do
+/-- `findAsync?` after `base` access -/
+private def findAsync?' (env : Environment) (n : Name) : Option AsyncConstantInfo := do
+  if let some asyncConst := env.asyncConsts.find? n then
+    -- Constant for which an asynchronous elaboration task was spawned
+    return asyncConst.constInfo
  if env.asyncMayContain n then
    -- Constant definitely not generated in a different environment branch: return none, callers
    -- have already checked this branch.
    none
-  else if let some _ := env.asyncConsts.findPrefix? n then
+  if let some c := env.asyncConsts.findRec? n then
    -- Constant generated in a different environment branch: wait for final kernel environment. Rare
    -- case when only proofs are elaborated asynchronously as they are rarely inspected. Could be
    -- optimized in the future by having the elaboration thread publish an (incremental?) map of
    -- generated declarations before kernel checking (which must wait on all previous threads).
-    env.checked.get.constants.find?' n
-  else
-    -- Not in the kernel environment nor in the name prefix of environment branch: undefined by
-    -- `addDeclCore` invariant.
-    none
+    return c.constInfo
+  -- Not in the kernel environment nor in the name prefix of environment branch: undefined by
+  -- `addDeclCore` invariant.
+  none

 /--
 Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration
 tasks unless necessary.
 -/
 def findAsync? (env : Environment) (n : Name) : Option AsyncConstantInfo := do
-  -- Check declarations already added to the kernel environment (e.g. because they were imported)
-  -- first as that should be the most common case. It is safe to use `find?'` because we never
-  -- overwrite imported declarations.
-  if let some c := env.checkedWithoutAsync.constants.find?' n then
-    some <| .ofConstantInfo c
-  else if let some asyncConst := env.asyncConsts.find? n then
-    -- Constant for which an asynchronous elaboration task was spawned
-    return asyncConst.constInfo
-  else env.findNoAsync n |>.map .ofConstantInfo
+  -- Avoid going through `AsyncConstantInfo` for `base` access
+  if let some c := env.base.constants.map₁[n]? then
+    return .ofConstantInfo c
+  findAsync?' env n

 /--
 Looks up the given declaration name in the environment, avoiding forcing any in-progress elaboration
 tasks for declaration bodies (which are not accessible from `ConstantVal`).
 -/
 def findConstVal? (env : Environment) (n : Name) : Option ConstantVal := do
-  if let some c := env.checkedWithoutAsync.constants.find?' n then
-    some c.toConstantVal
-  else if let some asyncConst := env.asyncConsts.find? n then
-    return asyncConst.constInfo.toConstantVal
-  else env.findNoAsync n |>.map (·.toConstantVal)
+  -- Avoid going through `AsyncConstantInfo` for `base` access
+  if let some c := env.base.constants.map₁[n]? then
+    return c.toConstantVal
+  env.findAsync?' n |>.map (·.toConstantVal)

 /--
 Allows `realizeConst` calls for imported declarations in all derived environment branches.
@@ -697,13 +714,10 @@ def enableRealizationsForConst (env : Environment) (opts : Options) (c : Name) :
 Looks up the given declaration name in the environment, blocking on the corresponding elaboration
 task if not yet complete.
 -/
-def find? (env : Environment) (n : Name) : Option ConstantInfo :=
-  if let some c := env.checkedWithoutAsync.constants.find?' n then
-    some c
-  else if let some asyncConst := env.asyncConsts.find? n then
-    return asyncConst.constInfo.toConstantInfo
-  else
-    env.findNoAsync n
+def find? (env : Environment) (n : Name) : Option ConstantInfo := do
+  if let some c := env.base.constants.map₁[n]? then
+    return c
+  env.findAsync?' n |>.map (·.toConstantInfo)

 /-- Returns debug output about the asynchronous state of the environment. -/
 def dbgFormatAsyncState (env : Environment) : BaseIO String :=
@@ -716,7 +730,7 @@ def dbgFormatAsyncState (env : Environment) : BaseIO String :=
  \nrealizedImportedConsts?: {repr <| (← env.realizedImportedConsts?.mapM fun ctx => do
    return (← ctx.constsRef.get).toList.map fun (n, m?) =>
      (n, m?.get.1.map (fun c : AsyncConst => c.constInfo.name.toString) |> toString))}
-  \ncheckedWithoutAsync.constants.map₂: {repr <| env.checkedWithoutAsync.constants.map₂.toList.map (·.1)}"
+  \nbase.constants.map₂: {repr <| env.base.constants.map₂.toList.map (·.1)}"

 /-- Returns debug output about the synchronous state of the environment. -/
 def dbgFormatCheckedSyncState (env : Environment) : BaseIO String :=
@@ -792,6 +806,7 @@ structure AddConstAsyncResult where
  private infoPromise : IO.Promise ConstantInfo
  private extensionsPromise : IO.Promise (Array EnvExtensionState)
  private checkedEnvPromise : IO.Promise Kernel.Environment
+  private constsPromise : IO.Promise AsyncConsts

 /-- Creates fallback info to be used in case promises are dropped unfulfilled. -/
 private def mkFallbackConstInfo (constName : Name) (kind : ConstantKind) : ConstantInfo :=
@@ -833,17 +848,23 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (
  let infoPromise ← IO.Promise.new
  let extensionsPromise ← IO.Promise.new
  let checkedEnvPromise ← IO.Promise.new
+  let constsPromise ← IO.Promise.new

-  let fallbackConstInfo := mkFallbackConstInfo constName kind
+  -- We use a thunk here because we don't have a fallback for recursors, but that specific
+  -- invocation cannot fail anyway
+  let fallbackConstInfo := Thunk.mk fun _ => mkFallbackConstInfo constName kind

  let asyncConst := {
    constInfo := {
      name := constName
      kind
-      sig := sigPromise.resultD fallbackConstInfo.toConstantVal
-      constInfo := infoPromise.resultD fallbackConstInfo
+      sig := sigPromise.resultD fallbackConstInfo.get.toConstantVal
+      constInfo := infoPromise.resultD fallbackConstInfo.get
    }
    exts? := guard reportExts *> some (extensionsPromise.resultD env.toKernelEnv.extensions)
+    consts := constsPromise.result?.map (sync := true) fun
+      | some consts => .mk consts
+      | none        => .mk (α := AsyncConsts) default
  }
  return {
    constName, kind
@@ -853,7 +874,7 @@ def addConstAsync (env : Environment) (constName : Name) (kind : ConstantKind) (
        | some kenv => .pure kenv
        | none      => env.checked }
    asyncEnv := env.enterAsync constName
-    sigPromise, infoPromise, extensionsPromise, checkedEnvPromise
+    sigPromise, infoPromise, extensionsPromise, checkedEnvPromise, constsPromise
  }

 /--
@@ -868,8 +889,9 @@ def AddConstAsyncResult.commitSignature (res : AddConstAsyncResult) (sig : Const
  res.sigPromise.resolve sig

 /--
-Commits the full constant info to the main environment branch. If `info?` is `none`, it is taken
-from the given environment. The declaration name and kind must match the original values given to
+Commits the full constant info as well as the current environment extension state and set of nested
+asynchronous constants to the main environment branch. If `info?` is `none`, it is taken from the
+given environment. The declaration name and kind must match the original values given to
 `addConstAsync`. The signature must match the previous `commitSignature` call, if any.
 -/
 def AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environment)
@@ -889,7 +911,8 @@ def AddConstAsyncResult.commitConst (res : AddConstAsyncResult) (env : Environme
  if sig.type != info.type then
    throw <| .userError s!"AddConstAsyncResult.commitConst: constant has type {info.type} but expected {sig.type}"
  res.infoPromise.resolve info
-  res.extensionsPromise.resolve env.checkedWithoutAsync.extensions
+  res.extensionsPromise.resolve env.base.extensions
+  res.constsPromise.resolve env.asyncConsts

 /--
 Assuming `Lean.addDecl` has been run for the constant to be added on the async environment branch,
@@ -899,10 +922,10 @@ kernel additions there. All `commitConst` preconditions apply.
 -/
 def AddConstAsyncResult.commitCheckEnv (res : AddConstAsyncResult) (env : Environment) :
    IO Unit := do
-  let some _ := env.findAsync? res.constName
-    | throw <| .userError s!"AddConstAsyncResult.checkAndCommitEnv: constant {res.constName} not \
-      found in async context"
-  res.commitConst env
+  -- We should skip `commitConst` in case it has already been called, perhaps with a different
+  -- `info?`
+  if !(← res.infoPromise.isResolved) then
+    res.commitConst env
  res.checkedEnvPromise.resolve env.checked.get

 def contains (env : Environment) (n : Name) : Bool :=
@@ -913,11 +936,11 @@ Checks whether the given declaration is known on the current branch, in which ca
 not block.
 -/
 def containsOnBranch (env : Environment) (n : Name) : Bool :=
-  (env.asyncConsts.find? n |>.isSome) || env.checkedWithoutAsync.constants.contains n
+  (env.asyncConsts.find? n |>.isSome) || env.base.constants.contains n

 def header (env : Environment) : EnvironmentHeader :=
  -- can be assumed to be in sync with `env.checked`; see `setMainModule`, the only modifier of the header
-  env.checkedWithoutAsync.header
+  env.base.header

 def imports (env : Environment) : Array Import :=
  env.header.imports
@@ -936,7 +959,7 @@ def mainModule (env : Environment) : Name :=

 def getModuleIdxFor? (env : Environment) (declName : Name) : Option ModuleIdx :=
  -- async constants are always from the current module
-  env.checkedWithoutAsync.const2ModIdx[declName]?
+  env.base.const2ModIdx[declName]?

 def isConstructor (env : Environment) (declName : Name) : Bool :=
  match env.find? declName with
@@ -1115,9 +1138,9 @@ def modifyState {σ : Type} (ext : EnvExtension σ) (env : Environment) (f : σ
    if let some asyncCtx := env.asyncCtx? then
      return panic! s!"environment extension is marked as `mainOnly` but used in \
        {if asyncCtx.realizing then "realization" else "async"} context '{asyncCtx.declPrefix}'"
-    return { env with checkedWithoutAsync.extensions := unsafe ext.modifyStateImpl env.checkedWithoutAsync.extensions f }
+    return { env with base.extensions := unsafe ext.modifyStateImpl env.base.extensions f }
  | .local =>
-    return { env with checkedWithoutAsync.extensions := unsafe ext.modifyStateImpl env.checkedWithoutAsync.extensions f }
+    return { env with base.extensions := unsafe ext.modifyStateImpl env.base.extensions f }
  | _ =>
    if ext.replay?.isNone then
      if let some asyncCtx := env.asyncCtx?.filter (·.realizing) then
@@ -1141,7 +1164,7 @@ private unsafe def getStateUnsafe {σ : Type} [Inhabited σ] (ext : EnvExtension
  | .sync     => ext.getStateImpl env.checked.get.extensions
  | .async    => panic! "called on `async` extension, use `findStateAsync` \
    instead or pass `(asyncMode := .local)` to explicitly access local state"
-  | _         => ext.getStateImpl env.checkedWithoutAsync.extensions
+  | _         => ext.getStateImpl env.base.extensions

 /--
 Returns the current extension state. See `AsyncMode` for details on how modifications from
@@ -1157,10 +1180,10 @@ opaque getState {σ : Type} [Inhabited σ] (ext : EnvExtension σ) (env : Enviro
 private unsafe def findStateAsyncUnsafe {σ : Type} [Inhabited σ]
    (ext : EnvExtension σ) (env : Environment) (declPrefix : Name) : σ :=
  -- safety: `ext`'s constructor is private, so we can assume the entry at `ext.idx` is of type `σ`
-  if let some { exts? := some exts, .. } := env.asyncConsts.findPrefix? declPrefix then
+  if let some { exts? := some exts, .. } := env.asyncConsts.findRec? declPrefix then
    ext.getStateImpl exts.get
  else
-    ext.getStateImpl env.checkedWithoutAsync.extensions
+    ext.getStateImpl env.base.extensions

 /--
 Returns the final extension state on the environment branch corresponding to the passed declaration
@@ -1200,7 +1223,7 @@ def mkEmptyEnvironment (trustLevel : UInt32 := 0) : IO Environment := do
  if initializing then throw (IO.userError "environment objects cannot be created during initialization")
  let exts ← mkInitialExtensionStates
  return {
-    checkedWithoutAsync := {
+    base := {
      const2ModIdx    := {}
      constants       := {}
      header          := { trustLevel }
@@ -1559,7 +1582,7 @@ def mkExtNameMap (startingAt : Nat) : IO (Std.HashMap Name Nat) := do
 private def setImportedEntries (env : Environment) (mods : Array ModuleData) (startingAt : Nat := 0) : IO Environment := do
  -- We work directly on the states array instead of `env` as `Environment.modifyState` introduces
  -- significant overhead on such frequent calls
-  let mut states := env.checkedWithoutAsync.extensions
+  let mut states := env.base.extensions
  let extDescrs ← persistentEnvExtensionsRef.get
  /- For extensions starting at `startingAt`, ensure their `importedEntries` array have size `mods.size`. -/
  for extDescr in extDescrs[startingAt:] do
@@ -1575,7 +1598,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
        -- safety: as in `modifyState`
        states := unsafe extDescrs[entryIdx]!.toEnvExtension.modifyStateImpl states fun s =>
          { s with importedEntries := s.importedEntries.set! modIdx entries }
-  return env.setCheckedSync { env.checkedWithoutAsync with extensions := states }
+  return env.setCheckedSync { env.base with extensions := states }

 /--
  "Forward declaration" needed for updating the attribute table with user-defined attributes.
@@ -1591,7 +1614,7 @@ private def setImportedEntries (env : Environment) (mods : Array ModuleData) (st
@[extern 1 "lean_get_num_attributes"] opaque getNumBuiltinAttributes : IO Nat

 private def ensureExtensionsArraySize (env : Environment) : IO Environment := do
-  let exts ← EnvExtension.ensureExtensionsArraySize env.checkedWithoutAsync.extensions
+  let exts ← EnvExtension.ensureExtensionsArraySize env.base.extensions
  return env.modifyCheckedAsync ({ · with extensions := exts })

 private partial def finalizePersistentExtensions (env : Environment) (mods : Array ModuleData) (opts : Options) : IO Environment := do
@@ -1711,7 +1734,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) (
  let constants : ConstMap := SMap.fromHashMap constantMap false
  let exts ← mkInitialExtensionStates
  let mut env : Environment := {
-    checkedWithoutAsync := {
+    base := {
      const2ModIdx, constants
      quotInit        := !imports.isEmpty -- We assume `core.lean` initializes quotient module
      extraConstNames := {}
@@ -1795,7 +1818,7 @@ def Kernel.enableDiag (env : Lean.Environment) (flag : Bool) : Lean.Environment
  env.modifyCheckedAsync (·.enableDiag flag)

 def Kernel.isDiagnosticsEnabled (env : Lean.Environment) : Bool :=
-  env.checkedWithoutAsync.isDiagnosticsEnabled
+  env.base.isDiagnosticsEnabled

 def Kernel.resetDiag (env : Lean.Environment) : Lean.Environment :=
  env.modifyCheckedAsync (·.resetDiag)
@@ -1821,16 +1844,16 @@ def getNamespaceSet (env : Environment) : NameSSet :=
  namespacesExt.getState env

@[export lean_elab_environment_update_base_after_kernel_add]
-private def updateBaseAfterKernelAdd (env : Environment) (kernel : Kernel.Environment) (decl : Declaration) : Environment :=
+private def updateBaseAfterKernelAdd (env : Environment) (kenv : Kernel.Environment) (decl : Declaration) : Environment :=
  { env with
-    checked := .pure kernel
-    checkedWithoutAsync := { kernel with extensions := env.checkedWithoutAsync.extensions }
+    checked := .pure kenv
    -- make constants available in `asyncConsts` as well; see its docstring
    asyncConsts := decl.getNames.foldl (init := env.asyncConsts) fun asyncConsts n =>
      if asyncConsts.find? n |>.isNone then
        asyncConsts.add {
-          constInfo := .ofConstantInfo (kernel.find? n |>.get!)
+          constInfo := .ofConstantInfo (kenv.find? n |>.get!)
          exts? := none
+          consts := .pure <| .mk (α := AsyncConsts) default
        }
      else asyncConsts }

@@ -1842,7 +1865,7 @@ def displayStats (env : Environment) : IO Unit := do
  IO.println ("number of memory-mapped modules:       " ++ toString (env.header.regions.filter (·.isMemoryMapped) |>.size));
  IO.println ("number of buckets for imported consts: " ++ toString env.constants.numBuckets);
  IO.println ("trust level:                           " ++ toString env.header.trustLevel);
-  IO.println ("number of extensions:                  " ++ toString env.checkedWithoutAsync.extensions.size);
+  IO.println ("number of extensions:                  " ++ toString env.base.extensions.size);
  pExtDescrs.forM fun extDescr => do
    IO.println ("extension '" ++ toString extDescr.name ++ "'")
    let s := extDescr.toEnvExtension.getState env
@@ -1887,7 +1910,7 @@ def realizeConst (env : Environment) (forConst : Name) (constName : Name)
    IO (Environment × Dynamic) := do
  let mut env := env
  -- find `RealizationContext` for `forConst` in `realizedImportedConsts?` or `realizedLocalConsts`
-  let ctx ← if env.checkedWithoutAsync.const2ModIdx.contains forConst then
+  let ctx ← if env.base.const2ModIdx.contains forConst then
    env.realizedImportedConsts?.getDM <|
      throw <| .userError s!"Environment.realizeConst: `realizedImportedConsts` is empty"
  else
@@ -1928,7 +1951,7 @@ def realizeConst (env : Environment) (forConst : Name) (constName : Name)
      let consts := realizeEnv'.asyncConsts.revList.take numNewConsts |>.reverse
      let consts := consts.map fun c =>
        if c.exts?.isNone then
-          { c with exts? := some <| .pure realizeEnv'.checkedWithoutAsync.extensions }
+          { c with exts? := some <| .pure realizeEnv'.base.extensions }
        else c
      let exts ← EnvExtension.envExtensionsRef.get
      let replay := (maybeAddToKernelEnv realizeEnv realizeEnv' consts · exts)
--- a/src/Lean/Meta/Eqns.lean
+++ b/src/Lean/Meta/Eqns.lean
@@ -141,25 +141,27 @@ structure EqnsExtState where

 /- We generate the equations on demand. -/
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
-  registerEnvExtension (pure {})
+  registerEnvExtension (pure {}) (asyncMode := .local)

 /--
 Simple equation theorem for nonrecursive definitions.
 -/
 private def mkSimpleEqThm (declName : Name) (suffix := Name.mkSimple unfoldThmSuffix) : MetaM (Option Name) := do
  if let some (.defnInfo info) := (← getEnv).find? declName then
-    lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
-      let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
-      let type  ← mkForallFVars xs (← mkEq lhs body)
-      let value ← mkLambdaFVars xs (← mkEqRefl lhs)
-      let name := declName ++ suffix
-      addDecl <| Declaration.thmDecl {
-        name, type, value
-        levelParams := info.levelParams
-      }
-      return some name
+    let name := declName ++ suffix
+    realizeConst declName name (doRealize name info)
+    return some name
  else
    return none
+where doRealize name info := do
+  lambdaTelescope (cleanupAnnotations := true) info.value fun xs body => do
+    let lhs := mkAppN (mkConst info.name <| info.levelParams.map mkLevelParam) xs
+    let type  ← mkForallFVars xs (← mkEq lhs body)
+    let value ← mkLambdaFVars xs (← mkEqRefl lhs)
+    addDecl <| Declaration.thmDecl {
+      name, type, value
+      levelParams := info.levelParams
+    }

 /--
 Returns `some declName` if `thmName` is an equational theorem for `declName`.
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -209,6 +209,12 @@ partial def UnsatProof.toExprProofCore (h : UnsatProof) : ProofM Expr := do
      return mkApp5 (mkConst ``Int.Linear.eq_unsat_coeff) (← getContext) (toExpr c.p) (toExpr (Int.ofNat k)) reflBoolTrue (← c.toExprProof)
  | .diseq c =>
    return mkApp4 (mkConst ``Int.Linear.diseq_unsat) (← getContext) (toExpr c.p) reflBoolTrue (← c.toExprProof)
+  | .cooper c₁ c₂ c₃ =>
+    let .add c _ _ := c₃.p | c₃.throwUnexpected
+    let d := c₃.d
+    let (_, α, β) := gcdExt c d
+    let h := mkApp7 (mkConst ``Int.Linear.cooper_unsat) (← getContext) (toExpr c₁.p) (toExpr c₂.p) (toExpr c₃.p) (toExpr c₃.d) (toExpr α) (toExpr β)
+    return mkApp4 h reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof) (← c₃.toExprProof)

 end

@@ -292,6 +298,7 @@ end
 def UnsatProof.collectDecVars (h : UnsatProof) : CollectDecVarsM Unit := do
  match h with
  | .le c | .dvd c | .eq c | .diseq c => c.collectDecVars
+  | .cooper c₁ c₂ c₃ => c₁.collectDecVars; c₂.collectDecVars; c₃.collectDecVars

 abbrev CollectDecVarsM.run (x : CollectDecVarsM Unit) (decVars : FVarIdSet) : FVarIdSet :=
  let (_, s) := x decVars |>.run {}
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean
@@ -279,8 +279,22 @@ def resolveRealLowerUpperConflict (c₁ c₂ : LeCnstr) : GoalM Bool := do
    c.assert
    return true

+def resolveCooperUnary (pred : CooperSplitPred) : SearchM Bool := do
+  let some c₃ := pred.c₃? | return false
+  let .add (-1) _ (.num a) := pred.c₁.p | return false
+  let .add 1 _ (.num b) := pred.c₂.p | return false
+  let .add c _ (.num e) := c₃.p | return false
+  let d := c₃.d
+  let (1, α, _) := gcdExt c d | return false
+  unless -b < Int.Linear.cdiv (a - -α * e % d) d * d + -α * e % d do
+    return false
+  setInconsistent (.cooper pred.c₁ pred.c₂ c₃)
+  return true
+
 def resolveCooperPred (pred : CooperSplitPred) : SearchM Unit := do
  trace[grind.cutsat.conflict] "[{pred.numCases}]: {← pred.pp}"
+  if (← resolveCooperUnary pred) then
+    return
  let n := pred.numCases
  let fvarId ← mkCase (.cooper pred #[] {})
  { pred, k := n - 1, h := .dec fvarId : CooperSplit }.assert
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean
@@ -182,6 +182,7 @@ inductive UnsatProof where
  | le (c : LeCnstr)
  | eq (c : EqCnstr)
  | diseq (c : DiseqCnstr)
+  | cooper (c₁ c₂ : LeCnstr) (c₃ : DvdCnstr)

 end

--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
@@ -290,5 +290,6 @@ def CooperSplitPred.pp (pred : CooperSplitPred) : GoalM MessageData := do
 def UnsatProof.pp (h : UnsatProof) : GoalM MessageData := do
  match h with
  | .le c | .eq c | .dvd c | .diseq c => c.pp
+  | .cooper c₁ c₂ c₃ => return m!"{← c₁.pp}, {← c₂.pp}, {← c₃.pp}"

 end Lean.Meta.Grind.Arith.Cutsat
--- a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
+++ b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
@@ -8,6 +8,7 @@ import Init.Grind.Util
 import Lean.Util.PtrSet
 import Lean.Meta.Basic
 import Lean.Meta.InferType
+import Lean.Meta.Tactic.Grind.Util

 namespace Lean.Meta.Grind

@@ -21,6 +22,13 @@ where
      if let some r := (← get).find? e then
        return r
      let prop ← inferType e
+      /-
+      We must unfold reducible constants occurring in `prop` because the congruence closure
+      module in `grind` assumes they have been expanded.
+      See `grind_mark_nested_proofs_bug.lean` for an example.
+      TODO: We may have to normalize `prop` too.
+      -/
+      let prop ← unfoldReducible prop
      let e' := mkApp2 (mkConst ``Lean.Grind.nestedProof) prop e
      modify fun s => s.insert e e'
      return e'
--- a/src/Lean/MonadEnv.lean
+++ b/src/Lean/MonadEnv.lean
@@ -24,10 +24,11 @@ def withEnv [Monad m] [MonadFinally m] [MonadEnv m] (env : Environment) (x : m
  finally
    setEnv saved

-def isInductive [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
-  match (← getEnv).find? declName with
-  | some (ConstantInfo.inductInfo ..) => return true
-  | _ => return false
+def isInductiveCore (env : Environment) (declName : Name) : Bool :=
+  env.find? declName matches some (.inductInfo ..)
+
+def isInductive [Monad m] [MonadEnv m] (declName : Name) : m Bool :=
+  return isInductiveCore (← getEnv) declName

 def isRecCore (env : Environment) (declName : Name) : Bool :=
  match env.find? declName with
--- a/src/Lean/Server/FileWorker/InlayHints.lean
+++ b/src/Lean/Server/FileWorker/InlayHints.lean
@@ -98,15 +98,17 @@ def applyEditToHint? (hintMod : Name) (ihi : Elab.InlayHintInfo) (range : String
  }

 structure InlayHintState where
-  oldInlayHints      : Array Elab.InlayHintInfo
-  oldFinishedSnaps   : Nat
-  lastEditTimestamp? : Option Nat
+  oldInlayHints           : Array Elab.InlayHintInfo
+  oldFinishedSnaps        : Nat
+  lastEditTimestamp?      : Option Nat
+  isFirstRequestAfterEdit : Bool
  deriving TypeName, Inhabited

 def InlayHintState.init : InlayHintState := {
  oldInlayHints := #[]
  oldFinishedSnaps := 0
  lastEditTimestamp? := none
+  isFirstRequestAfterEdit := false
 }

 def handleInlayHints (p : InlayHintParams) (s : InlayHintState) :
@@ -115,6 +117,20 @@ def handleInlayHints (p : InlayHintParams) (s : InlayHintState) :
  let text := ctx.doc.meta.text
  let range := text.lspRangeToUtf8Range p.range
  let srcSearchPath := ctx.srcSearchPath
+  if s.isFirstRequestAfterEdit then
+    -- We immediately respond to the first inlay hint request after an edit with the old inlay hints,
+    -- without waiting for the edit delay.
+    -- The reason for this is that in VS Code, when it hasn't received a new set of inlay hints,
+    -- edits to the document visually move all old inlay hints, but do not actually update other
+    -- fields, like the `textEdit` field. This means that e.g. inlay hint insertion will insert
+    -- the inlay hint at the wrong position.
+    -- To reduce the size of the window for this race condition, we attempt to minimize the delay
+    -- after an edit, providing VS Code with a set of old inlay hints that we have already updated
+    -- correctly for VS Code ASAP.
+    let lspInlayHints ← s.oldInlayHints.mapM (·.toLspInlayHint srcSearchPath text)
+    let r := { response := lspInlayHints, isComplete := false }
+    let s := { s with isFirstRequestAfterEdit := false }
+    return (r, s)
  -- We delay sending inlay hints by 3000ms to avoid inlay hint flickering on the client.
  -- VS Code already has a mechanism for this, but it is not sufficient.
  let inlayHintEditDelayMs := 3000
@@ -126,6 +142,16 @@ def handleInlayHints (p : InlayHintParams) (s : InlayHintState) :
      let timeSinceLastEditMs := timestamp - lastEditTimestamp
      inlayHintEditDelayMs - timeSinceLastEditMs
  let (snaps, _, isComplete) ← ctx.doc.cmdSnaps.getFinishedPrefixWithConsistentLatency editDelayMs.toUInt32 (cancelTk? := ctx.cancelTk.cancellationTask)
+  if ← IO.hasFinished ctx.cancelTk.cancellationTask then
+    -- Inlay hint request has been cancelled, either by a cancellation request or another edit.
+    -- In the former case, we will simply discard the result and respond with a request error
+    -- denoting cancellation.
+    -- In the latter case, we respond with the old inlay hints, since we can't respond with an error.
+    -- This is to prevent cancellation from making us serve updated inlay hints before the
+    -- edit delay has passed.
+    let lspInlayHints ← s.oldInlayHints.mapM (·.toLspInlayHint srcSearchPath text)
+    let r := { response := lspInlayHints, isComplete := false }
+    return (r, s)
  let snaps := snaps.toArray
  let finishedSnaps := snaps.size
  let oldFinishedSnaps := s.oldFinishedSnaps
@@ -170,6 +196,7 @@ def handleInlayHintsDidChange (p : DidChangeTextDocumentParams)
    oldInlayHints := updatedOldInlayHints
    oldFinishedSnaps := 0
    lastEditTimestamp?
+    isFirstRequestAfterEdit := true
  }

 where
@@ -186,8 +213,13 @@ where
      return some mod
    let modName ← match modName? with
      | .ok (some modName) => pure modName
-      | .ok none => pure .anonymous -- `.anonymous` occurs in untitled files
-      | .error err => throw <| .ofIoError err
+      -- `.anonymous` occurs in untitled files (`.ok none` case).
+      -- There is an intentional bug here where the `.error _` case spits out `.anonymous`.
+      -- This means that we don't correctly update inlay hint locations when the file for this
+      -- file worker has been deleted. As of writing this, there are no inlay hints that use this
+      -- field anyways.
+      -- In the future, we should resolve this by caching the module name in `DocumentMeta`.
+      | _ => pure .anonymous
    let mut updatedOldInlayHints := #[]
    for ihi in oldInlayHints do
      let mut ihi := ihi
--- a/src/Std/Data/DHashMap/Internal/Index.lean
+++ b/src/Std/Data/DHashMap/Internal/Index.lean
@@ -48,7 +48,7 @@ cf. https://github.com/leanprover/lean4/issues/4157
  ⟨(scrambleHash hash).toUSize &&& (sz.toUSize - 1), by
    -- This proof is a good test for our USize API
    by_cases h' : sz < USize.size
-    · rw [USize.toNat_and, USize.toNat_sub_of_le, USize.toNat_ofNat_of_lt h']
+    · rw [USize.toNat_and, USize.toNat_sub_of_le, USize.toNat_ofNat_of_lt' h']
      · exact Nat.lt_of_le_of_lt Nat.and_le_right (Nat.sub_lt h (by simp))
      · simp [USize.le_iff_toNat_le, Nat.mod_eq_of_lt h', Nat.succ_le_of_lt h]
    · exact Nat.lt_of_lt_of_le (USize.toNat_lt_size _) (Nat.le_of_not_lt h')⟩
--- a/src/Std/Tactic/BVDecide/Syntax.lean
+++ b/src/Std/Tactic/BVDecide/Syntax.lean
@@ -21,7 +21,6 @@ structure BVDecideConfig where
  trimProofs : Bool := true
  /--
  Whether to use the binary LRAT proof format.
-  Currently set to false and ignored on Windows due to a bug in CaDiCal.
  -/
  binaryProofs : Bool := true
  /--
--- a/src/lean.mk.in
+++ b/src/lean.mk.in
@@ -163,5 +163,7 @@ clean:
 .PRECIOUS: $(BC_OUT)/%.bc $(C_OUT)/%.c $(TEMP_OUT)/%.o $(TEMP_OUT)/%.o.export

 ifndef C_ONLY
+ifndef UNSAFE_ASSUME_OLD
 include $(DEPS)
 endif
+endif
--- a/stage0/stdlib/Init/Data/SInt/Lemmas.c
+++ b/stage0/stdlib/Init/Data/SInt/Lemmas.c
--- a/stage0/stdlib/Lean/Elab/Deriving/DecEq.c
+++ b/stage0/stdlib/Lean/Elab/Deriving/DecEq.c
--- a/stage0/stdlib/Lean/Elab/MutualInductive.c
+++ b/stage0/stdlib/Lean/Elab/MutualInductive.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/FixedParams.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/FixedParams.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Mutual.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Mutual.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/PartialFixpoint/Induction.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/PartialFixpoint/Induction.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/PartialFixpoint/Main.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/PartialFixpoint/Main.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/BRecOn.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/BRecOn.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Eqns.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/FindRecArg.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/FindRecArg.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/IndPred.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/IndPred.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/Main.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/Structural/RecArgInfo.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/Structural/RecArgInfo.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Eqns.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Fix.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Fix.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/GuessLex.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/GuessLex.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Main.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/PackMutual.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/PackMutual.c
--- a/stage0/stdlib/Lean/Elab/PreDefinition/WF/Rel.c
+++ b/stage0/stdlib/Lean/Elab/PreDefinition/WF/Rel.c
--- a/stage0/stdlib/Lean/Elab/Structure.c
+++ b/stage0/stdlib/Lean/Elab/Structure.c
--- a/stage0/stdlib/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.c
+++ b/stage0/stdlib/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.c
--- a/stage0/stdlib/Lean/Elab/Term.c
+++ b/stage0/stdlib/Lean/Elab/Term.c
--- a/stage0/stdlib/Lean/Environment.c
+++ b/stage0/stdlib/Lean/Environment.c
--- a/stage0/stdlib/Lean/Meta/ArgsPacker.c
+++ b/stage0/stdlib/Lean/Meta/ArgsPacker.c
--- a/stage0/stdlib/Lean/Meta/Basic.c
+++ b/stage0/stdlib/Lean/Meta/Basic.c
--- a/stage0/stdlib/Lean/Meta/Match/MatcherApp/Transform.c
+++ b/stage0/stdlib/Lean/Meta/Match/MatcherApp/Transform.c
--- a/stage0/stdlib/Lean/Meta/Tactic/FunInd.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/FunInd.c
--- a/stage0/stdlib/Lean/Meta/Tactic/FunIndInfo.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/FunIndInfo.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.c
--- a/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.c
+++ b/stage0/stdlib/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.c
--- a/stage0/stdlib/Lean/Replay.c
+++ b/stage0/stdlib/Lean/Replay.c
--- a/stage0/stdlib/Lean/Server/FileWorker/InlayHints.c
+++ b/stage0/stdlib/Lean/Server/FileWorker/InlayHints.c
--- a/stage0/stdlib/Std/Data/DHashMap/Basic.c
+++ b/stage0/stdlib/Std/Data/DHashMap/Basic.c
--- a/stage0/stdlib/Std/Data/DHashMap/Internal/RawLemmas.c
+++ b/stage0/stdlib/Std/Data/DHashMap/Internal/RawLemmas.c
--- a/stage0/stdlib/Std/Data/DHashMap/Raw.c
+++ b/stage0/stdlib/Std/Data/DHashMap/Raw.c
--- a/stage0/stdlib/Std/Data/DHashMap/RawLemmas.c
+++ b/stage0/stdlib/Std/Data/DHashMap/RawLemmas.c
--- a/stage0/stdlib/Std/Data/DTreeMap/Basic.c
+++ b/stage0/stdlib/Std/Data/DTreeMap/Basic.c
--- a/stage0/stdlib/Std/Data/DTreeMap/Internal/Lemmas.c
+++ b/stage0/stdlib/Std/Data/DTreeMap/Internal/Lemmas.c
--- a/stage0/stdlib/Std/Data/DTreeMap/Internal/Queries.c
+++ b/stage0/stdlib/Std/Data/DTreeMap/Internal/Queries.c
--- a/stage0/stdlib/Std/Data/DTreeMap/Internal/WF/Lemmas.c
+++ b/stage0/stdlib/Std/Data/DTreeMap/Internal/WF/Lemmas.c
--- a/stage0/stdlib/Std/Data/DTreeMap/Raw/Basic.c
+++ b/stage0/stdlib/Std/Data/DTreeMap/Raw/Basic.c
--- a/tests/lean/run/5667.lean
+++ b/tests/lean/run/5667.lean
@@ -32,14 +32,25 @@ error: Failed to realize constant optimize.eq_def:
  ⊢ Expr.const 0 = Expr.op bop✝ (Expr.const 0)
 ---
 error: Failed to realize constant optimize.eq_def:
-  failed to generate unfold theorem for 'optimize'
-  case h_2.h_1
-  x e1 : Expr
-  bop✝ bop_1 : Unit
-  x_1 : Expr
+  failed to generate equational theorem for 'optimize'
+  case h_2
+  e1 : Expr
  i : BitVec 32
-  heq✝ : optimize e1 = Expr.const i
-  ⊢ optimize (Expr.op bop✝ e1) = Expr.op bop✝ (Expr.const 0)
+  heq : optimize e1 = Expr.const i
+  bop✝ bop_1 : Unit
+  x : Expr
+  x_3 :
+    ∀ (i : BitVec 32),
+      (Expr.rec (fun i => ⟨Expr.const i, PUnit.unit⟩)
+              (fun op e1 e1_ih =>
+                ⟨match op, e1_ih.1 with
+                  | x, Expr.const i => Expr.op op (Expr.const 0)
+                  | x, x_1 => Expr.const 0,
+                  e1_ih⟩)
+              e1).1 =
+          Expr.const i →
+        False
+  ⊢ Expr.const 0 = Expr.op bop✝ (Expr.const 0)
 ---
 error: unknown identifier 'optimize.eq_def'
 -/
--- a/tests/lean/run/grind_cutsat_cooper.lean
+++ b/tests/lean/run/grind_cutsat_cooper.lean
@@ -7,3 +7,6 @@ example (x y : Int) :
    7*x - 9*y ≤ 4 → False := by
  -- `omega` fails in this example
  grind
+
+example (x : Int) : 100 ≤ x → x ≤ 10000 → 20000 ∣ 3*x → False := by
+  grind
--- a/tests/lean/run/grind_mark_nested_proofs_bug.lean
+++ b/tests/lean/run/grind_mark_nested_proofs_bug.lean
@@ -0,0 +1,28 @@
+set_option grind.warning false
+
+example (as bs cs : Array α) (v : α)
+        (i : Nat)
+        (h₁ : i < as.size)
+        (h₂ : bs = as.set i v)
+        (h₃ : cs = bs)
+        (h₄ : i ≠ j)
+        (h₅ : j < cs.size)
+        (h₆ : j < as.size)
+        : cs[j] = as[j] := by
+  skip
+  grind only [= Array.getElem_set_ne, = Array.size_set] -- works
+
+theorem Array.getElem_set_ne_abstracted (xs : Array α) (i : Nat) (h' : i < xs.size) (v : α) {j : Nat}
+    (pj : j < xs.size) (h : i ≠ j) :
+    (xs.set i v)[j]'(by as_aux_lemma => simp [*]) = xs[j] := Array.getElem_set_ne xs i h' v pj h
+
+example (as bs cs : Array α) (v : α)
+        (i : Nat)
+        (h₁ : i < as.size)
+        (h₂ : bs = as.set i v)
+        (h₃ : cs = bs)
+        (h₄ : i ≠ j)
+        (h₅ : j < cs.size)
+        (h₆ : j < as.size)
+        : cs[j] = as[j] := by
+  grind only [= Array.getElem_set_ne_abstracted, = Array.size_set] -- should work
--- a/tests/lean/run/issue6531.lean
+++ b/tests/lean/run/issue6531.lean
@@ -0,0 +1,9 @@
+-- This used to cause
+-- error: The termination argument's type must not depend on the function's varying parameters
+
+def foo (as : Array Nat) (i := 0) (j := as.size - 1) : Array Nat :=
+  if j ≤ i then as
+  else
+    let newas := as.set! 0 0
+    foo newas (i+1) (j-1)
+termination_by j - i
Author	SHA1	Message	Date
Leonardo de Moura	59d0515aa3	fix: `MarkNestedProofs`	2025-03-05 16:27:31 -08:00
Leonardo de Moura	9ae2ac39c9	feat: avoid cooper case analysis for univariate polynomials (#7351 ) This PR ensures cutsat does not have to perform case analysis in the univariate polynomial case. That it, it can close a goal whenever there is no solution for a divisibility constraint in an interval. Example of theorem that is now proved in a single step by cutsat: ```lean example (x : Int) : 100 ≤ x → x ≤ 10000 → 20000 ∣ 3*x → False := by grind ```	2025-03-05 20:37:29 +00:00
Wojciech Rozowski	2c8fb9d3fc	fix: strip optional parameters when elaborating the termination hints (#7335 ) This PR modifies `elabTerminationByHints` in a way that the type of the recursive function used for elaboration of the termination measure is striped of from optional parameters. It prevents introducing dependencies between the default values for arguments, that can cause the termination checker to fail. Closes https://github.com/leanprover/lean4/issues/6351.	2025-03-05 18:15:49 +00:00
Henrik Böving	dc7358b4df	feat: upgrade cadical to 2.1.2 (#7347 ) This PR upgrades the CaDiCal we ship and use for bv_decide to version 2.1.2. Additionally it enables binary LRAT proofs on windows by default as https://github.com/arminbiere/cadical/issues/112 has been fixed. Version 2.1.3 is already available but as the Bitwuzla authors [have pointed out](https://github.com/bitwuzla/bitwuzla/pull/129) one needs to be careful when upgrading CaDiCal so we just move to a version [they confirmed](`6e93389d86`) is fine for now.	2025-03-05 17:58:58 +00:00
Sebastian Ullrich	44a518b331	fix: never transfer constants from checked environment into elab branches (#7306 ) Otherwise we may lose the environment extension state of the constant	2025-03-05 17:12:27 +00:00
Markus Himmel	68f3fc6d5d	feat: finite type conversions (`Nat`/`Int`/`Fin`/`BitVec` -> `UIntX` -> *) (#7340 ) This PR adds lemmas for iterated conversions between finite types which start with `Nat`/`Int`/`Fin`/`BitVec` and then go through `UIntX`.	2025-03-05 15:35:36 +00:00
Sebastian Ullrich	72c4630aab	feat: use `realizeConst` for all equation and unfold theorems (#7348 ) This PR ensures all equation and unfold theorem generators in core are compatible with parallelism.	2025-03-05 14:56:50 +00:00
Lean stage0 autoupdater	db0abe89cf	chore: update stage0	2025-03-05 13:37:40 +00:00
Marc Huisinga	2b44a4f0d9	fix: inlay hint assertion violation when deleting open file (#7346 ) This PR fixes an issue where the language server would run into an inlay hint assertion violation when deleting a file that is still open in the language server.	2025-03-05 12:40:21 +00:00
Marc Huisinga	72f4098156	feat: combined auto-implicit inlay hint tooltip (#7344 ) This PR combines the auto-implicit inlay hint tooltips into a single tooltip. This works around an issue in VS Code where VS Code fails to update hovers for tooltips in adjacent inlay hint parts when moving the mouse.	2025-03-05 12:23:58 +00:00
Marc Huisinga	f0f7c3ff01	fix: inlay hints inserted at wrong position after edit (#7343 ) This PR mitigates an issue where inserting an inlay hint in VS Code by double-clicking would insert the inlay hint at the wrong position right after an edit. This bug was originally reported by @plp127 at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/v4.2E18.2E0.20-.20inlay.20hints/near/503362330. The cause of this bug is that when VS Code hasn't yet received a new set of inlay hints for a new document state, it will happily move around the displayed inlay hint, but it won't move around any of the other position-dependent properties of the inlay hint, like the property describing where to insert the inlay hint. Since we delay responses after an edit by an edit delay of 3000ms to prevent inlay hint flickering while typing, the window for this bug is relatively large. To work around this bug, we now always immediately respond to the first inlay hint request after an edit with the old state of the inlay hints, which we already update correctly on edits on the server-side so that we can serve old inlay hints for parts of the file that are still in-progress. Essentially, we are just telling VS Code how it should have moved all position-dependent properties of each inlay hint. Even with this mitigation, there is still a small window for this bug to occur, namely the window from an edit to when VS Code receives the old inlay hints from the server. In practice, this window should be a couple of milliseconds at most, so I'd hope it doesn't cause many problems. There's nothing we can do about this in either vscode-lean4 or the language server, unfortunately.	2025-03-05 12:23:53 +00:00