Merge remote-tracking branch 'origin/master' into copyright_headers

This is a quite substantial tactic.

It also includes the infamour `NatCast` typeclass (which I've equipped
with a module-doc). I wasn't at all sure where that should live, so it
is currently randomly in `Lean/Elan/Tactic/NatCast.lean`: presumably if
we're doing this it will go somewhere in `Init`.

---------

Co-authored-by: Leonardo de Moura <leomoura@amazon.com>

.github/workflows/copyright-header.yml

@@ -0,0 +1,20 @@
+name: Check for copyright header
+
+on: [pull_request]
+
+jobs:
+  check-lean-files:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v4
+
+    - name: Verify .lean files start with a copyright header.
+      run: |
+        FILES=$(find . -type d \( -path "./tests" -o -path "./doc" -o -path "./src/lake/examples" -o -path "./src/lake/tests" -o -path "./build" -o -path "./nix" \) -prune -o -type f -name "*.lean" -exec perl -ne 'BEGIN { $/ = undef; } print "$ARGV\n" if !m{\A/-\nCopyright}; exit;' {} \;)
+        if [ -n "$FILES" ]; then
+          echo "Found .lean files which do not have a copyright header:"
+          echo "$FILES"
+          exit 1
+        else
+          echo "All copyright headres present!"
+        fi

.github/workflows/nix-ci.yml

@@ -71,12 +71,6 @@ jobs:
         run: |
           sudo chown -R root:nixbld /nix/var/cache
           sudo chmod -R 770 /nix/var/cache
-      - name: Install Cachix
-        uses: cachix/cachix-action@v12
-        with:
-          name: lean4
-          authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
-          skipPush: true  # we push specific outputs only
       - name: Build
         run: |
           nix build $NIX_BUILD_ARGS .#cacheRoots -o push-build
@@ -98,9 +92,6 @@ jobs:
           # gmplib.org consistently times out from GH actions
           # the GitHub token is to avoid rate limiting
           args: --base './dist' --no-progress --github-token ${{ secrets.GITHUB_TOKEN }} --exclude 'gmplib.org' './dist/**/*.html'
-      - name: Push to Cachix
-        run: |
-          [ -z "${{ secrets.CACHIX_AUTH_TOKEN }}" ] || cachix push -j4 lean4 ./push-* || true
       - name: Rebuild Nix Store Cache
         run: |
           rm -rf nix-store-cache || true

.github/workflows/update-stage0.yml

@@ -40,18 +40,32 @@ jobs:
       run: |
           git config --global user.name "Lean stage0 autoupdater"
           git config --global user.email "<>"
-    - if: env.should_update_stage0 == 'yes'
-      uses: DeterminateSystems/nix-installer-action@main
     # Would be nice, but does not work yet:
     # https://github.com/DeterminateSystems/magic-nix-cache/issues/39
     # This action does not run that often and building runs in a few minutes, so ok for now
     #- if: env.should_update_stage0 == 'yes'
     #  uses: DeterminateSystems/magic-nix-cache-action@v2
     - if: env.should_update_stage0 == 'yes'
-      name: Install Cachix
-      uses: cachix/cachix-action@v12
+      name: Restore Build Cache
+      uses: actions/cache/restore@v3
       with:
-        name: lean4
+        path: nix-store-cache
+        key: Nix Linux-nix-store-cache-${{ github.sha }}
+        # fall back to (latest) previous cache
+        restore-keys: |
+          Nix Linux-nix-store-cache
+    - if: env.should_update_stage0 == 'yes'
+      name: Further Set Up Nix Cache
+      shell: bash -euxo pipefail {0}
+      run: |
+        # Nix seems to mutate the cache, so make a copy
+        cp -r nix-store-cache nix-store-cache-copy || true
+    - if: env.should_update_stage0 == 'yes'
+      name: Install Nix
+      uses: DeterminateSystems/nix-installer-action@main
+      with:
+        extra-conf: |
+          substituters = file://${{ github.workspace }}/nix-store-cache-copy?priority=10&trusted=true https://cache.nixos.org  
     - if: env.should_update_stage0 == 'yes'
       run: nix run .#update-stage0-commit
     - if: env.should_update_stage0 == 'yes'

RELEASES.md

@@ -66,6 +66,21 @@ v4.7.0 (development in progress)
     rw [h]
   ```
 
+* When adding new local theorems to `simp`, the system assumes that the function application arguments
+  have been annotated with `no_index`. This modification, which addresses issue [#2670](https://github.com/leanprover/lean4/issues/2670),
+  restores the Lean 3 behavior that users expect. With this modification, the following examples are now operational:
+  ```
+  example {α β : Type} {f : α × β → β → β} (h : ∀ p : α × β, f p p.2 = p.2)
+    (a : α) (b : β) : f (a, b) b = b := by
+    simp [h]
+
+  example {α β : Type} {f : α × β → β → β}
+    (a : α) (b : β) (h : f (a,b) (a,b).2 = (a,b).2) : f (a, b) b = b := by
+    simp [h]
+  ```
+  In both cases, `h` is applicable because `simp` does not index f-arguments anymore when adding `h` to the `simp`-set.
+  It's important to note, however, that global theorems continue to be indexed in the usual manner.
+
 Breaking changes:
 * `Lean.withTraceNode` and variants got a stronger `MonadAlwaysExcept` assumption to
   fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration

script/apply.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
 import Lean.Runtime
 
 abbrev M := ReaderT IO.FS.Stream IO
@@ -16,7 +21,7 @@ def mkTypedefFn (i : Nat) : M Unit := do
   emit s!"typedef obj* (*fn{i})({args}); // NOLINT\n"
   emit s!"#define FN{i}(f) reinterpret_cast<fn{i}>(lean_closure_fun(f))\n"
 
-def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String := 
+def genSeq (n : Nat) (f : Nat → String) (sep := ", ") : String :=
   List.range n |>.map f |>.intersperse sep |> .join
 
 -- make string: "obj* a1, obj* a2, ..., obj* an"

src/Init/Conv.lean

@@ -308,4 +308,7 @@ Basic forms:
 -- refer to the syntax category instead of this syntax
 syntax (name := conv) "conv" (" at " ident)? (" in " (occs)? term)? " => " convSeq : tactic
 
+/-- `norm_cast` tactic in `conv` mode. -/
+syntax (name := normCast) "norm_cast" : conv
+
 end Lean.Parser.Tactic.Conv

src/Init/Data.lean

@@ -7,6 +7,7 @@ prelude
 import Init.Data.Basic
 import Init.Data.Nat
 import Init.Data.Bool
+import Init.Data.BitVec
 import Init.Data.Cast
 import Init.Data.Char
 import Init.Data.String
@@ -31,3 +32,4 @@ import Init.Data.Prod
 import Init.Data.AC
 import Init.Data.Queue
 import Init.Data.Channel
+import Init.Data.Cast

src/Init/Data/Array/Lemmas.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 prelude
-import Init.Data.Nat
+import Init.Data.Nat.MinMax
 import Init.Data.List.Lemmas
 import Init.Data.Fin.Basic
 import Init.Data.Array.Mem

src/Init/Data/Array/Subarray.lean

@@ -143,6 +143,7 @@ def toSubarray (as : Array α) (start : Nat := 0) (stop : Nat := as.size) : Suba
      else
        { as := as, start := as.size, stop := as.size, h₁ := Nat.le_refl _, h₂ := Nat.le_refl _ }
 
+@[coe]
 def ofSubarray (s : Subarray α) : Array α := Id.run do
   let mut as := mkEmpty (s.stop - s.start)
   for a in s do

src/Init/Data/BitVec.lean

@@ -0,0 +1,10 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Init.Data.BitVec.Basic
+import Init.Data.BitVec.Bitblast
+import Init.Data.BitVec.Folds
+import Init.Data.BitVec.Lemmas

src/Init/Data/BitVec/Basic.lean

@@ -0,0 +1,535 @@
+/-
+Copyright (c) 2022 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix, Wojciech Nawrocki, Leonardo de Moura, Mario Carneiro, Alex Keizer
+-/
+prelude
+import Init.Data.Fin.Basic
+import Init.Data.Nat.Bitwise.Lemmas
+import Init.Data.Nat.Power2
+
+namespace Std
+
+/-!
+We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
+(Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
+with `Fin`, and the fact that bitwise operations on `Fin` are already defined. Some other possible
+representations are `List Bool`, `{ l : List Bool // l.length = w }`, `Fin w → Bool`.
+
+We define many of the bitvector operations from the
+[`QF_BV` logic](https://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV).
+of SMT-LIBv2.
+-/
+
+/--
+A bitvector of the specified width. This is represented as the underlying `Nat` number
+in both the runtime and the kernel, inheriting all the special support for `Nat`.
+-/
+structure BitVec (w : Nat) where
+  /-- Construct a `BitVec w` from a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  ofFin ::
+  /-- Interpret a bitvector as a number less than `2^w`.
+  O(1), because we use `Fin` as the internal representation of a bitvector. -/
+  toFin : Fin (2^w)
+  deriving DecidableEq
+
+namespace BitVec
+
+/-- `cast eq i` embeds `i` into an equal `BitVec` type. -/
+@[inline] def cast (eq : n = m) (i : BitVec n) : BitVec m :=
+  .ofFin (Fin.cast (congrArg _ eq) i.toFin)
+
+/-- The `BitVec` with value `i mod 2^n`. Treated as an operation on bitvectors,
+this is truncation of the high bits when downcasting and zero-extension when upcasting. -/
+protected def ofNat (n : Nat) (i : Nat) : BitVec n where
+  toFin := Fin.ofNat' i (Nat.two_pow_pos n)
+
+instance : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
+
+/-- Given a bitvector `a`, return the underlying `Nat`. This is O(1) because `BitVec` is a
+(zero-cost) wrapper around a `Nat`. -/
+protected def toNat (a : BitVec n) : Nat := a.toFin.val
+
+/-- Return the bound in terms of toNat. -/
+theorem isLt (x : BitVec w) : x.toNat < 2^w := x.toFin.isLt
+
+/-- Return the `i`-th least significant bit or `false` if `i ≥ w`. -/
+@[inline] def getLsb (x : BitVec w) (i : Nat) : Bool := x.toNat.testBit i
+
+/-- Return the `i`-th most significant bit or `false` if `i ≥ w`. -/
+@[inline] def getMsb (x : BitVec w) (i : Nat) : Bool := i < w && getLsb x (w-1-i)
+
+/-- Return most-significant bit in bitvector. -/
+@[inline] protected def msb (a : BitVec n) : Bool := getMsb a 0
+
+/-- Interpret the bitvector as an integer stored in two's complement form. -/
+protected def toInt (a : BitVec n) : Int :=
+  if a.msb then Int.ofNat a.toNat - Int.ofNat (2^n) else a.toNat
+
+/-- Return a bitvector `0` of size `n`. This is the bitvector with all zero bits. -/
+protected def zero (n : Nat) : BitVec n := ⟨0, Nat.two_pow_pos n⟩
+
+instance : Inhabited (BitVec n) where default := .zero n
+
+instance instOfNat : OfNat (BitVec n) i where ofNat := .ofNat n i
+
+/-- Notation for bit vector literals. `i#n` is a shorthand for `BitVec.ofNat n i`. -/
+scoped syntax:max term:max noWs "#" noWs term:max : term
+macro_rules | `($i#$n) => `(BitVec.ofNat $n $i)
+
+/- Support for `i#n` notation in patterns.  -/
+attribute [match_pattern] BitVec.ofNat
+
+/-- Unexpander for bit vector literals. -/
+@[app_unexpander BitVec.ofNat] def unexpandBitVecOfNat : Lean.PrettyPrinter.Unexpander
+  | `($(_) $n $i) => `($i#$n)
+  | _ => throw ()
+
+/-- Convert bitvector into a fixed-width hex number. -/
+protected def toHex {n : Nat} (x : BitVec n) : String :=
+  let s := (Nat.toDigits 16 x.toNat).asString
+  let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
+  t ++ s
+
+instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Format) ++ "#" ++ repr n
+
+instance : ToString (BitVec n) where toString a := toString (repr a)
+
+/-- Theorem for normalizing the bit vector literal representation. -/
+-- TODO: This needs more usage data to assess which direction the simp should go.
+@[simp] theorem ofNat_eq_ofNat : @OfNat.ofNat (BitVec n) i _ = BitVec.ofNat n i := rfl
+@[simp] theorem natCast_eq_ofNat : Nat.cast x = x#w := rfl
+
+/--
+Addition for bit vectors. This can be interpreted as either signed or unsigned addition
+modulo `2^n`.
+
+SMT-Lib name: `bvadd`.
+-/
+protected def add (x y : BitVec n) : BitVec n where toFin := x.toFin + y.toFin
+instance : Add (BitVec n) := ⟨BitVec.add⟩
+
+/--
+Subtraction for bit vectors. This can be interpreted as either signed or unsigned subtraction
+modulo `2^n`.
+-/
+protected def sub (x y : BitVec n) : BitVec n where toFin := x.toFin - y.toFin
+instance : Sub (BitVec n) := ⟨BitVec.sub⟩
+
+/--
+Negation for bit vectors. This can be interpreted as either signed or unsigned negation
+modulo `2^n`.
+
+SMT-Lib name: `bvneg`.
+-/
+protected def neg (x : BitVec n) : BitVec n := .sub 0 x
+instance : Neg (BitVec n) := ⟨.neg⟩
+
+/-- Bit vector of size `n` where all bits are `1`s -/
+def allOnes (n : Nat) : BitVec n := -1
+
+/--
+Return the absolute value of a signed bitvector.
+-/
+protected def abs (s : BitVec n) : BitVec n := if s.msb then .neg s else s
+
+/--
+Multiplication for bit vectors. This can be interpreted as either signed or unsigned negation
+modulo `2^n`.
+
+SMT-Lib name: `bvmul`.
+-/
+protected def mul (x y : BitVec n) : BitVec n := ofFin <| x.toFin * y.toFin
+instance : Mul (BitVec n) := ⟨.mul⟩
+
+/--
+Unsigned division for bit vectors using the Lean convention where division by zero returns zero.
+-/
+def udiv (x y : BitVec n) : BitVec n := ofFin <| x.toFin / y.toFin
+instance : Div (BitVec n) := ⟨.udiv⟩
+
+/--
+Unsigned modulo for bit vectors.
+
+SMT-Lib name: `bvurem`.
+-/
+def umod (x y : BitVec n) : BitVec n := ofFin <| x.toFin % y.toFin
+instance : Mod (BitVec n) := ⟨.umod⟩
+
+/--
+Unsigned division for bit vectors using the
+[SMT-Lib convention](http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml)
+where division by zero returns the `allOnes` bitvector.
+
+SMT-Lib name: `bvudiv`.
+-/
+def smtUDiv (x y : BitVec n) : BitVec n := if y = 0 then -1 else .udiv x y
+
+/--
+Signed t-division for bit vectors using the Lean convention where division
+by zero returns zero.
+
+```lean
+sdiv 7#4 2 = 3#4
+sdiv (-9#4) 2 = -4#4
+sdiv 5#4 -2 = -2#4
+sdiv (-7#4) (-2) = 3#4
+```
+-/
+def sdiv (s t : BitVec n) : BitVec n :=
+  match s.msb, t.msb with
+  | false, false => udiv s t
+  | false, true  => .neg (udiv s (.neg t))
+  | true,  false => .neg (udiv (.neg s) t)
+  | true,  true  => udiv (.neg s) (.neg t)
+
+/--
+Signed division for bit vectors using SMTLIB rules for division by zero.
+
+Specifically, `smtSDiv x 0 = if x >= 0 then -1 else 1`
+
+SMT-Lib name: `bvsdiv`.
+-/
+def smtSDiv (s t : BitVec n) : BitVec n :=
+  match s.msb, t.msb with
+  | false, false => smtUDiv s t
+  | false, true  => .neg (smtUDiv s (.neg t))
+  | true,  false => .neg (smtUDiv (.neg s) t)
+  | true,  true  => smtUDiv (.neg s) (.neg t)
+
+/--
+Remainder for signed division rounding to zero.
+
+SMT_Lib name: `bvsrem`.
+-/
+def srem (s t : BitVec n) : BitVec n :=
+  match s.msb, t.msb with
+  | false, false => umod s t
+  | false, true  => umod s (.neg t)
+  | true,  false => .neg (umod (.neg s) t)
+  | true,  true  => .neg (umod (.neg s) (.neg t))
+
+/--
+Remainder for signed division rounded to negative infinity.
+
+SMT_Lib name: `bvsmod`.
+-/
+def smod (s t : BitVec m) : BitVec m :=
+  match s.msb, t.msb with
+  | false, false => .umod s t
+  | false, true =>
+    let u := .umod s (.neg t)
+    (if u = BitVec.ofNat m 0 then u else .add u t)
+  | true, false =>
+    let u := .umod (.neg s) t
+    (if u = BitVec.ofNat m 0 then u else .sub t u)
+  | true, true => .neg (.umod (.neg s) (.neg t))
+
+/--
+Unsigned less-than for bit vectors.
+
+SMT-Lib name: `bvult`.
+-/
+protected def ult (x y : BitVec n) : Bool := x.toFin < y.toFin
+instance : LT (BitVec n) where lt x y := x.toFin < y.toFin
+instance (x y : BitVec n) : Decidable (x < y) :=
+  inferInstanceAs (Decidable (x.toFin < y.toFin))
+
+/--
+Unsigned less-than-or-equal-to for bit vectors.
+
+SMT-Lib name: `bvule`.
+-/
+protected def ule (x y : BitVec n) : Bool := x.toFin ≤ y.toFin
+
+instance : LE (BitVec n) where le x y := x.toFin ≤ y.toFin
+instance (x y : BitVec n) : Decidable (x ≤ y) :=
+  inferInstanceAs (Decidable (x.toFin ≤ y.toFin))
+
+/--
+Signed less-than for bit vectors.
+
+```lean
+BitVec.slt 6#4 7 = true
+BitVec.slt 7#4 8 = false
+```
+SMT-Lib name: `bvslt`.
+-/
+protected def slt (x y : BitVec n) : Bool := x.toInt < y.toInt
+
+/--
+Signed less-than-or-equal-to for bit vectors.
+
+SMT-Lib name: `bvsle`.
+-/
+protected def sle (x y : BitVec n) : Bool := x.toInt ≤ y.toInt
+
+/--
+Bitwise AND for bit vectors.
+
+```lean
+0b1010#4 &&& 0b0110#4 = 0b0010#4
+```
+
+SMT-Lib name: `bvand`.
+-/
+protected def and (x y : BitVec n) : BitVec n where toFin :=
+   ⟨x.toNat &&& y.toNat, Nat.and_lt_two_pow x.toNat y.isLt⟩
+instance : AndOp (BitVec w) := ⟨.and⟩
+
+/--
+Bitwise OR for bit vectors.
+
+```lean
+0b1010#4 ||| 0b0110#4 = 0b1110#4
+```
+
+SMT-Lib name: `bvor`.
+-/
+protected def or (x y : BitVec n) : BitVec n where toFin :=
+   ⟨x.toNat ||| y.toNat, Nat.or_lt_two_pow x.isLt y.isLt⟩
+instance : OrOp (BitVec w) := ⟨.or⟩
+
+/--
+ Bitwise XOR for bit vectors.
+
+```lean
+0b1010#4 ^^^ 0b0110#4 = 0b1100#4
+```
+
+SMT-Lib name: `bvxor`.
+-/
+protected def xor (x y : BitVec n) : BitVec n where toFin :=
+   ⟨x.toNat ^^^ y.toNat, Nat.xor_lt_two_pow x.isLt y.isLt⟩
+instance : Xor (BitVec w) := ⟨.xor⟩
+
+/--
+Bitwise NOT for bit vectors.
+
+```lean
+~~~(0b0101#4) == 0b1010
+```
+SMT-Lib name: `bvnot`.
+-/
+protected def not (x : BitVec n) : BitVec n :=
+  allOnes n ^^^ x
+instance : Complement (BitVec w) := ⟨.not⟩
+
+/-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`.  -/
+protected def ofInt (n : Nat) (i : Int) : BitVec n :=
+  match i with
+  | Int.ofNat a => .ofNat n a
+  | Int.negSucc a => ~~~.ofNat n a
+
+instance : IntCast (BitVec w) := ⟨BitVec.ofInt w⟩
+
+/--
+Left shift for bit vectors. The low bits are filled with zeros. As a numeric operation, this is
+equivalent to `a * 2^s`, modulo `2^n`.
+
+SMT-Lib name: `bvshl` except this operator uses a `Nat` shift value.
+-/
+protected def shiftLeft (a : BitVec n) (s : Nat) : BitVec n := .ofNat n (a.toNat <<< s)
+instance : HShiftLeft (BitVec w) Nat (BitVec w) := ⟨.shiftLeft⟩
+
+/--
+(Logical) right shift for bit vectors. The high bits are filled with zeros.
+As a numeric operation, this is equivalent to `a / 2^s`, rounding down.
+
+SMT-Lib name: `bvlshr` except this operator uses a `Nat` shift value.
+-/
+def ushiftRight (a : BitVec n) (s : Nat) : BitVec n :=
+  ⟨a.toNat >>> s, by
+  let ⟨a, lt⟩ := a
+  simp only [BitVec.toNat, Nat.shiftRight_eq_div_pow, Nat.div_lt_iff_lt_mul (Nat.two_pow_pos s)]
+  rw [←Nat.mul_one a]
+  exact Nat.mul_lt_mul_of_lt_of_le' lt (Nat.two_pow_pos s) (Nat.le_refl 1)⟩
+
+instance : HShiftRight (BitVec w) Nat (BitVec w) := ⟨.ushiftRight⟩
+
+/--
+Arithmetic right shift for bit vectors. The high bits are filled with the
+most-significant bit.
+As a numeric operation, this is equivalent to `a.toInt >>> s`.
+
+SMT-Lib name: `bvashr` except this operator uses a `Nat` shift value.
+-/
+def sshiftRight (a : BitVec n) (s : Nat) : BitVec n := .ofInt n (a.toInt >>> s)
+
+instance {n} : HShiftLeft  (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x <<< y.toNat⟩
+instance {n} : HShiftRight (BitVec m) (BitVec n) (BitVec m) := ⟨fun x y => x >>> y.toNat⟩
+
+/--
+Rotate left for bit vectors. All the bits of `x` are shifted to higher positions, with the top `n`
+bits wrapping around to fill the low bits.
+
+```lean
+rotateLeft  0b0011#4 3 = 0b1001
+```
+SMT-Lib name: `rotate_left` except this operator uses a `Nat` shift amount.
+-/
+def rotateLeft (x : BitVec w) (n : Nat) : BitVec w := x <<< n ||| x >>> (w - n)
+
+/--
+Rotate right for bit vectors. All the bits of `x` are shifted to lower positions, with the
+bottom `n` bits wrapping around to fill the high bits.
+
+```lean
+rotateRight 0b01001#5 1 = 0b10100
+```
+SMT-Lib name: `rotate_right` except this operator uses a `Nat` shift amount.
+-/
+def rotateRight (x : BitVec w) (n : Nat) : BitVec w := x >>> n ||| x <<< (w - n)
+
+/--
+A version of `zeroExtend` that requires a proof, but is a noop.
+-/
+def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n)  : BitVec w :=
+  ⟨x.toNat, by
+    apply Nat.lt_of_lt_of_le x.isLt
+    exact Nat.pow_le_pow_of_le_right (by trivial) le⟩
+
+/--
+`shiftLeftZeroExtend x n` returns `zeroExtend (w+n) x <<< n` without
+needing to compute `x % 2^(2+n)`.
+-/
+def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w+m) :=
+  let shiftLeftLt {x : Nat} (p : x < 2^w) (m : Nat) : x <<< m < 2^(w+m) := by
+        simp [Nat.shiftLeft_eq, Nat.pow_add]
+        apply Nat.mul_lt_mul_of_pos_right p
+        exact (Nat.two_pow_pos m)
+  ⟨msbs.toNat <<< m, shiftLeftLt msbs.isLt m⟩
+
+/--
+Concatenation of bitvectors. This uses the "big endian" convention that the more significant
+input is on the left, so `0xAB#8 ++ 0xCD#8 = 0xABCD#16`.
+
+SMT-Lib name: `concat`.
+-/
+def append (msbs : BitVec n) (lsbs : BitVec m) : BitVec (n+m) :=
+  shiftLeftZeroExtend msbs m ||| zeroExtend' (Nat.le_add_left m n) lsbs
+
+instance : HAppend (BitVec w) (BitVec v) (BitVec (w + v)) := ⟨.append⟩
+
+/--
+Extraction of bits `start` to `start + len - 1` from a bit vector of size `n` to yield a
+new bitvector of size `len`. If `start + len > n`, then the vector will be zero-padded in the
+high bits.
+-/
+def extractLsb' (start len : Nat) (a : BitVec n) : BitVec len := .ofNat _ (a.toNat >>> start)
+
+/--
+Extraction of bits `hi` (inclusive) down to `lo` (inclusive) from a bit vector of size `n` to
+yield a new bitvector of size `hi - lo + 1`.
+
+SMT-Lib name: `extract`.
+-/
+def extractLsb (hi lo : Nat) (a : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ a
+
+-- TODO: write this using multiplication
+/-- `replicate i x` concatenates `i` copies of `x` into a new vector of length `w*i`. -/
+def replicate : (i : Nat) → BitVec w → BitVec (w*i)
+  | 0,   _ => 0
+  | n+1, x =>
+    have hEq : w + w*n = w*(n + 1) := by
+      rw [Nat.mul_add, Nat.add_comm, Nat.mul_one]
+    hEq ▸ (x ++ replicate n x)
+
+/-- Fills a bitvector with `w` copies of the bit `b`. -/
+def fill (w : Nat) (b : Bool) : BitVec w := bif b then -1 else 0
+
+/--
+Zero extend vector `x` of length `w` by adding zeros in the high bits until it has length `v`.
+If `v < w` then it truncates the high bits instead.
+
+SMT-Lib name: `zero_extend`.
+-/
+def zeroExtend (v : Nat) (x : BitVec w) : BitVec v :=
+  if h : w ≤ v then
+    zeroExtend' h x
+  else
+    .ofNat v x.toNat
+
+/--
+Truncate the high bits of bitvector `x` of length `w`, resulting in a vector of length `v`.
+If `v > w` then it zero-extends the vector instead.
+-/
+abbrev truncate := @zeroExtend
+
+/--
+Sign extend a vector of length `w`, extending with `i` additional copies of the most significant
+bit in `x`. If `x` is an empty vector, then the sign is treated as zero.
+
+SMT-Lib name: `sign_extend`.
+-/
+def signExtend (v : Nat) (x : BitVec w) : BitVec v := .ofInt v x.toInt
+
+/-! We add simp-lemmas that rewrite bitvector operations into the equivalent notation -/
+@[simp] theorem append_eq (x : BitVec w) (y : BitVec v)   : BitVec.append x y = x ++ y        := rfl
+@[simp] theorem shiftLeft_eq (x : BitVec w) (n : Nat)     : BitVec.shiftLeft x n = x <<< n    := rfl
+@[simp] theorem ushiftRight_eq (x : BitVec w) (n : Nat)   : BitVec.ushiftRight x n = x >>> n  := rfl
+@[simp] theorem not_eq (x : BitVec w)                     : BitVec.not x = ~~~x               := rfl
+@[simp] theorem and_eq (x y : BitVec w)                   : BitVec.and x y = x &&& y          := rfl
+@[simp] theorem or_eq (x y : BitVec w)                    : BitVec.or x y = x ||| y           := rfl
+@[simp] theorem xor_eq (x y : BitVec w)                   : BitVec.xor x y = x ^^^ y          := rfl
+@[simp] theorem neg_eq (x : BitVec w)                     : BitVec.neg x = -x                 := rfl
+@[simp] theorem add_eq (x y : BitVec w)                   : BitVec.add x y = x + y            := rfl
+@[simp] theorem sub_eq (x y : BitVec w)                   : BitVec.sub x y = x - y            := rfl
+@[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
+@[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
+
+@[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
+    cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by
+  subst h; rfl
+
+@[simp] theorem cast_cast {n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) :
+    cast h₂ (cast h₁ x) = cast (h₁ ▸ h₂) x :=
+  rfl
+
+@[simp] theorem cast_eq {n : Nat} (h : n = n) (x : BitVec n) :
+    cast h x = x :=
+  rfl
+
+/-- Turn a `Bool` into a bitvector of length `1` -/
+def ofBool (b : Bool) : BitVec 1 := cond b 1 0
+
+@[simp] theorem ofBool_false : ofBool false = 0 := by trivial
+@[simp] theorem ofBool_true  : ofBool true  = 1 := by trivial
+
+/-- The empty bitvector -/
+abbrev nil : BitVec 0 := 0
+
+/-!
+### Cons and Concat
+We give special names to the operations of adding a single bit to either end of a bitvector.
+We follow the precedent of `Vector.cons`/`Vector.concat` both for the name, and for the decision
+to have the resulting size be `n + 1` for both operations (rather than `1 + n`, which would be the
+result of appending a single bit to the front in the naive implementation).
+-/
+
+/-- Append a single bit to the end of a bitvector, using big endian order (see `append`).
+    That is, the new bit is the least significant bit. -/
+def concat {n} (msbs : BitVec n) (lsb : Bool) : BitVec (n+1) := msbs ++ (ofBool lsb)
+
+/-- Prepend a single bit to the front of a bitvector, using big endian order (see `append`).
+    That is, the new bit is the most significant bit. -/
+def cons {n} (msb : Bool) (lsbs : BitVec n) : BitVec (n+1) :=
+  ((ofBool msb) ++ lsbs).cast (Nat.add_comm ..)
+
+/-- All empty bitvectors are equal -/
+instance : Subsingleton (BitVec 0) where
+  allEq := by intro ⟨0, _⟩ ⟨0, _⟩; rfl
+
+/-- Every bitvector of length 0 is equal to `nil`, i.e., there is only one empty bitvector -/
+theorem eq_nil : ∀ (x : BitVec 0), x = nil
+  | ofFin ⟨0, _⟩ => rfl
+
+theorem append_ofBool (msbs : BitVec w) (lsb : Bool) :
+    msbs ++ ofBool lsb = concat msbs lsb :=
+  rfl
+
+theorem ofBool_append (msb : Bool) (lsbs : BitVec w) :
+    ofBool msb ++ lsbs = (cons msb lsbs).cast (Nat.add_comm ..) :=
+  rfl

src/Init/Data/BitVec/Bitblast.lean

@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Harun Khan, Abdalrhman M Mohamed, Joe Hendrix
+-/
+prelude
+import Init.Data.BitVec.Folds
+
+/-!
+# Bitblasting of bitvectors
+
+This module provides theorems for showing the equivalence between BitVec operations using
+the `Fin 2^n` representation and Boolean vectors.  It is still under development, but
+intended to provide a path for converting SAT and SMT solver proofs about BitVectors
+as vectors of bits into proofs about Lean `BitVec` values.
+
+The module is named for the bit-blasting operation in an SMT solver that converts bitvector
+expressions into expressions about individual bits in each vector.
+
+## Main results
+* `x + y : BitVec w` is `(adc x y false).2`.
+
+
+## Future work
+All other operations are to be PR'ed later and are already proved in
+https://github.com/mhk119/lean-smt/blob/bitvec/Smt/Data/Bitwise.lean.
+
+-/
+
+open Nat Bool
+
+/-! ### Preliminaries -/
+
+namespace Std.BitVec
+
+private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
+    testBit x i = decide (x ≥ 2^i) := by
+  cases xi : testBit x i with
+  | true =>
+    simp [testBit_implies_ge xi]
+  | false =>
+    simp
+    cases Nat.lt_or_ge x (2^i) with
+    | inl x_lt =>
+      exact x_lt
+    | inr x_ge =>
+      have ⟨j, ⟨j_ge, jp⟩⟩  := ge_two_pow_implies_high_bit_true x_ge
+      cases Nat.lt_or_eq_of_le j_ge with
+      | inr x_eq =>
+        simp [x_eq, jp] at xi
+      | inl x_lt =>
+        exfalso
+        apply Nat.lt_irrefl
+        calc x < 2^(i+1) := x_lt_succ
+             _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two x_lt
+             _ ≤ x := testBit_implies_ge jp
+
+private theorem mod_two_pow_succ (x i : Nat) :
+  x % 2^(i+1) = 2^i*(x.testBit i).toNat + x % (2 ^ i):= by
+  apply Nat.eq_of_testBit_eq
+  intro j
+  simp only [Nat.mul_add_lt_is_or, testBit_or, testBit_mod_two_pow, testBit_shiftLeft,
+    Nat.testBit_bool_to_nat, Nat.sub_eq_zero_iff_le, Nat.mod_lt, Nat.two_pow_pos,
+    testBit_mul_pow_two]
+  rcases Nat.lt_trichotomy i j with i_lt_j | i_eq_j | j_lt_i
+  · have i_le_j : i ≤ j := Nat.le_of_lt i_lt_j
+    have not_j_le_i : ¬(j ≤ i) := Nat.not_le_of_lt i_lt_j
+    have not_j_lt_i : ¬(j < i) := Nat.not_lt_of_le i_le_j
+    have not_j_lt_i_succ : ¬(j < i + 1) :=
+          Nat.not_le_of_lt (Nat.succ_lt_succ i_lt_j)
+    simp [i_le_j, not_j_le_i, not_j_lt_i, not_j_lt_i_succ]
+  · simp [i_eq_j]
+  · have j_le_i : j ≤ i := Nat.le_of_lt j_lt_i
+    have j_le_i_succ : j < i + 1 := Nat.succ_le_succ j_le_i
+    have not_j_ge_i : ¬(j ≥ i) := Nat.not_le_of_lt j_lt_i
+    simp [j_lt_i, j_le_i, not_j_ge_i, j_le_i_succ]
+
+private theorem mod_two_pow_lt (x i : Nat) : x % 2 ^ i < 2^i := Nat.mod_lt _ (Nat.two_pow_pos _)
+
+/-! ### Addition -/
+
+/-- carry w x y c returns true if the `w` carry bit is true when computing `x + y + c`. -/
+def carry (w x y : Nat) (c : Bool) : Bool := decide (x % 2^w + y % 2^w + c.toNat ≥ 2^w)
+
+@[simp] theorem carry_zero : carry 0 x y c = c := by
+  cases c <;> simp [carry, mod_one]
+
+/-- At least two out of three booleans are true. -/
+abbrev atLeastTwo (a b c : Bool) : Bool := a && b || a && c || b && c
+
+/-- Carry function for bitwise addition. -/
+def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xor y c))
+
+/-- Bitwise addition implemented via a ripple carry adder. -/
+def adc (x y : BitVec w) : Bool → Bool × BitVec w :=
+  iunfoldr fun (i : Fin w) c => adcb (x.getLsb i) (y.getLsb i) c
+
+theorem adc_overflow_limit (x y i : Nat) (c : Bool) : x % 2^i + (y % 2^i + c.toNat) < 2^(i+1) := by
+  have : c.toNat ≤ 1 := Bool.toNat_le_one c
+  rw [Nat.pow_succ]
+  omega
+
+theorem carry_succ (w x y : Nat) (c : Bool) :
+    carry (succ w) x y c = atLeastTwo (x.testBit w) (y.testBit w) (carry w x y c) := by
+  simp only [carry, mod_two_pow_succ, atLeastTwo]
+  simp only [Nat.pow_succ']
+  generalize testBit x w = xh
+  generalize testBit y w = yh
+  have sum_bnd : x%2^w + (y%2^w + c.toNat) < 2*2^w := by
+          simp only [← Nat.pow_succ']
+          exact adc_overflow_limit x y w c
+  cases xh <;> cases yh <;> (simp; omega)
+
+theorem getLsb_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
+    getLsb (x + y + zeroExtend w (ofBool c)) i =
+      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x.toNat y.toNat c)) := by
+  let ⟨x, x_lt⟩ := x
+  let ⟨y, y_lt⟩ := y
+  simp only [getLsb, toNat_add, toNat_zeroExtend, i_lt, toNat_ofFin, toNat_ofBool,
+    Nat.mod_add_mod, Nat.add_mod_mod]
+  apply Eq.trans
+  rw [← Nat.div_add_mod x (2^i), ← Nat.div_add_mod y (2^i)]
+  simp only
+    [ Nat.testBit_mod_two_pow,
+      Nat.testBit_mul_two_pow_add_eq,
+      i_lt,
+      decide_True,
+      Bool.true_and,
+      Nat.add_assoc,
+      Nat.add_left_comm (_%_) (_ * _) _,
+      testBit_limit (adc_overflow_limit x y i c)
+    ]
+  simp [testBit_to_div_mod, carry, Nat.add_assoc]
+
+theorem getLsb_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
+    getLsb (x + y) i =
+      Bool.xor (getLsb x i) (Bool.xor (getLsb y i) (carry i x.toNat y.toNat false)) := by
+  simpa using getLsb_add_add_bool i_lt x y false
+
+theorem adc_spec (x y : BitVec w) (c : Bool) :
+    adc x y c = (carry w x.toNat y.toNat c, x + y + zeroExtend w (ofBool c)) := by
+  simp only [adc]
+  apply iunfoldr_replace
+          (fun i => carry i x.toNat y.toNat c)
+          (x + y + zeroExtend w (ofBool c))
+          c
+  case init =>
+    simp [carry, Nat.mod_one]
+    cases c <;> rfl
+  case step =>
+    intro ⟨i, lt⟩
+    simp only [adcb, Prod.mk.injEq, carry_succ]
+    apply And.intro
+    case left =>
+      rw [testBit_toNat, testBit_toNat]
+    case right =>
+      simp [getLsb_add_add_bool lt]
+
+theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := by
+  simp [adc_spec]
+
+/-! ### add -/
+
+/-- Adding a bitvector to its own complement yields the all ones bitpattern -/
+@[simp] theorem add_not_self (x : BitVec w) : x + ~~~x = allOnes w := by
+  rw [add_eq_adc, adc, iunfoldr_replace (fun _ => false) (allOnes w)]
+  · rfl
+  · simp [adcb, atLeastTwo]
+
+/-- Subtracting `x` from the all ones bitvector is equivalent to taking its complement -/
+theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
+  rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]

src/Init/Data/BitVec/Folds.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Init.Data.BitVec.Lemmas
+import Init.Data.Nat.Lemmas
+import Init.Data.Fin.Iterate
+
+namespace Std.BitVec
+
+/--
+iunfoldr is an iterative operation that applies a function `f` repeatedly.
+
+It produces a sequence of state values `[s_0, s_1 .. s_w]` and a bitvector
+`v` where `f i s_i = (s_{i+1}, b_i)` and `b_i` is bit `i`th least-significant bit
+in `v` (e.g., `getLsb v i = b_i`).
+
+Theorems involving `iunfoldr` can be eliminated using `iunfoldr_replace` below.
+-/
+def iunfoldr (f : Fin w -> α → α × Bool) (s : α) : α × BitVec w :=
+  Fin.hIterate (fun i => α × BitVec i) (s, nil) fun i q =>
+    (fun p => ⟨p.fst, cons p.snd q.snd⟩) (f i q.fst)
+
+theorem iunfoldr.fst_eq
+    {f : Fin w → α → α × Bool} (state : Nat → α) (s : α)
+    (init : s = state 0)
+    (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :
+    (iunfoldr f s).fst = state w := by
+  unfold iunfoldr
+  apply Fin.hIterate_elim (fun i (p : α × BitVec i) => p.fst = state i)
+  case init =>
+    exact init
+  case step =>
+    intro i ⟨s, v⟩ p
+    simp_all [ind i]
+
+private theorem iunfoldr.eq_test
+    {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
+    (init : state 0 = a)
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    iunfoldr f a = (state w, BitVec.truncate w value) := by
+  apply Fin.hIterate_eq (fun i => ((state i, BitVec.truncate i value) : α × BitVec i))
+  case init =>
+    simp only [init, eq_nil]
+  case step =>
+    intro i
+    simp_all [truncate_succ]
+
+/--
+Correctness theorem for `iunfoldr`.
+-/
+theorem iunfoldr_replace
+    {f : Fin w → α → α × Bool} (state : Nat → α) (value : BitVec w) (a : α)
+    (init : state 0 = a)
+    (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
+    iunfoldr f a = (state w, value) := by
+  simp [iunfoldr.eq_test state value a init step]

src/Init/Data/BitVec/Lemmas.lean

@@ -0,0 +1,534 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+prelude
+import Init.Data.Bool
+import Init.Data.BitVec.Basic
+import Init.Data.Fin.Lemmas
+import Init.Data.Nat.Lemmas
+
+namespace Std.BitVec
+
+/--
+This normalized a bitvec using `ofFin` to `ofNat`.
+-/
+theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by
+  simp only [BitVec.ofNat, Fin.ofNat', lt, Nat.mod_eq_of_lt]
+
+/-- Prove equality of bitvectors in terms of nat operations. -/
+theorem eq_of_toNat_eq {n} : ∀ {i j : BitVec n}, i.toNat = j.toNat → i = j
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+@[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl
+
+theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
+  Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
+
+theorem toNat_lt (x : BitVec n) : x.toNat < 2^n := x.toFin.2
+
+theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsb i := rfl
+
+@[simp] theorem getLsb_ofFin (x : Fin (2^n)) (i : Nat) :
+  getLsb (BitVec.ofFin x) i = x.val.testBit i := rfl
+
+@[simp] theorem getLsb_ge (x : BitVec w) (i : Nat) (ge : i ≥ w) : getLsb x i = false := by
+  let ⟨x, x_lt⟩ := x
+  simp
+  apply Nat.testBit_lt_two_pow
+  have p : 2^w ≤ 2^i := Nat.pow_le_pow_of_le_right (by omega) ge
+  omega
+
+theorem lt_of_getLsb (x : BitVec w) (i : Nat) : getLsb x i = true → i < w := by
+  if h : i < w then
+    simp [h]
+  else
+    simp [Nat.ge_of_not_lt h]
+
+-- We choose `eq_of_getLsb_eq` as the `@[ext]` theorem for `BitVec`
+-- somewhat arbitrarily over `eq_of_getMsg_eq`.
+@[ext] theorem eq_of_getLsb_eq {x y : BitVec w}
+    (pred : ∀(i : Fin w), x.getLsb i.val = y.getLsb i.val) : x = y := by
+  apply eq_of_toNat_eq
+  apply Nat.eq_of_testBit_eq
+  intro i
+  if i_lt : i < w then
+    exact pred ⟨i, i_lt⟩
+  else
+    have p : i ≥ w := Nat.le_of_not_gt i_lt
+    simp [testBit_toNat, getLsb_ge _ _ p]
+
+theorem eq_of_getMsb_eq {x y : BitVec w}
+    (pred : ∀(i : Fin w), x.getMsb i = y.getMsb i.val) : x = y := by
+  simp only [getMsb] at pred
+  apply eq_of_getLsb_eq
+  intro ⟨i, i_lt⟩
+  if w_zero : w = 0 then
+    simp [w_zero]
+  else
+    have w_pos := Nat.pos_of_ne_zero w_zero
+    have r : i ≤ w - 1 := by
+      simp [Nat.le_sub_iff_add_le w_pos, Nat.add_succ]
+      exact i_lt
+    have q_lt : w - 1 - i < w := by
+      simp only [Nat.sub_sub]
+      apply Nat.sub_lt w_pos
+      simp [Nat.succ_add]
+    have q := pred ⟨w - 1 - i, q_lt⟩
+    simpa [q_lt, Nat.sub_sub_self, r] using q
+
+theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+@[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
+  cases b <;> rfl
+
+theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  by
+  rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']
+
+theorem ofBool_eq_iff_eq : ∀(b b' : Bool), BitVec.ofBool b = BitVec.ofBool b' ↔ b = b' := by
+  decide
+
+@[simp] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
+
+@[simp] theorem toNat_ofNat (x w : Nat) : (x#w).toNat = x % 2^w := by
+  simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
+
+-- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
+-- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
+theorem getLsb_ofNat (n : Nat) (x : Nat) (i : Nat) :
+  getLsb (x#n) i = (i < n && x.testBit i) := by
+  simp [getLsb, BitVec.ofNat, Fin.val_ofNat']
+
+@[deprecated toNat_ofNat] theorem toNat_zero (n : Nat) : (0#n).toNat = 0 := by trivial
+
+@[simp] theorem toNat_mod_cancel (x : BitVec n) : x.toNat % (2^n) = x.toNat :=
+  Nat.mod_eq_of_lt x.isLt
+
+private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
+  Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)
+
+@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : x.toNat#m = truncate m x := by
+  let ⟨x, lt_n⟩ := x
+  unfold truncate
+  unfold zeroExtend
+  if h : n ≤ m then
+    unfold zeroExtend'
+    have lt_m : x < 2 ^ m := lt_two_pow_of_le lt_n h
+    simp [h, lt_m, Nat.mod_eq_of_lt, BitVec.toNat, BitVec.ofNat, Fin.ofNat']
+  else
+    simp [h]
+
+
+/-! ### msb -/
+
+theorem msb_eq_decide (x : BitVec (Nat.succ w)) : BitVec.msb x = decide (2 ^ w ≤ x.toNat) := by
+  simp only [BitVec.msb, getMsb, Nat.zero_lt_succ,
+    decide_True, getLsb, Nat.testBit, Nat.succ_sub_succ_eq_sub,
+    Nat.sub_zero, Nat.and_one_is_mod, Bool.true_and, Nat.shiftRight_eq_div_pow]
+  rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h
+  · simp [Nat.div_eq_of_lt h, h]
+  · simp only [h]
+    rw [Nat.div_eq_sub_div (Nat.two_pow_pos w) h, Nat.div_eq_of_lt]
+    · decide
+    · have : BitVec.toNat x < 2^w + 2^w := by simpa [Nat.pow_succ, Nat.mul_two] using x.isLt
+      omega
+
+/-! ### cast -/
+
+@[simp] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
+@[simp] theorem toFin_cast (h : w = v) (x : BitVec w) :
+    (cast h x).toFin = x.toFin.cast (by rw [h]) :=
+  rfl
+
+@[simp] theorem getLsb_cast (h : w = v) (x : BitVec w) : (cast h x).getLsb i = x.getLsb i := by
+  subst h; simp
+
+@[simp] theorem getMsb_cast (h : w = v) (x : BitVec w) : (cast h x).getMsb i = x.getMsb i := by
+  subst h; simp
+@[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
+  simp [BitVec.msb]
+
+/-! ### zeroExtend and truncate -/
+
+@[simp] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
+    (zeroExtend' p x).toNat = x.toNat := by
+  unfold zeroExtend'
+  simp [p, x.isLt, Nat.mod_eq_of_lt]
+
+theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
+    BitVec.toNat (zeroExtend i x) = x.toNat % 2^i := by
+  let ⟨x, lt_n⟩ := x
+  simp only [zeroExtend]
+  if n_le_i : n ≤ i then
+    have x_lt_two_i : x < 2 ^ i := lt_two_pow_of_le lt_n n_le_i
+    simp [n_le_i, Nat.mod_eq_of_lt, x_lt_two_i]
+  else
+    simp [n_le_i, toNat_ofNat]
+
+@[simp] theorem zeroExtend_eq (x : BitVec n) : zeroExtend n x = x := by
+  apply eq_of_toNat_eq
+  let ⟨x, lt_n⟩ := x
+  simp [truncate, zeroExtend]
+
+@[simp] theorem zeroExtend_zero (m n : Nat) : zeroExtend m (0#n) = 0#m := by
+  apply eq_of_toNat_eq
+  simp [toNat_zeroExtend]
+
+@[simp] theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
+
+@[simp] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
+  toNat_zeroExtend i x
+
+@[simp] theorem getLsb_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getLsb (zeroExtend' ge x) i = getLsb x i := by
+  simp [getLsb, toNat_zeroExtend']
+
+@[simp] theorem getLsb_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
+    getLsb (zeroExtend m x) i = (decide (i < m) && getLsb x i) := by
+  simp [getLsb, toNat_zeroExtend, Nat.testBit_mod_two_pow]
+
+@[simp] theorem getLsb_truncate (m : Nat) (x : BitVec n) (i : Nat) :
+    getLsb (truncate m x) i = (decide (i < m) && getLsb x i) :=
+  getLsb_zeroExtend m x i
+
+/-! ## extractLsb -/
+
+@[simp]
+protected theorem extractLsb_ofFin {n} (x : Fin (2^n)) (hi lo : Nat) :
+  extractLsb hi lo (@BitVec.ofFin n x) = .ofNat (hi-lo+1) (x.val >>> lo) := rfl
+
+@[simp]
+protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
+  extractLsb hi lo x#n = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo) := by
+  apply eq_of_getLsb_eq
+  intro ⟨i, _lt⟩
+  simp [BitVec.ofNat]
+
+@[simp] theorem extractLsb'_toNat (s m : Nat) (x : BitVec n) :
+  (extractLsb' s m x).toNat = (x.toNat >>> s) % 2^m := rfl
+
+@[simp] theorem extractLsb_toNat (hi lo : Nat) (x : BitVec n) :
+  (extractLsb hi lo x).toNat = (x.toNat >>> lo) % 2^(hi-lo+1) := rfl
+
+@[simp] theorem getLsb_extract (hi lo : Nat) (x : BitVec n) (i : Nat) :
+    getLsb (extractLsb hi lo x) i = (i ≤ (hi-lo) && getLsb x (lo+i)) := by
+  unfold getLsb
+  simp [Nat.lt_succ]
+
+/-! ### allOnes -/
+
+private theorem allOnes_def :
+    allOnes v = .ofFin (⟨0, Nat.two_pow_pos v⟩ - ⟨1 % 2^v, Nat.mod_lt _ (Nat.two_pow_pos v)⟩) := by
+  rfl
+
+@[simp] theorem toNat_allOnes : (allOnes v).toNat = 2^v - 1 := by
+  simp only [allOnes_def, toNat_ofFin, Fin.coe_sub, Nat.zero_add]
+  by_cases h : v = 0
+  · subst h
+    rfl
+  · rw [Nat.mod_eq_of_lt (Nat.one_lt_two_pow h), Nat.mod_eq_of_lt]
+    exact Nat.pred_lt_self (Nat.two_pow_pos v)
+
+@[simp] theorem getLsb_allOnes : (allOnes v).getLsb i = decide (i < v) := by
+  simp only [allOnes_def, getLsb_ofFin, Fin.coe_sub, Nat.zero_add, Nat.testBit_mod_two_pow]
+  if h : i < v then
+    simp only [h, decide_True, Bool.true_and]
+    match i, v, h with
+    | i, (v + 1), h =>
+      rw [Nat.mod_eq_of_lt (by simp), Nat.testBit_two_pow_sub_one]
+      simp [h]
+  else
+    simp [h]
+
+@[simp] theorem negOne_eq_allOnes : -1#w = allOnes w :=
+  rfl
+
+/-! ### or -/
+
+@[simp] theorem toNat_or (x y : BitVec v) :
+    BitVec.toNat (x ||| y) = BitVec.toNat x ||| BitVec.toNat y := rfl
+
+@[simp] theorem toFin_or (x y : BitVec v) :
+    BitVec.toFin (x ||| y) = BitVec.toFin x ||| BitVec.toFin y := by
+  simp only [HOr.hOr, OrOp.or, BitVec.or, Fin.lor, val_toFin, Fin.mk.injEq]
+  exact (Nat.mod_eq_of_lt <| Nat.or_lt_two_pow x.isLt y.isLt).symm
+
+
+@[simp] theorem getLsb_or {x y : BitVec v} : (x ||| y).getLsb i = (x.getLsb i || y.getLsb i) := by
+  rw [← testBit_toNat, getLsb, getLsb]
+  simp
+
+/-! ### and -/
+
+@[simp] theorem toNat_and (x y : BitVec v) :
+    BitVec.toNat (x &&& y) = BitVec.toNat x &&& BitVec.toNat y := rfl
+
+@[simp] theorem toFin_and (x y : BitVec v) :
+    BitVec.toFin (x &&& y) = BitVec.toFin x &&& BitVec.toFin y := by
+  simp only [HAnd.hAnd, AndOp.and, BitVec.and, Fin.land, val_toFin, Fin.mk.injEq]
+  exact (Nat.mod_eq_of_lt <| Nat.and_lt_two_pow _ y.isLt).symm
+
+@[simp] theorem getLsb_and {x y : BitVec v} : (x &&& y).getLsb i = (x.getLsb i && y.getLsb i) := by
+  rw [← testBit_toNat, getLsb, getLsb]
+  simp
+
+/-! ### xor -/
+
+@[simp] theorem toNat_xor (x y : BitVec v) :
+    BitVec.toNat (x ^^^ y) = BitVec.toNat x ^^^ BitVec.toNat y := rfl
+
+@[simp] theorem toFin_xor (x y : BitVec v) :
+    BitVec.toFin (x ^^^ y) = BitVec.toFin x ^^^ BitVec.toFin y := by
+  simp only [HXor.hXor, Xor.xor, BitVec.xor, Fin.xor, val_toFin, Fin.mk.injEq]
+  exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm
+
+@[simp] theorem getLsb_xor {x y : BitVec v} :
+    (x ^^^ y).getLsb i = (xor (x.getLsb i) (y.getLsb i)) := by
+  rw [← testBit_toNat, getLsb, getLsb]
+  simp
+
+/-! ### not -/
+
+theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
+
+@[simp] theorem toNat_not {x : BitVec v} : (~~~x).toNat = 2^v - 1 - x.toNat := by
+  rw [Nat.sub_sub, Nat.add_comm, not_def, toNat_xor]
+  apply Nat.eq_of_testBit_eq
+  intro i
+  simp only [toNat_allOnes, Nat.testBit_xor, Nat.testBit_two_pow_sub_one]
+  match h : BitVec.toNat x with
+  | 0 => simp
+  | y+1 =>
+    rw [Nat.succ_eq_add_one] at h
+    rw [← h]
+    rw [Nat.testBit_two_pow_sub_succ (toNat_lt _)]
+    · cases w : decide (i < v)
+      · simp at w
+        simp [w]
+        rw [Nat.testBit_lt_two_pow]
+        calc BitVec.toNat x < 2 ^ v := toNat_lt _
+          _ ≤ 2 ^ i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two w
+      · simp
+
+@[simp] theorem toFin_not (x : BitVec w) :
+    (~~~x).toFin = x.toFin.rev := by
+  apply Fin.val_inj.mp
+  simp only [val_toFin, toNat_not, Fin.val_rev]
+  omega
+
+@[simp] theorem getLsb_not {x : BitVec v} : (~~~x).getLsb i = (decide (i < v) && ! x.getLsb i) := by
+  by_cases h' : i < v <;> simp_all [not_def]
+
+/-! ### shiftLeft -/
+
+@[simp] theorem toNat_shiftLeft {x : BitVec v} :
+    BitVec.toNat (x <<< n) = BitVec.toNat x <<< n % 2^v :=
+  BitVec.toNat_ofNat _ _
+
+@[simp] theorem toFin_shiftLeft {n : Nat} (x : BitVec w) :
+    BitVec.toFin (x <<< n) = Fin.ofNat' (x.toNat <<< n) (Nat.two_pow_pos w) := rfl
+
+@[simp] theorem getLsb_shiftLeft (x : BitVec m) (n) :
+    getLsb (x <<< n) i = (decide (i < m) && !decide (i < n) && getLsb x (i - n)) := by
+  rw [← testBit_toNat, getLsb]
+  simp only [toNat_shiftLeft, Nat.testBit_mod_two_pow, Nat.testBit_shiftLeft, ge_iff_le]
+  -- This step could be a case bashing tactic.
+  cases h₁ : decide (i < m) <;> cases h₂ : decide (n ≤ i) <;> cases h₃ : decide (i < n)
+  all_goals { simp_all <;> omega }
+
+theorem shiftLeftZeroExtend_eq {x : BitVec w} :
+    shiftLeftZeroExtend x n = zeroExtend (w+n) x <<< n := by
+  apply eq_of_toNat_eq
+  rw [shiftLeftZeroExtend, zeroExtend]
+  split
+  · simp
+    rw [Nat.mod_eq_of_lt]
+    rw [Nat.shiftLeft_eq, Nat.pow_add]
+    exact Nat.mul_lt_mul_of_pos_right (BitVec.toNat_lt x) (Nat.two_pow_pos _)
+  · omega
+
+@[simp] theorem getLsb_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
+    getLsb (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsb x (i - n)) := by
+  rw [shiftLeftZeroExtend_eq]
+  simp only [getLsb_shiftLeft, getLsb_zeroExtend]
+  cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n) <;> cases h₃ : decide (i < m + n)
+    <;> simp_all
+    <;> (rw [getLsb_ge]; omega)
+
+/-! ### ushiftRight -/
+
+@[simp] theorem toNat_ushiftRight (x : BitVec n) (i : Nat) :
+    (x >>> i).toNat = x.toNat >>> i := rfl
+
+@[simp] theorem getLsb_ushiftRight (x : BitVec n) (i j : Nat) :
+    getLsb (x >>> i) j = getLsb x (i+j) := by
+  unfold getLsb ; simp
+
+/-! ### append -/
+
+theorem append_def (x : BitVec v) (y : BitVec w) :
+    x ++ y = (shiftLeftZeroExtend x w ||| zeroExtend' (Nat.le_add_left w v) y) := rfl
+
+@[simp] theorem toNat_append (x : BitVec m) (y : BitVec n) :
+    (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
+  rfl
+
+@[simp] theorem getLsb_append {v : BitVec n} {w : BitVec m} :
+    getLsb (v ++ w) i = bif i < m then getLsb w i else getLsb v (i - m) := by
+  simp [append_def]
+  by_cases h : i < m
+  · simp [h]
+  · simp [h]; simp_all
+
+/-! ### rev -/
+
+theorem getLsb_rev (x : BitVec w) (i : Fin w) :
+    x.getLsb i.rev = x.getMsb i := by
+  simp [getLsb, getMsb]
+  congr 1
+  omega
+
+theorem getMsb_rev (x : BitVec w) (i : Fin w) :
+    x.getMsb i.rev = x.getLsb i := by
+  simp only [← getLsb_rev]
+  simp only [Fin.rev]
+  congr
+  omega
+
+/-! ### cons -/
+
+@[simp] theorem toNat_cons (b : Bool) (x : BitVec w) :
+    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat := by
+  let ⟨x, _⟩ := x
+  simp [cons, toNat_append, toNat_ofBool]
+
+@[simp] theorem getLsb_cons (b : Bool) {n} (x : BitVec n) (i : Nat) :
+    getLsb (cons b x) i = if i = n then b else getLsb x i := by
+  simp only [getLsb, toNat_cons, Nat.testBit_or]
+  rw [Nat.testBit_shiftLeft]
+  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
+  · have p1 : ¬(n ≤ i) := by omega
+    have p2 : i ≠ n := by omega
+    simp [p1, p2]
+  · simp [i_eq_n, testBit_toNat]
+    cases b <;> trivial
+  · have p1 : i ≠ n := by omega
+    have p2 : i - n ≠ 0 := by omega
+    simp [p1, p2, Nat.testBit_bool_to_nat]
+
+theorem truncate_succ (x : BitVec w) :
+    truncate (i+1) x = cons (getLsb x i) (truncate i x) := by
+  apply eq_of_getLsb_eq
+  intro j
+  simp only [getLsb_truncate, getLsb_cons, j.isLt, decide_True, Bool.true_and]
+  if j_eq : j.val = i then
+    simp [j_eq]
+  else
+    have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
+    simp [j_eq, j_lt]
+
+/-! ### add -/
+
+theorem add_def {n} (x y : BitVec n) : x + y = .ofNat n (x.toNat + y.toNat) := rfl
+
+/--
+Definition of bitvector addition as a nat.
+-/
+@[simp] theorem toNat_add (x y : BitVec w) : (x + y).toNat = (x.toNat + y.toNat) % 2^w := rfl
+@[simp] theorem toFin_add (x y : BitVec w) : (x + y).toFin = toFin x + toFin y := rfl
+@[simp] theorem ofFin_add (x : Fin (2^n)) (y : BitVec n) :
+  .ofFin x + y = .ofFin (x + y.toFin) := rfl
+@[simp] theorem add_ofFin (x : BitVec n) (y : Fin (2^n)) :
+  x + .ofFin y = .ofFin (x.toFin + y) := rfl
+@[simp] theorem ofNat_add_ofNat {n} (x y : Nat) : x#n + y#n = (x + y)#n := by
+  apply eq_of_toNat_eq ; simp [BitVec.ofNat]
+
+protected theorem add_assoc (x y z : BitVec n) : x + y + z = x + (y + z) := by
+  apply eq_of_toNat_eq ; simp [Nat.add_assoc]
+
+protected theorem add_comm (x y : BitVec n) : x + y = y + x := by
+  simp [add_def, Nat.add_comm]
+
+@[simp] protected theorem add_zero (x : BitVec n) : x + 0#n = x := by simp [add_def]
+
+@[simp] protected theorem zero_add (x : BitVec n) : 0#n + x = x := by simp [add_def]
+
+
+/-! ### sub/neg -/
+
+theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n (x.toNat + (2^n - y.toNat)) := by rfl
+
+@[simp] theorem toNat_sub {n} (x y : BitVec n) :
+  (x - y).toNat = ((x.toNat + (2^n - y.toNat)) % 2^n) := rfl
+@[simp] theorem toFin_sub (x y : BitVec n) : (x - y).toFin = toFin x - toFin y := rfl
+
+@[simp] theorem ofFin_sub (x : Fin (2^n)) (y : BitVec n) : .ofFin x - y = .ofFin (x - y.toFin) :=
+  rfl
+@[simp] theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
+  rfl
+-- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
+-- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
+theorem ofNat_sub_ofNat {n} (x y : Nat) : x#n - y#n = .ofNat n (x + (2^n - y % 2^n)) := by
+  apply eq_of_toNat_eq ; simp [BitVec.ofNat]
+
+@[simp] protected theorem sub_zero (x : BitVec n) : x - (0#n) = x := by apply eq_of_toNat_eq ; simp
+
+@[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by
+  apply eq_of_toNat_eq
+  simp only [toNat_sub]
+  rw [Nat.add_sub_of_le]
+  · simp
+  · exact Nat.le_of_lt x.isLt
+
+@[simp] theorem toNat_neg (x : BitVec n) : (- x).toNat = (2^n - x.toNat) % 2^n := by
+  simp [Neg.neg, BitVec.neg]
+
+theorem sub_toAdd {n} (x y : BitVec n) : x - y = x + - y := by
+  apply eq_of_toNat_eq
+  simp
+
+@[simp] theorem neg_zero (n:Nat) : -0#n = 0#n := by apply eq_of_toNat_eq ; simp
+
+theorem add_sub_cancel (x y : BitVec w) : x + y - y = x := by
+  apply eq_of_toNat_eq
+  have y_toNat_le := Nat.le_of_lt y.toNat_lt
+  rw [toNat_sub, toNat_add, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
+    Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]
+
+/-! ### mul -/
+
+theorem mul_def {n} {x y : BitVec n} : x * y = (ofFin <| x.toFin * y.toFin) := by rfl
+
+theorem toNat_mul (x y : BitVec n) : (x * y).toNat = (x.toNat * y.toNat) % 2 ^ n := rfl
+@[simp] theorem toFin_mul (x y : BitVec n) : (x * y).toFin = (x.toFin * y.toFin) := rfl
+
+/-! ### le and lt -/
+
+theorem le_def (x y : BitVec n) :
+  x ≤ y ↔ x.toNat ≤ y.toNat := Iff.rfl
+
+@[simp] theorem le_ofFin (x : BitVec n) (y : Fin (2^n)) :
+  x ≤ BitVec.ofFin y ↔ x.toFin ≤ y := Iff.rfl
+@[simp] theorem ofFin_le (x : Fin (2^n)) (y : BitVec n) :
+  BitVec.ofFin x ≤ y ↔ x ≤ y.toFin := Iff.rfl
+@[simp] theorem ofNat_le_ofNat {n} (x y : Nat) : (x#n) ≤ (y#n) ↔ x % 2^n ≤ y % 2^n := by
+  simp [le_def]
+
+theorem lt_def (x y : BitVec n) :
+  x < y ↔ x.toNat < y.toNat := Iff.rfl
+
+@[simp] theorem lt_ofFin (x : BitVec n) (y : Fin (2^n)) :
+  x < BitVec.ofFin y ↔ x.toFin < y := Iff.rfl
+@[simp] theorem ofFin_lt (x : Fin (2^n)) (y : BitVec n) :
+  BitVec.ofFin x < y ↔ x < y.toFin := Iff.rfl
+@[simp] theorem ofNat_lt_ofNat {n} (x y : Nat) : (x#n) < (y#n) ↔ x % 2^n < y % 2^n := by
+  simp [lt_def]
+
+protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x < y := by
+  revert h1 h2
+  let ⟨x, lt⟩ := x
+  let ⟨y, lt⟩ := y
+  simp
+  exact Nat.lt_of_le_of_ne

src/Init/Data/Fin.lean

@@ -8,3 +8,4 @@ import Init.Data.Fin.Basic
 import Init.Data.Fin.Log2
 import Init.Data.Fin.Iterate
 import Init.Data.Fin.Fold
+import Init.Data.Fin.Lemmas

src/Init/Data/Fin/Basic.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura, Robert Y. Lewis, Keeley Hoek, Mario Carneiro
 -/
 prelude
 import Init.Data.Nat.Div
-import Init.Data.Nat.Bitwise
+import Init.Data.Nat.Bitwise.Basic
 import Init.Coe
 
 open Nat

src/Init/Data/Fin/Lemmas.lean

@@ -0,0 +1,830 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+prelude
+import Init.Data.Fin.Basic
+import Init.Data.Nat.Lemmas
+import Init.Ext
+import Init.ByCases
+import Init.Conv
+import Init.Omega
+
+namespace Fin
+
+/-- If you actually have an element of `Fin n`, then the `n` is always positive -/
+theorem size_pos (i : Fin n) : 0 < n := Nat.lt_of_le_of_lt (Nat.zero_le _) i.2
+
+theorem mod_def (a m : Fin n) : a % m = Fin.mk (a % m) (Nat.lt_of_le_of_lt (Nat.mod_le _ _) a.2) :=
+  rfl
+
+theorem mul_def (a b : Fin n) : a * b = Fin.mk ((a * b) % n) (Nat.mod_lt _ a.size_pos) := rfl
+
+theorem sub_def (a b : Fin n) : a - b = Fin.mk ((a + (n - b)) % n) (Nat.mod_lt _ a.size_pos) := rfl
+
+theorem size_pos' : ∀ [Nonempty (Fin n)], 0 < n | ⟨i⟩ => i.size_pos
+
+@[simp] theorem is_lt (a : Fin n) : (a : Nat) < n := a.2
+
+theorem pos_iff_nonempty {n : Nat} : 0 < n ↔ Nonempty (Fin n) :=
+  ⟨fun h => ⟨⟨0, h⟩⟩, fun ⟨i⟩ => i.pos⟩
+
+/-! ### coercions and constructions -/
+
+@[simp] protected theorem eta (a : Fin n) (h : a < n) : (⟨a, h⟩ : Fin n) = a := rfl
+
+@[ext] theorem ext {a b : Fin n} (h : (a : Nat) = b) : a = b := eq_of_val_eq h
+
+theorem val_inj {a b : Fin n} : a.1 = b.1 ↔ a = b := ⟨Fin.eq_of_val_eq, Fin.val_eq_of_eq⟩
+
+theorem ext_iff {a b : Fin n} : a = b ↔ a.1 = b.1 := val_inj.symm
+
+theorem val_ne_iff {a b : Fin n} : a.1 ≠ b.1 ↔ a ≠ b := not_congr val_inj
+
+theorem exists_iff {p : Fin n → Prop} : (∃ i, p i) ↔ ∃ i h, p ⟨i, h⟩ :=
+  ⟨fun ⟨⟨i, hi⟩, hpi⟩ => ⟨i, hi, hpi⟩, fun ⟨i, hi, hpi⟩ => ⟨⟨i, hi⟩, hpi⟩⟩
+
+theorem forall_iff {p : Fin n → Prop} : (∀ i, p i) ↔ ∀ i h, p ⟨i, h⟩ :=
+  ⟨fun h i hi => h ⟨i, hi⟩, fun h ⟨i, hi⟩ => h i hi⟩
+
+protected theorem mk.inj_iff {n a b : Nat} {ha : a < n} {hb : b < n} :
+    (⟨a, ha⟩ : Fin n) = ⟨b, hb⟩ ↔ a = b := ext_iff
+
+theorem val_mk {m n : Nat} (h : m < n) : (⟨m, h⟩ : Fin n).val = m := rfl
+
+theorem eq_mk_iff_val_eq {a : Fin n} {k : Nat} {hk : k < n} :
+    a = ⟨k, hk⟩ ↔ (a : Nat) = k := ext_iff
+
+theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
+
+@[simp] theorem val_ofNat' (a : Nat) (is_pos : n > 0) :
+  (Fin.ofNat' a is_pos).val = a % n := rfl
+
+@[deprecated ofNat'_zero_val] theorem ofNat'_zero_val : (Fin.ofNat' 0 h).val = 0 := Nat.zero_mod _
+
+@[simp] theorem mod_val (a b : Fin n) : (a % b).val = a.val % b.val :=
+  rfl
+
+@[simp] theorem div_val (a b : Fin n) : (a / b).val = a.val / b.val :=
+  rfl
+
+@[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
+  rfl
+
+theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) :
+    (if h : c then x h else y h).val = if h : c then (x h).val else (y h).val := by
+  by_cases c <;> simp [*]
+
+theorem dite_val {n : Nat} {c : Prop} [Decidable c] {x y : Fin n} :
+    (if c then x else y).val = if c then x.val else y.val := by
+  by_cases c <;> simp [*]
+
+/-! ### order -/
+
+theorem le_def {a b : Fin n} : a ≤ b ↔ a.1 ≤ b.1 := .rfl
+
+theorem lt_def {a b : Fin n} : a < b ↔ a.1 < b.1 := .rfl
+
+theorem lt_iff_val_lt_val {a b : Fin n} : a < b ↔ a.val < b.val := Iff.rfl
+
+@[simp] protected theorem not_le {a b : Fin n} : ¬ a ≤ b ↔ b < a := Nat.not_le
+
+@[simp] protected theorem not_lt {a b : Fin n} : ¬ a < b ↔ b ≤ a := Nat.not_lt
+
+protected theorem ne_of_lt {a b : Fin n} (h : a < b) : a ≠ b := Fin.ne_of_val_ne (Nat.ne_of_lt h)
+
+protected theorem ne_of_gt {a b : Fin n} (h : a < b) : b ≠ a := Fin.ne_of_val_ne (Nat.ne_of_gt h)
+
+protected theorem le_of_lt {a b : Fin n} (h : a < b) : a ≤ b := Nat.le_of_lt h
+
+theorem is_le (i : Fin (n + 1)) : i ≤ n := Nat.le_of_lt_succ i.is_lt
+
+@[simp] theorem is_le' {a : Fin n} : a ≤ n := Nat.le_of_lt a.is_lt
+
+theorem mk_lt_of_lt_val {b : Fin n} {a : Nat} (h : a < b) :
+    (⟨a, Nat.lt_trans h b.is_lt⟩ : Fin n) < b := h
+
+theorem mk_le_of_le_val {b : Fin n} {a : Nat} (h : a ≤ b) :
+    (⟨a, Nat.lt_of_le_of_lt h b.is_lt⟩ : Fin n) ≤ b := h
+
+@[simp] theorem mk_le_mk {x y : Nat} {hx hy} : (⟨x, hx⟩ : Fin n) ≤ ⟨y, hy⟩ ↔ x ≤ y := .rfl
+
+@[simp] theorem mk_lt_mk {x y : Nat} {hx hy} : (⟨x, hx⟩ : Fin n) < ⟨y, hy⟩ ↔ x < y := .rfl
+
+@[simp] theorem val_zero (n : Nat) : (0 : Fin (n + 1)).1 = 0 := rfl
+
+@[simp] theorem mk_zero : (⟨0, Nat.succ_pos n⟩ : Fin (n + 1)) = 0 := rfl
+
+@[simp] theorem zero_le (a : Fin (n + 1)) : 0 ≤ a := Nat.zero_le a.val
+
+theorem zero_lt_one : (0 : Fin (n + 2)) < 1 := Nat.zero_lt_one
+
+@[simp] theorem not_lt_zero (a : Fin (n + 1)) : ¬a < 0 := nofun
+
+theorem pos_iff_ne_zero {a : Fin (n + 1)} : 0 < a ↔ a ≠ 0 := by
+  rw [lt_def, val_zero, Nat.pos_iff_ne_zero, ← val_ne_iff]; rfl
+
+theorem eq_zero_or_eq_succ {n : Nat} : ∀ i : Fin (n + 1), i = 0 ∨ ∃ j : Fin n, i = j.succ
+  | 0 => .inl rfl
+  | ⟨j + 1, h⟩ => .inr ⟨⟨j, Nat.lt_of_succ_lt_succ h⟩, rfl⟩
+
+theorem eq_succ_of_ne_zero {n : Nat} {i : Fin (n + 1)} (hi : i ≠ 0) : ∃ j : Fin n, i = j.succ :=
+  (eq_zero_or_eq_succ i).resolve_left hi
+
+@[simp] theorem val_rev (i : Fin n) : rev i = n - (i + 1) := rfl
+
+@[simp] theorem rev_rev (i : Fin n) : rev (rev i) = i := ext <| by
+  rw [val_rev, val_rev, ← Nat.sub_sub, Nat.sub_sub_self (by exact i.2), Nat.add_sub_cancel]
+
+@[simp] theorem rev_le_rev {i j : Fin n} : rev i ≤ rev j ↔ j ≤ i := by
+  simp only [le_def, val_rev, Nat.sub_le_sub_iff_left (Nat.succ_le.2 j.is_lt)]
+  exact Nat.succ_le_succ_iff
+
+@[simp] theorem rev_inj {i j : Fin n} : rev i = rev j ↔ i = j :=
+  ⟨fun h => by simpa using congrArg rev h, congrArg _⟩
+
+theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
+    rev i = ⟨a, Nat.lt_succ_of_le (h ▸ Nat.le_add_right ..)⟩ := by
+  ext; dsimp
+  conv => lhs; congr; rw [h]
+  rw [Nat.add_assoc, Nat.add_sub_cancel]
+
+@[simp] theorem rev_lt_rev {i j : Fin n} : rev i < rev j ↔ j < i := by
+  rw [← Fin.not_le, ← Fin.not_le, rev_le_rev]
+
+@[simp] theorem val_last (n : Nat) : last n = n := rfl
+
+theorem le_last (i : Fin (n + 1)) : i ≤ last n := Nat.le_of_lt_succ i.is_lt
+
+theorem last_pos : (0 : Fin (n + 2)) < last (n + 1) := Nat.succ_pos _
+
+theorem eq_last_of_not_lt {i : Fin (n + 1)} (h : ¬(i : Nat) < n) : i = last n :=
+  ext <| Nat.le_antisymm (le_last i) (Nat.not_lt.1 h)
+
+theorem val_lt_last {i : Fin (n + 1)} : i ≠ last n → (i : Nat) < n :=
+  Decidable.not_imp_comm.1 eq_last_of_not_lt
+
+@[simp] theorem rev_last (n : Nat) : rev (last n) = 0 := ext <| by simp
+
+@[simp] theorem rev_zero (n : Nat) : rev 0 = last n := by
+  rw [← rev_rev (last _), rev_last]
+
+/-! ### addition, numerals, and coercion from Nat -/
+
+@[simp] theorem val_one (n : Nat) : (1 : Fin (n + 2)).val = 1 := rfl
+
+@[simp] theorem mk_one : (⟨1, Nat.succ_lt_succ (Nat.succ_pos n)⟩ : Fin (n + 2)) = (1 : Fin _) := rfl
+
+theorem subsingleton_iff_le_one : Subsingleton (Fin n) ↔ n ≤ 1 := by
+  (match n with | 0 | 1 | n+2 => ?_) <;> try simp
+  · exact ⟨nofun⟩
+  · exact ⟨fun ⟨0, _⟩ ⟨0, _⟩ => rfl⟩
+  · exact iff_of_false (fun h => Fin.ne_of_lt zero_lt_one (h.elim ..)) (of_decide_eq_false rfl)
+
+instance subsingleton_zero : Subsingleton (Fin 0) := subsingleton_iff_le_one.2 (by decide)
+
+instance subsingleton_one : Subsingleton (Fin 1) := subsingleton_iff_le_one.2 (by decide)
+
+theorem fin_one_eq_zero (a : Fin 1) : a = 0 := Subsingleton.elim a 0
+
+theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.size_pos) := rfl
+
+theorem val_add (a b : Fin n) : (a + b).val = (a.val + b.val) % n := rfl
+
+theorem val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last _) : (i + 1).1 = i + 1 := by
+  match n with
+  | 0 => cases h
+  | n+1 => rw [val_add, val_one, Nat.mod_eq_of_lt (by exact Nat.succ_lt_succ h)]
+
+@[simp] theorem last_add_one : ∀ n, last n + 1 = 0
+  | 0 => rfl
+  | n + 1 => by ext; rw [val_add, val_zero, val_last, val_one, Nat.mod_self]
+
+theorem val_add_one {n : Nat} (i : Fin (n + 1)) :
+    ((i + 1 : Fin (n + 1)) : Nat) = if i = last _ then (0 : Nat) else i + 1 := by
+  match Nat.eq_or_lt_of_le (le_last i) with
+  | .inl h => cases Fin.eq_of_val_eq h; simp
+  | .inr h => simpa [Fin.ne_of_lt h] using val_add_one_of_lt h
+
+@[simp] theorem val_two {n : Nat} : (2 : Fin (n + 3)).val = 2 := rfl
+
+theorem add_one_pos (i : Fin (n + 1)) (h : i < Fin.last n) : (0 : Fin (n + 1)) < i + 1 := by
+  match n with
+  | 0 => cases h
+  | n+1 =>
+    rw [Fin.lt_def, val_last, ← Nat.add_lt_add_iff_right] at h
+    rw [Fin.lt_def, val_add, val_zero, val_one, Nat.mod_eq_of_lt h]
+    exact Nat.zero_lt_succ _
+
+theorem one_pos : (0 : Fin (n + 2)) < 1 := Nat.succ_pos 0
+
+theorem zero_ne_one : (0 : Fin (n + 2)) ≠ 1 := Fin.ne_of_lt one_pos
+
+/-! ### succ and casts into larger Fin types -/
+
+@[simp] theorem val_succ (j : Fin n) : (j.succ : Nat) = j + 1 := rfl
+
+@[simp] theorem succ_pos (a : Fin n) : (0 : Fin (n + 1)) < a.succ := by
+  simp [Fin.lt_def, Nat.succ_pos]
+
+@[simp] theorem succ_le_succ_iff {a b : Fin n} : a.succ ≤ b.succ ↔ a ≤ b := Nat.succ_le_succ_iff
+
+@[simp] theorem succ_lt_succ_iff {a b : Fin n} : a.succ < b.succ ↔ a < b := Nat.succ_lt_succ_iff
+
+@[simp] theorem succ_inj {a b : Fin n} : a.succ = b.succ ↔ a = b := by
+  refine ⟨fun h => ext ?_, congrArg _⟩
+  apply Nat.le_antisymm <;> exact succ_le_succ_iff.1 (h ▸ Nat.le_refl _)
+
+theorem succ_ne_zero {n} : ∀ k : Fin n, Fin.succ k ≠ 0
+  | ⟨k, _⟩, heq => Nat.succ_ne_zero k <| ext_iff.1 heq
+
+@[simp] theorem succ_zero_eq_one : Fin.succ (0 : Fin (n + 1)) = 1 := rfl
+
+/-- Version of `succ_one_eq_two` to be used by `dsimp` -/
+@[simp] theorem succ_one_eq_two : Fin.succ (1 : Fin (n + 2)) = 2 := rfl
+
+@[simp] theorem succ_mk (n i : Nat) (h : i < n) :
+    Fin.succ ⟨i, h⟩ = ⟨i + 1, Nat.succ_lt_succ h⟩ := rfl
+
+theorem mk_succ_pos (i : Nat) (h : i < n) :
+    (0 : Fin (n + 1)) < ⟨i.succ, Nat.add_lt_add_right h 1⟩ := by
+  rw [lt_def, val_zero]; exact Nat.succ_pos i
+
+theorem one_lt_succ_succ (a : Fin n) : (1 : Fin (n + 2)) < a.succ.succ := by
+  let n+1 := n
+  rw [← succ_zero_eq_one, succ_lt_succ_iff]; exact succ_pos a
+
+@[simp] theorem add_one_lt_iff {n : Nat} {k : Fin (n + 2)} : k + 1 < k ↔ k = last _ := by
+  simp only [lt_def, val_add, val_last, ext_iff]
+  let ⟨k, hk⟩ := k
+  match Nat.eq_or_lt_of_le (Nat.le_of_lt_succ hk) with
+  | .inl h => cases h; simp [Nat.succ_pos]
+  | .inr hk' => simp [Nat.ne_of_lt hk', Nat.mod_eq_of_lt (Nat.succ_lt_succ hk'), Nat.le_succ]
+
+@[simp] theorem add_one_le_iff {n : Nat} : ∀ {k : Fin (n + 1)}, k + 1 ≤ k ↔ k = last _ := by
+  match n with
+  | 0 =>
+    intro (k : Fin 1)
+    exact iff_of_true (Subsingleton.elim (α := Fin 1) (k+1) _ ▸ Nat.le_refl _) (fin_one_eq_zero ..)
+  | n + 1 =>
+    intro (k : Fin (n+2))
+    rw [← add_one_lt_iff, lt_def, le_def, Nat.lt_iff_le_and_ne, and_iff_left]
+    rw [val_add_one]
+    split <;> simp [*, (Nat.succ_ne_zero _).symm, Nat.ne_of_gt (Nat.lt_succ_self _)]
+
+@[simp] theorem last_le_iff {n : Nat} {k : Fin (n + 1)} : last n ≤ k ↔ k = last n := by
+  rw [ext_iff, Nat.le_antisymm_iff, le_def, and_iff_right (by apply le_last)]
+
+@[simp] theorem lt_add_one_iff {n : Nat} {k : Fin (n + 1)} : k < k + 1 ↔ k < last n := by
+  rw [← Decidable.not_iff_not]; simp
+
+@[simp] theorem le_zero_iff {n : Nat} {k : Fin (n + 1)} : k ≤ 0 ↔ k = 0 :=
+  ⟨fun h => Fin.eq_of_val_eq <| Nat.eq_zero_of_le_zero h, (· ▸ Nat.le_refl _)⟩
+
+theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
+  Fin.ne_of_gt (one_lt_succ_succ a)
+
+@[simp] theorem coe_castLT (i : Fin m) (h : i.1 < n) : (castLT i h : Nat) = i := rfl
+
+@[simp] theorem castLT_mk (i n m : Nat) (hn : i < n) (hm : i < m) : castLT ⟨i, hn⟩ hm = ⟨i, hm⟩ :=
+  rfl
+
+@[simp] theorem coe_castLE (h : n ≤ m) (i : Fin n) : (castLE h i : Nat) = i := rfl
+
+@[simp] theorem castLE_mk (i n m : Nat) (hn : i < n) (h : n ≤ m) :
+    castLE h ⟨i, hn⟩ = ⟨i, Nat.lt_of_lt_of_le hn h⟩ := rfl
+
+@[simp] theorem castLE_zero {n m : Nat} (h : n.succ ≤ m.succ) : castLE h 0 = 0 := by simp [ext_iff]
+
+@[simp] theorem castLE_succ {m n : Nat} (h : m + 1 ≤ n + 1) (i : Fin m) :
+    castLE h i.succ = (castLE (Nat.succ_le_succ_iff.mp h) i).succ := by simp [ext_iff]
+
+@[simp] theorem castLE_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) (i : Fin k) :
+    Fin.castLE mn (Fin.castLE km i) = Fin.castLE (Nat.le_trans km mn) i :=
+  Fin.ext (by simp only [coe_castLE])
+
+@[simp] theorem castLE_comp_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) :
+    Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) :=
+  funext (castLE_castLE km mn)
+
+@[simp] theorem coe_cast (h : n = m) (i : Fin n) : (cast h i : Nat) = i := rfl
+
+@[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : cast h (last n) = last n' :=
+  ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
+
+@[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := rfl
+
+@[simp] theorem cast_trans {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
+    cast h' (cast h i) = cast (Eq.trans h h') i := rfl
+
+theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := rfl
+
+@[simp] theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
+
+@[simp] theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = cast rfl := rfl
+
+theorem castAdd_lt {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m := by simp
+
+@[simp] theorem castAdd_mk (m : Nat) (i : Nat) (h : i < n) :
+    castAdd m ⟨i, h⟩ = ⟨i, Nat.lt_add_right m h⟩ := rfl
+
+@[simp] theorem castAdd_castLT (m : Nat) (i : Fin (n + m)) (hi : i.val < n) :
+    castAdd m (castLT i hi) = i := rfl
+
+@[simp] theorem castLT_castAdd (m : Nat) (i : Fin n) :
+    castLT (castAdd m i) (castAdd_lt m i) = i := rfl
+
+/-- For rewriting in the reverse direction, see `Fin.cast_castAdd_left`. -/
+theorem castAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
+    castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := ext rfl
+
+theorem cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
+    cast h (castAdd m i) = castAdd m (cast (Nat.add_right_cancel h) i) := rfl
+
+@[simp] theorem cast_castAdd_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
+    cast h (castAdd m' i) = castAdd m i := rfl
+
+theorem castAdd_castAdd {m n p : Nat} (i : Fin m) :
+    castAdd p (castAdd n i) = cast (Nat.add_assoc ..).symm (castAdd (n + p) i) := rfl
+
+/-- The cast of the successor is the successor of the cast. See `Fin.succ_cast_eq` for rewriting in
+the reverse direction. -/
+@[simp] theorem cast_succ_eq {n' : Nat} (i : Fin n) (h : n.succ = n'.succ) :
+    cast h i.succ = (cast (Nat.succ.inj h) i).succ := rfl
+
+theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
+    (cast h i).succ = cast (by rw [h]) i.succ := rfl
+
+@[simp] theorem coe_castSucc (i : Fin n) : (Fin.castSucc i : Nat) = i := rfl
+
+@[simp] theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt.step h⟩ := rfl
+
+@[simp] theorem cast_castSucc {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
+    cast h (castSucc i) = castSucc (cast (Nat.succ.inj h) i) := rfl
+
+theorem castSucc_lt_succ (i : Fin n) : Fin.castSucc i < i.succ :=
+  lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
+
+theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ Fin.castSucc j ↔ i < j.succ := by
+  simpa [lt_def, le_def] using Nat.succ_le_succ_iff.symm
+
+theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
+    Fin.castSucc i < j ↔ i.succ ≤ j := .rfl
+
+@[simp] theorem succ_last (n : Nat) : (last n).succ = last n.succ := rfl
+
+@[simp] theorem succ_eq_last_succ {n : Nat} (i : Fin n.succ) :
+    i.succ = last (n + 1) ↔ i = last n := by rw [← succ_last, succ_inj]
+
+@[simp] theorem castSucc_castLT (i : Fin (n + 1)) (h : (i : Nat) < n) :
+    castSucc (castLT i h) = i := rfl
+
+@[simp] theorem castLT_castSucc {n : Nat} (a : Fin n) (h : (a : Nat) < n) :
+    castLT (castSucc a) h = a := rfl
+
+@[simp] theorem castSucc_lt_castSucc_iff {a b : Fin n} :
+    Fin.castSucc a < Fin.castSucc b ↔ a < b := .rfl
+
+theorem castSucc_inj {a b : Fin n} : castSucc a = castSucc b ↔ a = b := by simp [ext_iff]
+
+theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt
+
+@[simp] theorem castSucc_zero : castSucc (0 : Fin (n + 1)) = 0 := rfl
+
+@[simp] theorem castSucc_one {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := rfl
+
+/-- `castSucc i` is positive when `i` is positive -/
+theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < castSucc i := by
+  simpa [lt_def] using h
+
+@[simp] theorem castSucc_eq_zero_iff (a : Fin (n + 1)) : castSucc a = 0 ↔ a = 0 := by simp [ext_iff]
+
+theorem castSucc_ne_zero_iff (a : Fin (n + 1)) : castSucc a ≠ 0 ↔ a ≠ 0 :=
+  not_congr <| castSucc_eq_zero_iff a
+
+theorem castSucc_fin_succ (n : Nat) (j : Fin n) :
+    castSucc (Fin.succ j) = Fin.succ (castSucc j) := by simp [Fin.ext_iff]
+
+@[simp]
+theorem coeSucc_eq_succ {a : Fin n} : castSucc a + 1 = a.succ := by
+  cases n
+  · exact a.elim0
+  · simp [ext_iff, add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ a.is_lt)]
+
+theorem lt_succ {a : Fin n} : castSucc a < a.succ := by
+  rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
+
+theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n :=
+  ⟨fun ⟨j, hj⟩ => hj ▸ Fin.ne_of_lt j.castSucc_lt_last,
+   fun hi => ⟨i.castLT <| Fin.val_lt_last hi, rfl⟩⟩
+
+theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = castSucc i.succ := rfl
+
+@[simp] theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
+
+@[simp] theorem addNat_one {i : Fin n} : addNat i 1 = i.succ := rfl
+
+theorem le_coe_addNat (m : Nat) (i : Fin n) : m ≤ addNat i m :=
+  Nat.le_add_left _ _
+
+@[simp] theorem addNat_mk (n i : Nat) (hi : i < m) :
+    addNat ⟨i, hi⟩ n = ⟨i + n, Nat.add_lt_add_right hi n⟩ := rfl
+
+@[simp] theorem cast_addNat_zero {n n' : Nat} (i : Fin n) (h : n + 0 = n') :
+    cast h (addNat i 0) = cast ((Nat.add_zero _).symm.trans h) i := rfl
+
+/-- For rewriting in the reverse direction, see `Fin.cast_addNat_left`. -/
+theorem addNat_cast {n n' m : Nat} (i : Fin n') (h : n' = n) :
+    addNat (cast h i) m = cast (congrArg (. + m) h) (addNat i m) := rfl
+
+theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
+    cast h (addNat i m) = addNat (cast (Nat.add_right_cancel h) i) m := rfl
+
+@[simp] theorem cast_addNat_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
+    cast h (addNat i m') = addNat i m :=
+  ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
+
+@[simp] theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
+
+@[simp] theorem natAdd_mk (n i : Nat) (hi : i < m) :
+    natAdd n ⟨i, hi⟩ = ⟨n + i, Nat.add_lt_add_left hi n⟩ := rfl
+
+theorem le_coe_natAdd (m : Nat) (i : Fin n) : m ≤ natAdd m i := Nat.le_add_right ..
+
+theorem natAdd_zero {n : Nat} : natAdd 0 = cast (Nat.zero_add n).symm := by ext; simp
+
+/-- For rewriting in the reverse direction, see `Fin.cast_natAdd_right`. -/
+theorem natAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
+    natAdd m (cast h i) = cast (congrArg _ h) (natAdd m i) := rfl
+
+theorem cast_natAdd_right {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
+    cast h (natAdd m i) = natAdd m (cast (Nat.add_left_cancel h) i) := rfl
+
+@[simp] theorem cast_natAdd_left {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
+    cast h (natAdd m' i) = natAdd m i :=
+  ext <| (congrArg (· + (i : Nat)) (Nat.add_right_cancel h) : _)
+
+theorem castAdd_natAdd (p m : Nat) {n : Nat} (i : Fin n) :
+    castAdd p (natAdd m i) = cast (Nat.add_assoc ..).symm (natAdd m (castAdd p i)) := rfl
+
+theorem natAdd_castAdd (p m : Nat) {n : Nat} (i : Fin n) :
+    natAdd m (castAdd p i) = cast (Nat.add_assoc ..) (castAdd p (natAdd m i)) := rfl
+
+theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
+    natAdd m (natAdd n i) = cast (Nat.add_assoc ..) (natAdd (m + n) i) :=
+  ext <| (Nat.add_assoc ..).symm
+
+@[simp]
+theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
+    cast h (natAdd 0 i) = cast ((Nat.zero_add _).symm.trans h) i :=
+  ext <| Nat.zero_add _
+
+@[simp]
+theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :
+    cast (Nat.add_comm ..) (natAdd n i) = addNat i n := ext <| Nat.add_comm ..
+
+@[simp]
+theorem cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
+    cast (Nat.add_comm ..) (addNat i m) = natAdd m i := ext <| Nat.add_comm ..
+
+@[simp] theorem natAdd_last {m n : Nat} : natAdd n (last m) = last (n + m) := rfl
+
+theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) :=
+  rfl
+
+theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := ext <| by
+  rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
+
+theorem rev_addNat (k : Fin n) (m : Nat) : rev (addNat k m) = castAdd m (rev k) := by
+  rw [← rev_rev (castAdd ..), rev_castAdd, rev_rev]
+
+theorem rev_castSucc (k : Fin n) : rev (castSucc k) = succ (rev k) := k.rev_castAdd 1
+
+theorem rev_succ (k : Fin n) : rev (succ k) = castSucc (rev k) := k.rev_addNat 1
+
+/-! ### pred -/
+
+@[simp] theorem coe_pred (j : Fin (n + 1)) (h : j ≠ 0) : (j.pred h : Nat) = j - 1 := rfl
+
+@[simp] theorem succ_pred : ∀ (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i
+  | ⟨0, h⟩, hi => by simp only [mk_zero, ne_eq, not_true] at hi
+  | ⟨n + 1, h⟩, hi => rfl
+
+@[simp]
+theorem pred_succ (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i := by
+  cases i
+  rfl
+
+theorem pred_eq_iff_eq_succ {n : Nat} (i : Fin (n + 1)) (hi : i ≠ 0) (j : Fin n) :
+    i.pred hi = j ↔ i = j.succ :=
+  ⟨fun h => by simp only [← h, Fin.succ_pred], fun h => by simp only [h, Fin.pred_succ]⟩
+
+theorem pred_mk_succ (i : Nat) (h : i < n + 1) :
+    Fin.pred ⟨i + 1, Nat.add_lt_add_right h 1⟩ (ne_of_val_ne (Nat.ne_of_gt (mk_succ_pos i h))) =
+      ⟨i, h⟩ := by
+  simp only [ext_iff, coe_pred, Nat.add_sub_cancel]
+
+@[simp] theorem pred_mk_succ' (i : Nat) (h₁ : i + 1 < n + 1 + 1) (h₂) :
+    Fin.pred ⟨i + 1, h₁⟩ h₂ = ⟨i, Nat.lt_of_succ_lt_succ h₁⟩ := pred_mk_succ i _
+
+-- This is not a simp theorem by default, because `pred_mk_succ` is nicer when it applies.
+theorem pred_mk {n : Nat} (i : Nat) (h : i < n + 1) (w) : Fin.pred ⟨i, h⟩ w =
+    ⟨i - 1, Nat.sub_lt_right_of_lt_add (Nat.pos_iff_ne_zero.2 (Fin.val_ne_of_ne w)) h⟩ :=
+  rfl
+
+@[simp] theorem pred_le_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
+    a.pred ha ≤ b.pred hb ↔ a ≤ b := by rw [← succ_le_succ_iff, succ_pred, succ_pred]
+
+@[simp] theorem pred_lt_pred_iff {n : Nat} {a b : Fin n.succ} {ha : a ≠ 0} {hb : b ≠ 0} :
+    a.pred ha < b.pred hb ↔ a < b := by rw [← succ_lt_succ_iff, succ_pred, succ_pred]
+
+@[simp] theorem pred_inj :
+    ∀ {a b : Fin (n + 1)} {ha : a ≠ 0} {hb : b ≠ 0}, a.pred ha = b.pred hb ↔ a = b
+  | ⟨0, _⟩, _, ha, _ => by simp only [mk_zero, ne_eq, not_true] at ha
+  | ⟨i + 1, _⟩, ⟨0, _⟩, _, hb => by simp only [mk_zero, ne_eq, not_true] at hb
+  | ⟨i + 1, hi⟩, ⟨j + 1, hj⟩, ha, hb => by simp [ext_iff]
+
+@[simp] theorem pred_one {n : Nat} :
+    Fin.pred (1 : Fin (n + 2)) (Ne.symm (Fin.ne_of_lt one_pos)) = 0 := rfl
+
+theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
+    pred (i + 1) (Fin.ne_of_gt (add_one_pos _ (lt_def.2 h))) = castLT i h := by
+  rw [ext_iff, coe_pred, coe_castLT, val_add, val_one, Nat.mod_eq_of_lt, Nat.add_sub_cancel]
+  exact Nat.add_lt_add_right h 1
+
+@[simp] theorem coe_subNat (i : Fin (n + m)) (h : m ≤ i) : (i.subNat m h : Nat) = i - m := rfl
+
+@[simp] theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
+    subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := rfl
+
+@[simp] theorem pred_castSucc_succ (i : Fin n) :
+    pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := rfl
+
+@[simp] theorem addNat_subNat {i : Fin (n + m)} (h : m ≤ i) : addNat (subNat m i h) m = i :=
+  ext <| Nat.sub_add_cancel h
+
+@[simp] theorem subNat_addNat (i : Fin n) (m : Nat) (h : m ≤ addNat i m := le_coe_addNat m i) :
+    subNat m (addNat i m) h = i := ext <| Nat.add_sub_cancel i m
+
+@[simp] theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
+    natAdd n (subNat n (cast (Nat.add_comm ..) i) h) = i := by simp [← cast_addNat]; rfl
+
+/-! ### recursion and induction principles -/
+
+/-- Define `motive n i` by induction on `i : Fin n` interpreted as `(0 : Fin (n - i)).succ.succ…`.
+This function has two arguments: `zero n` defines `0`-th element `motive (n+1) 0` of an
+`(n+1)`-tuple, and `succ n i` defines `(i+1)`-st element of `(n+1)`-tuple based on `n`, `i`, and
+`i`-th element of `n`-tuple. -/
+-- FIXME: Performance review
+@[elab_as_elim] def succRec {motive : ∀ n, Fin n → Sort _}
+    (zero : ∀ n, motive n.succ (0 : Fin (n + 1)))
+    (succ : ∀ n i, motive n i → motive n.succ i.succ) : ∀ {n : Nat} (i : Fin n), motive n i
+  | 0, i => i.elim0
+  | Nat.succ n, ⟨0, _⟩ => by rw [mk_zero]; exact zero n
+  | Nat.succ _, ⟨Nat.succ i, h⟩ => succ _ _ (succRec zero succ ⟨i, Nat.lt_of_succ_lt_succ h⟩)
+
+/-- Define `motive n i` by induction on `i : Fin n` interpreted as `(0 : Fin (n - i)).succ.succ…`.
+This function has two arguments:
+`zero n` defines the `0`-th element `motive (n+1) 0` of an `(n+1)`-tuple, and
+`succ n i` defines the `(i+1)`-st element of an `(n+1)`-tuple based on `n`, `i`,
+and the `i`-th element of an `n`-tuple.
+
+A version of `Fin.succRec` taking `i : Fin n` as the first argument. -/
+-- FIXME: Performance review
+@[elab_as_elim] def succRecOn {n : Nat} (i : Fin n) {motive : ∀ n, Fin n → Sort _}
+    (zero : ∀ n, motive (n + 1) 0) (succ : ∀ n i, motive n i → motive (Nat.succ n) i.succ) :
+    motive n i := i.succRec zero succ
+
+@[simp] theorem succRecOn_zero {motive : ∀ n, Fin n → Sort _} {zero succ} (n) :
+    @Fin.succRecOn (n + 1) 0 motive zero succ = zero n := by
+  cases n <;> rfl
+
+@[simp] theorem succRecOn_succ {motive : ∀ n, Fin n → Sort _} {zero succ} {n} (i : Fin n) :
+    @Fin.succRecOn (n + 1) i.succ motive zero succ = succ n i (Fin.succRecOn i zero succ) := by
+  cases i; rfl
+
+/-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
+This function has two arguments: `zero` handles the base case on `motive 0`,
+and `succ` defines the inductive step using `motive i.castSucc`.
+-/
+-- FIXME: Performance review
+@[elab_as_elim] def induction {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
+    ∀ i : Fin (n + 1), motive i
+  | ⟨0, hi⟩ => by rwa [Fin.mk_zero]
+  | ⟨i+1, hi⟩ => succ ⟨i, Nat.lt_of_succ_lt_succ hi⟩ (induction zero succ ⟨i, Nat.lt_of_succ_lt hi⟩)
+
+@[simp] theorem induction_zero {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (hs : ∀ i : Fin n, motive (castSucc i) → motive i.succ) :
+    (induction zero hs : ∀ i : Fin (n + 1), motive i) 0 = zero := rfl
+
+@[simp] theorem induction_succ {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) (i : Fin n) :
+    induction (motive := motive) zero succ i.succ = succ i (induction zero succ (castSucc i)) := rfl
+
+/-- Define `motive i` by induction on `i : Fin (n + 1)` via induction on the underlying `Nat` value.
+This function has two arguments: `zero` handles the base case on `motive 0`,
+and `succ` defines the inductive step using `motive i.castSucc`.
+
+A version of `Fin.induction` taking `i : Fin (n + 1)` as the first argument.
+-/
+-- FIXME: Performance review
+@[elab_as_elim] def inductionOn (i : Fin (n + 1)) {motive : Fin (n + 1) → Sort _} (zero : motive 0)
+    (succ : ∀ i : Fin n, motive (castSucc i) → motive i.succ) : motive i := induction zero succ i
+
+/-- Define `f : Π i : Fin n.succ, motive i` by separately handling the cases `i = 0` and
+`i = j.succ`, `j : Fin n`. -/
+@[elab_as_elim] def cases {motive : Fin (n + 1) → Sort _}
+    (zero : motive 0) (succ : ∀ i : Fin n, motive i.succ) :
+    ∀ i : Fin (n + 1), motive i := induction zero fun i _ => succ i
+
+@[simp] theorem cases_zero {n} {motive : Fin (n + 1) → Sort _} {zero succ} :
+    @Fin.cases n motive zero succ 0 = zero := rfl
+
+@[simp] theorem cases_succ {n} {motive : Fin (n + 1) → Sort _} {zero succ} (i : Fin n) :
+    @Fin.cases n motive zero succ i.succ = succ i := rfl
+
+@[simp] theorem cases_succ' {n} {motive : Fin (n + 1) → Sort _} {zero succ}
+    {i : Nat} (h : i + 1 < n + 1) :
+    @Fin.cases n motive zero succ ⟨i.succ, h⟩ = succ ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl
+
+theorem forall_fin_succ {P : Fin (n + 1) → Prop} : (∀ i, P i) ↔ P 0 ∧ ∀ i : Fin n, P i.succ :=
+  ⟨fun H => ⟨H 0, fun _ => H _⟩, fun ⟨H0, H1⟩ i => Fin.cases H0 H1 i⟩
+
+theorem exists_fin_succ {P : Fin (n + 1) → Prop} : (∃ i, P i) ↔ P 0 ∨ ∃ i : Fin n, P i.succ :=
+  ⟨fun ⟨i, h⟩ => Fin.cases Or.inl (fun i hi => Or.inr ⟨i, hi⟩) i h, fun h =>
+    (h.elim fun h => ⟨0, h⟩) fun ⟨i, hi⟩ => ⟨i.succ, hi⟩⟩
+
+theorem forall_fin_one {p : Fin 1 → Prop} : (∀ i, p i) ↔ p 0 :=
+  ⟨fun h => h _, fun h i => Subsingleton.elim i 0 ▸ h⟩
+
+theorem exists_fin_one {p : Fin 1 → Prop} : (∃ i, p i) ↔ p 0 :=
+  ⟨fun ⟨i, h⟩ => Subsingleton.elim i 0 ▸ h, fun h => ⟨_, h⟩⟩
+
+theorem forall_fin_two {p : Fin 2 → Prop} : (∀ i, p i) ↔ p 0 ∧ p 1 :=
+  forall_fin_succ.trans <| and_congr_right fun _ => forall_fin_one
+
+theorem exists_fin_two {p : Fin 2 → Prop} : (∃ i, p i) ↔ p 0 ∨ p 1 :=
+  exists_fin_succ.trans <| or_congr_right exists_fin_one
+
+theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b := by
+  simp only [forall_fin_two]; decide
+
+/--
+Define `motive i` by reverse induction on `i : Fin (n + 1)` via induction on the underlying `Nat`
+value. This function has two arguments: `last` handles the base case on `motive (Fin.last n)`,
+and `cast` defines the inductive step using `motive i.succ`, inducting downwards.
+-/
+@[elab_as_elim] def reverseInduction {motive : Fin (n + 1) → Sort _} (last : motive (Fin.last n))
+    (cast : ∀ i : Fin n, motive i.succ → motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
+  if hi : i = Fin.last n then _root_.cast (congrArg motive hi.symm) last
+  else
+    let j : Fin n := ⟨i, Nat.lt_of_le_of_ne (Nat.le_of_lt_succ i.2) fun h => hi (Fin.ext h)⟩
+    cast _ (reverseInduction last cast j.succ)
+termination_by n + 1 - i
+decreasing_by decreasing_with
+  -- FIXME: we put the proof down here to avoid getting a dummy `have` in the definition
+  exact Nat.add_sub_add_right .. ▸ Nat.sub_lt_sub_left i.2 (Nat.lt_succ_self i)
+
+@[simp] theorem reverseInduction_last {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ} :
+    (reverseInduction zero succ (Fin.last n) : motive (Fin.last n)) = zero := by
+  rw [reverseInduction]; simp; rfl
+
+@[simp] theorem reverseInduction_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {zero succ}
+    (i : Fin n) : reverseInduction (motive := motive) zero succ (castSucc i) =
+      succ i (reverseInduction zero succ i.succ) := by
+  rw [reverseInduction, dif_neg (Fin.ne_of_lt (Fin.castSucc_lt_last i))]; rfl
+
+/-- Define `f : Π i : Fin n.succ, motive i` by separately handling the cases `i = Fin.last n` and
+`i = j.castSucc`, `j : Fin n`. -/
+@[elab_as_elim] def lastCases {n : Nat} {motive : Fin (n + 1) → Sort _} (last : motive (Fin.last n))
+    (cast : ∀ i : Fin n, motive (castSucc i)) (i : Fin (n + 1)) : motive i :=
+  reverseInduction last (fun i _ => cast i) i
+
+@[simp] theorem lastCases_last {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast} :
+    (Fin.lastCases last cast (Fin.last n) : motive (Fin.last n)) = last :=
+  reverseInduction_last ..
+
+@[simp] theorem lastCases_castSucc {n : Nat} {motive : Fin (n + 1) → Sort _} {last cast}
+    (i : Fin n) : (Fin.lastCases last cast (Fin.castSucc i) : motive (Fin.castSucc i)) = cast i :=
+  reverseInduction_castSucc ..
+
+/-- Define `f : Π i : Fin (m + n), motive i` by separately handling the cases `i = castAdd n i`,
+`j : Fin m` and `i = natAdd m j`, `j : Fin n`. -/
+@[elab_as_elim] def addCases {m n : Nat} {motive : Fin (m + n) → Sort u}
+    (left : ∀ i, motive (castAdd n i)) (right : ∀ i, motive (natAdd m i))
+    (i : Fin (m + n)) : motive i :=
+  if hi : (i : Nat) < m then (castAdd_castLT n i hi) ▸ (left (castLT i hi))
+  else (natAdd_subNat_cast (Nat.le_of_not_lt hi)) ▸ (right _)
+
+@[simp] theorem addCases_left {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin m) :
+    addCases (motive := motive) left right (Fin.castAdd n i) = left i := by
+  rw [addCases, dif_pos (castAdd_lt _ _)]; rfl
+
+@[simp]
+theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
+    addCases (motive := motive) left right (natAdd m i) = right i := by
+  have : ¬(natAdd m i : Nat) < m := Nat.not_lt.2 (le_coe_natAdd ..)
+  rw [addCases, dif_neg this]; exact eq_of_heq <| (eqRec_heq _ _).trans (by congr 1; simp)
+
+/-! ### add -/
+
+@[simp] theorem ofNat'_add (x : Nat) (lt : 0 < n) (y : Fin n) :
+    Fin.ofNat' x lt + y = Fin.ofNat' (x + y.val) lt := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.add_def]
+
+@[simp] theorem add_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
+    x + Fin.ofNat' y lt = Fin.ofNat' (x.val + y) lt := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.add_def]
+
+/-! ### sub -/
+
+protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = (a + (n - b)) % n := by
+  cases a; cases b; rfl
+
+@[simp] theorem ofNat'_sub (x : Nat) (lt : 0 < n) (y : Fin n) :
+    Fin.ofNat' x lt - y = Fin.ofNat' (x + (n - y.val)) lt := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.sub_def]
+
+@[simp] theorem sub_ofNat' (x : Fin n) (y : Nat) (lt : 0 < n) :
+    x - Fin.ofNat' y lt = Fin.ofNat' (x.val + (n - y % n)) lt := by
+  apply Fin.eq_of_val_eq
+  simp [Fin.ofNat', Fin.sub_def]
+
+private theorem _root_.Nat.mod_eq_sub_of_lt_two_mul {x n} (h₁ : n ≤ x) (h₂ : x < 2 * n) :
+    x % n = x - n := by
+  rw [Nat.mod_eq, if_pos (by omega), Nat.mod_eq_of_lt (by omega)]
+
+theorem coe_sub_iff_le {a b : Fin n} : (↑(a - b) : Nat) = a - b ↔ b ≤ a := by
+  rw [sub_def, le_def]
+  dsimp only
+  if h : n ≤ a + (n - b) then
+    rw [Nat.mod_eq_sub_of_lt_two_mul h]
+    all_goals omega
+  else
+    rw [Nat.mod_eq_of_lt]
+    all_goals omega
+
+theorem coe_sub_iff_lt {a b : Fin n} : (↑(a - b) : Nat) = n + a - b ↔ a < b := by
+  rw [sub_def, lt_def]
+  dsimp only
+  if h : n ≤ a + (n - b) then
+    rw [Nat.mod_eq_sub_of_lt_two_mul h]
+    all_goals omega
+  else
+    rw [Nat.mod_eq_of_lt]
+    all_goals omega
+
+/-! ### mul -/
+
+theorem val_mul {n : Nat} : ∀ a b : Fin n, (a * b).val = a.val * b.val % n
+  | ⟨_, _⟩, ⟨_, _⟩ => rfl
+
+theorem coe_mul {n : Nat} : ∀ a b : Fin n, ((a * b : Fin n) : Nat) = a * b % n
+  | ⟨_, _⟩, ⟨_, _⟩ => rfl
+
+protected theorem mul_one (k : Fin (n + 1)) : k * 1 = k := by
+  match n with
+  | 0 => exact Subsingleton.elim (α := Fin 1) ..
+  | n+1 => simp [ext_iff, mul_def, Nat.mod_eq_of_lt (is_lt k)]
+
+protected theorem mul_comm (a b : Fin n) : a * b = b * a :=
+  ext <| by rw [mul_def, mul_def, Nat.mul_comm]
+
+protected theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k := by
+  rw [Fin.mul_comm, Fin.mul_one]
+
+protected theorem mul_zero (k : Fin (n + 1)) : k * 0 = 0 := by simp [ext_iff, mul_def]
+
+protected theorem zero_mul (k : Fin (n + 1)) : (0 : Fin (n + 1)) * k = 0 := by
+  simp [ext_iff, mul_def]
+
+end Fin
+
+namespace USize
+
+@[simp] theorem lt_def {a b : USize} : a < b ↔ a.toNat < b.toNat := .rfl
+
+@[simp] theorem le_def {a b : USize} : a ≤ b ↔ a.toNat ≤ b.toNat := .rfl
+
+@[simp] theorem zero_toNat : (0 : USize).toNat = 0 := Nat.zero_mod _
+
+@[simp] theorem mod_toNat (a b : USize) : (a % b).toNat = a.toNat % b.toNat :=
+  Fin.mod_val ..
+
+@[simp] theorem div_toNat (a b : USize) : (a / b).toNat = a.toNat / b.toNat :=
+  Fin.div_val ..
+
+@[simp] theorem modn_toNat (a : USize) (b : Nat) : (a.modn b).toNat = a.toNat % b :=
+  Fin.modn_val ..
+
+theorem mod_lt (a b : USize) (h : 0 < b) : a % b < b := USize.modn_lt _ (by simp at h; exact h)
+
+theorem toNat.inj : ∀ {a b : USize}, a.toNat = b.toNat → a = b
+  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
+
+end USize

src/Init/Data/Int/Bitwise.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro
 -/
 prelude
 import Init.Data.Int.Basic
-import Init.Data.Nat.Bitwise
+import Init.Data.Nat.Bitwise.Basic
 
 namespace Int
 

src/Init/Data/Nat/Bitwise.lean

@@ -1,54 +1,8 @@
 /-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Scott Morrison
 -/
 prelude
-import Init.Data.Nat.Basic
-import Init.Data.Nat.Div
-import Init.Coe
-
-namespace Nat
-
-theorem bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) : n / 2 < n :=
-  Nat.div_lt_self (Nat.zero_lt_of_ne_zero hNe) (Nat.lt_succ_self _)
-
-def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat :=
-  if n = 0 then
-    if f false true then m else 0
-  else if m = 0 then
-    if f true false then n else 0
-  else
-    let n' := n / 2
-    let m' := m / 2
-    let b₁ := n % 2 = 1
-    let b₂ := m % 2 = 1
-    let r  := bitwise f n' m'
-    if f b₁ b₂ then
-      r+r+1
-    else
-      r+r
-decreasing_by apply bitwise_rec_lemma; assumption
-
-@[extern "lean_nat_land"]
-def land : @& Nat → @& Nat → Nat := bitwise and
-@[extern "lean_nat_lor"]
-def lor  : @& Nat → @& Nat → Nat := bitwise or
-@[extern "lean_nat_lxor"]
-def xor  : @& Nat → @& Nat → Nat := bitwise bne
-@[extern "lean_nat_shiftl"]
-def shiftLeft : @& Nat → @& Nat → Nat
-  | n, 0 => n
-  | n, succ m => shiftLeft (2*n) m
-@[extern "lean_nat_shiftr"]
-def shiftRight : @& Nat → @& Nat → Nat
-  | n, 0 => n
-  | n, succ m => shiftRight n m / 2
-
-instance : AndOp Nat := ⟨Nat.land⟩
-instance : OrOp Nat := ⟨Nat.lor⟩
-instance : Xor Nat := ⟨Nat.xor⟩
-instance : ShiftLeft Nat := ⟨Nat.shiftLeft⟩
-instance : ShiftRight Nat := ⟨Nat.shiftRight⟩
-
-end Nat
+import Init.Data.Nat.Bitwise.Basic
+import Init.Data.Nat.Bitwise.Lemmas

src/Init/Data/Nat/Bitwise/Basic.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Data.Nat.Basic
+import Init.Data.Nat.Div
+import Init.Coe
+
+namespace Nat
+
+theorem bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) : n / 2 < n :=
+  Nat.div_lt_self (Nat.zero_lt_of_ne_zero hNe) (Nat.lt_succ_self _)
+
+def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat :=
+  if n = 0 then
+    if f false true then m else 0
+  else if m = 0 then
+    if f true false then n else 0
+  else
+    let n' := n / 2
+    let m' := m / 2
+    let b₁ := n % 2 = 1
+    let b₂ := m % 2 = 1
+    let r  := bitwise f n' m'
+    if f b₁ b₂ then
+      r+r+1
+    else
+      r+r
+decreasing_by apply bitwise_rec_lemma; assumption
+
+@[extern "lean_nat_land"]
+def land : @& Nat → @& Nat → Nat := bitwise and
+@[extern "lean_nat_lor"]
+def lor  : @& Nat → @& Nat → Nat := bitwise or
+@[extern "lean_nat_lxor"]
+def xor  : @& Nat → @& Nat → Nat := bitwise bne
+@[extern "lean_nat_shiftl"]
+def shiftLeft : @& Nat → @& Nat → Nat
+  | n, 0 => n
+  | n, succ m => shiftLeft (2*n) m
+@[extern "lean_nat_shiftr"]
+def shiftRight : @& Nat → @& Nat → Nat
+  | n, 0 => n
+  | n, succ m => shiftRight n m / 2
+
+instance : AndOp Nat := ⟨Nat.land⟩
+instance : OrOp Nat := ⟨Nat.lor⟩
+instance : Xor Nat := ⟨Nat.xor⟩
+instance : ShiftLeft Nat := ⟨Nat.shiftLeft⟩
+instance : ShiftRight Nat := ⟨Nat.shiftRight⟩
+
+/-!
+### testBit
+We define an operation for testing individual bits in the binary representation
+of a number.
+-/
+
+/-- `testBit m n` returns whether the `(n+1)` least significant bit is `1` or `0`-/
+def testBit (m n : Nat) : Bool := (m >>> n) &&& 1 != 0
+
+end Nat

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -0,0 +1,503 @@
+/-
+Copyright (c) 2023 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joe Hendrix
+-/
+
+prelude
+import Init.Data.Bool
+import Init.Data.Nat.Bitwise.Basic
+import Init.Data.Nat.Lemmas
+import Init.TacticsExtra
+import Init.Omega
+
+/-
+This module defines properties of the bitwise operations on Natural numbers.
+
+It is primarily intended to support the bitvector library.
+-/
+
+namespace Nat
+
+@[local simp]
+private theorem one_div_two : 1/2 = 0 := by trivial
+
+private theorem two_pow_succ_sub_succ_div_two : (2 ^ (n+1) - (x + 1)) / 2 = 2^n - (x/2 + 1) := by
+  if h : x + 1 ≤ 2 ^ (n + 1) then
+    apply fun x => (Nat.sub_eq_of_eq_add x).symm
+    apply Eq.trans _
+    apply Nat.add_mul_div_left _ _ Nat.zero_lt_two
+    rw [← Nat.sub_add_comm h]
+    rw [Nat.add_sub_assoc (by omega)]
+    rw [Nat.pow_succ']
+    rw [Nat.mul_add_div Nat.zero_lt_two]
+    simp [show (2 * (x / 2 + 1) - (x + 1)) / 2 = 0 by omega]
+  else
+    rw [Nat.pow_succ'] at *
+    omega
+
+private theorem two_pow_succ_sub_one_div_two : (2 ^ (n+1) - 1) / 2 = 2^n - 1 :=
+  two_pow_succ_sub_succ_div_two
+
+private theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1 := by
+  match n with
+  | 0 => contradiction
+  | n + 1 => simp [Nat.mul_succ, Nat.mul_add_mod, mod_eq_of_lt]
+
+/-! ### Preliminaries -/
+
+/--
+An induction principal that works on divison by two.
+-/
+noncomputable def div2Induction {motive : Nat → Sort u}
+    (n : Nat) (ind : ∀(n : Nat), (n > 0 → motive (n/2)) → motive n) : motive n := by
+  induction n using Nat.strongInductionOn with
+  | ind n hyp =>
+    apply ind
+    intro n_pos
+    if n_eq : n = 0 then
+      simp [n_eq] at n_pos
+    else
+      apply hyp
+      exact Nat.div_lt_self n_pos (Nat.le_refl _)
+
+@[simp] theorem zero_and (x : Nat) : 0 &&& x = 0 := by rfl
+
+@[simp] theorem and_zero (x : Nat) : x &&& 0 = 0 := by
+  simp only [HAnd.hAnd, AndOp.and, land]
+  unfold bitwise
+  simp
+
+@[simp] theorem and_one_is_mod (x : Nat) : x &&& 1 = x % 2 := by
+  if xz : x = 0 then
+    simp [xz, zero_and]
+  else
+    have andz := and_zero (x/2)
+    simp only [HAnd.hAnd, AndOp.and, land] at andz
+    simp only [HAnd.hAnd, AndOp.and, land]
+    unfold bitwise
+    cases mod_two_eq_zero_or_one x with | _ p =>
+      simp [xz, p, andz, one_div_two, mod_eq_of_lt]
+
+/-! ### testBit -/
+
+@[simp] theorem zero_testBit (i : Nat) : testBit 0 i = false := by
+  simp only [testBit, zero_shiftRight, zero_and, bne_self_eq_false]
+
+@[simp] theorem testBit_zero (x : Nat) : testBit x 0 = decide (x % 2 = 1) := by
+  cases mod_two_eq_zero_or_one x with | _ p => simp [testBit, p]
+
+@[simp] theorem testBit_succ (x i : Nat) : testBit x (succ i) = testBit (x/2) i := by
+  unfold testBit
+  simp [shiftRight_succ_inside]
+
+theorem testBit_to_div_mod {x : Nat} : testBit x i = decide (x / 2^i % 2 = 1) := by
+  induction i generalizing x with
+  | zero =>
+    unfold testBit
+    cases mod_two_eq_zero_or_one x with | _ xz => simp [xz]
+  | succ i hyp =>
+    simp [hyp, Nat.div_div_eq_div_mul, Nat.pow_succ']
+
+theorem ne_zero_implies_bit_true {x : Nat} (xnz : x ≠ 0) : ∃ i, testBit x i := by
+  induction x using div2Induction with
+  | ind x hyp =>
+    have x_pos : x > 0 := Nat.pos_of_ne_zero xnz
+    match mod_two_eq_zero_or_one x with
+    | Or.inl mod2_eq =>
+      rw [←div_add_mod x 2] at xnz
+      simp only [mod2_eq, ne_eq, Nat.mul_eq_zero, Nat.add_zero, false_or] at xnz
+      have ⟨d, dif⟩   := hyp x_pos xnz
+      apply Exists.intro (d+1)
+      simp_all
+    | Or.inr mod2_eq =>
+      apply Exists.intro 0
+      simp_all
+
+theorem ne_implies_bit_diff {x y : Nat} (p : x ≠ y) : ∃ i, testBit x i ≠ testBit y i := by
+  induction y using Nat.div2Induction generalizing x with
+  | ind y hyp =>
+    cases Nat.eq_zero_or_pos y with
+    | inl yz =>
+      simp only [yz, Nat.zero_testBit, Bool.eq_false_iff]
+      simp only [yz] at p
+      have ⟨i,ip⟩  := ne_zero_implies_bit_true p
+      apply Exists.intro i
+      simp [ip]
+    | inr ypos =>
+      if lsb_diff : x % 2 = y % 2 then
+        rw [←Nat.div_add_mod x 2, ←Nat.div_add_mod y 2] at p
+        simp only [ne_eq, lsb_diff, Nat.add_right_cancel_iff,
+          Nat.zero_lt_succ, Nat.mul_left_cancel_iff] at p
+        have ⟨i, ieq⟩  := hyp ypos p
+        apply Exists.intro (i+1)
+        simpa
+      else
+        apply Exists.intro 0
+        simp only [testBit_zero]
+        revert lsb_diff
+        cases mod_two_eq_zero_or_one x with | _ p =>
+          cases mod_two_eq_zero_or_one y with | _ q =>
+            simp [p,q]
+
+/--
+`eq_of_testBit_eq` allows proving two natural numbers are equal
+if their bits are all equal.
+-/
+theorem eq_of_testBit_eq {x y : Nat} (pred : ∀i, testBit x i = testBit y i) : x = y := by
+  if h : x = y then
+    exact h
+  else
+    let ⟨i,eq⟩ := ne_implies_bit_diff h
+    have p := pred i
+    contradiction
+
+theorem ge_two_pow_implies_high_bit_true {x : Nat} (p : x ≥ 2^n) : ∃ i, i ≥ n ∧ testBit x i := by
+  induction x using div2Induction generalizing n with
+  | ind x hyp =>
+    have x_pos : x > 0 := Nat.lt_of_lt_of_le (Nat.two_pow_pos n) p
+    have x_ne_zero : x ≠ 0 := Nat.ne_of_gt x_pos
+    match n with
+    | zero =>
+      let ⟨j, jp⟩ := ne_zero_implies_bit_true x_ne_zero
+      exact Exists.intro j (And.intro (Nat.zero_le _) jp)
+    | succ n =>
+      have x_ge_n : x / 2 ≥ 2 ^ n := by
+          simpa [le_div_iff_mul_le, ← Nat.pow_succ'] using p
+      have ⟨j, jp⟩ := @hyp x_pos n x_ge_n
+      apply Exists.intro (j+1)
+      apply And.intro
+      case left =>
+        exact (Nat.succ_le_succ jp.left)
+      case right =>
+        simpa using jp.right
+
+theorem testBit_implies_ge {x : Nat} (p : testBit x i = true) : x ≥ 2^i := by
+  simp only [testBit_to_div_mod] at p
+  apply Decidable.by_contra
+  intro not_ge
+  have x_lt : x < 2^i := Nat.lt_of_not_le not_ge
+  simp [div_eq_of_lt x_lt] at p
+
+theorem testBit_lt_two_pow {x i : Nat} (lt : x < 2^i) : x.testBit i = false := by
+  match p : x.testBit i with
+  | false => trivial
+  | true =>
+    exfalso
+    exact Nat.not_le_of_gt lt (testBit_implies_ge p)
+
+theorem lt_pow_two_of_testBit (x : Nat) (p : ∀i, i ≥ n → testBit x i = false) : x < 2^n := by
+  apply Decidable.by_contra
+  intro not_lt
+  have x_ge_n := Nat.ge_of_not_lt not_lt
+  have ⟨i, ⟨i_ge_n, test_true⟩⟩ := ge_two_pow_implies_high_bit_true x_ge_n
+  have test_false := p _ i_ge_n
+  simp only [test_true] at test_false
+
+/-! ### testBit -/
+
+private theorem succ_mod_two : succ x % 2 = 1 - x % 2 := by
+  induction x with
+  | zero =>
+    trivial
+  | succ x hyp =>
+    have p : 2 ≤ x + 2 := Nat.le_add_left _ _
+    simp [Nat.mod_eq (x+2) 2, p, hyp]
+    cases Nat.mod_two_eq_zero_or_one x with | _ p => simp [p]
+
+private theorem testBit_succ_zero : testBit (x + 1) 0 = not (testBit x 0) := by
+  simp [testBit_to_div_mod, succ_mod_two]
+  cases Nat.mod_two_eq_zero_or_one x with | _ p =>
+    simp [p]
+
+theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = not (testBit x i) := by
+  simp [testBit_to_div_mod, add_div_left, Nat.two_pow_pos, succ_mod_two]
+  cases mod_two_eq_zero_or_one (x / 2 ^ i) with
+  | _ p => simp [p]
+
+theorem testBit_mul_two_pow_add_eq (a b i : Nat) :
+    testBit (2^i*a + b) i = Bool.xor (a%2 = 1) (testBit b i) := by
+  match a with
+  | 0 => simp
+  | a+1 =>
+    simp [Nat.mul_succ, Nat.add_assoc,
+          testBit_mul_two_pow_add_eq a,
+          testBit_two_pow_add_eq,
+          Nat.succ_mod_two]
+    cases mod_two_eq_zero_or_one a with
+    | _ p => simp [p]
+
+theorem testBit_two_pow_add_gt {i j : Nat} (j_lt_i : j < i) (x : Nat) :
+    testBit (2^i + x) j = testBit x j := by
+  have i_def : i = j + (i-j) := (Nat.add_sub_cancel' (Nat.le_of_lt j_lt_i)).symm
+  rw [i_def]
+  simp only [testBit_to_div_mod, Nat.pow_add,
+        Nat.add_comm x, Nat.mul_add_div (Nat.two_pow_pos _)]
+  match i_sub_j_eq : i - j with
+  | 0 =>
+    exfalso
+    rw [Nat.sub_eq_zero_iff_le] at i_sub_j_eq
+    exact Nat.not_le_of_gt j_lt_i i_sub_j_eq
+  | d+1 =>
+    simp [pow_succ, Nat.mul_comm _ 2,  Nat.mul_add_mod]
+
+@[simp] theorem testBit_mod_two_pow (x j i : Nat) :
+    testBit (x % 2^j) i = (decide (i < j) && testBit x i) := by
+  induction x using Nat.strongInductionOn generalizing j i with
+  | ind x hyp =>
+    rw [mod_eq]
+    rcases Nat.lt_or_ge x (2^j) with x_lt_j | x_ge_j
+    · have not_j_le_x := Nat.not_le_of_gt x_lt_j
+      simp [not_j_le_x]
+      rcases Nat.lt_or_ge i j with i_lt_j | i_ge_j
+      · simp [i_lt_j]
+      · have x_lt : x < 2^i :=
+            calc x < 2^j := x_lt_j
+                _ ≤ 2^i := Nat.pow_le_pow_of_le_right Nat.zero_lt_two i_ge_j
+        simp [Nat.testBit_lt_two_pow x_lt]
+    · generalize y_eq : x - 2^j = y
+      have x_eq : x = y + 2^j := Nat.eq_add_of_sub_eq x_ge_j y_eq
+      simp only [Nat.two_pow_pos, x_eq, Nat.le_add_left, true_and, ite_true]
+      have y_lt_x : y < x := by
+            simp [x_eq]
+            exact Nat.lt_add_of_pos_right (Nat.two_pow_pos j)
+      simp only [hyp y y_lt_x]
+      if i_lt_j : i < j then
+        rw [ Nat.add_comm _ (2^_), testBit_two_pow_add_gt i_lt_j]
+      else
+        simp [i_lt_j]
+
+theorem testBit_one_zero : testBit 1 0 = true := by trivial
+
+theorem testBit_two_pow_sub_succ (h₂ : x < 2 ^ n) (i : Nat) :
+    testBit (2^n - (x + 1)) i = (decide (i < n) && ! testBit x i) := by
+  induction i generalizing n x with
+  | zero =>
+    simp only [testBit_zero, zero_eq, Bool.and_eq_true, decide_eq_true_eq,
+      Bool.not_eq_true']
+    match n with
+    | 0 => simp
+    | n+1 =>
+      -- just logic + omega:
+      simp only [zero_lt_succ, decide_True, Bool.true_and]
+      rw [Nat.pow_succ', ← decide_not, decide_eq_decide]
+      rw [Nat.pow_succ'] at h₂
+      omega
+  | succ i ih =>
+    simp only [testBit_succ]
+    match n with
+    | 0 =>
+      simp only [pow_zero, succ_sub_succ_eq_sub, Nat.zero_sub, Nat.zero_div, zero_testBit]
+      rw [decide_eq_false] <;> simp
+    | n+1 =>
+      rw [Nat.two_pow_succ_sub_succ_div_two, ih]
+      · simp [Nat.succ_lt_succ_iff]
+      · rw [Nat.pow_succ'] at h₂
+        omega
+
+@[simp] theorem testBit_two_pow_sub_one (n i : Nat) : testBit (2^n-1) i = decide (i < n) := by
+  rw [testBit_two_pow_sub_succ]
+  · simp
+  · exact Nat.two_pow_pos _
+
+theorem testBit_bool_to_nat (b : Bool) (i : Nat) :
+    testBit (Bool.toNat b) i = (decide (i = 0) && b) := by
+  cases b <;> cases i <;>
+  simp [testBit_to_div_mod, Nat.pow_succ, Nat.mul_comm _ 2,
+        ←Nat.div_div_eq_div_mul _ 2, one_div_two,
+        Nat.mod_eq_of_lt]
+
+/-! ### bitwise -/
+
+theorem testBit_bitwise
+  (false_false_axiom : f false false = false) (x y i : Nat)
+: (bitwise f x y).testBit i = f (x.testBit i) (y.testBit i) := by
+  induction i using Nat.strongInductionOn generalizing x y with
+  | ind i hyp =>
+    unfold bitwise
+    if x_zero : x = 0 then
+      cases p : f false true <;>
+        cases yi : testBit y i <;>
+          simp [x_zero, p, yi, false_false_axiom]
+    else if y_zero : y = 0 then
+      simp [x_zero, y_zero]
+      cases p : f true false <;>
+        cases xi : testBit x i <;>
+          simp [p, xi, false_false_axiom]
+    else
+      simp only [x_zero, y_zero, ←Nat.two_mul]
+      cases i with
+      | zero =>
+        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
+          simp [p, Nat.mul_add_mod, mod_eq_of_lt]
+      | succ i =>
+        have hyp_i := hyp i (Nat.le_refl (i+1))
+        cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) <;>
+          simp [p, one_div_two, hyp_i, Nat.mul_add_div]
+
+/-! ### bitwise -/
+
+@[local simp]
+private theorem eq_0_of_lt_one (x : Nat) : x < 1 ↔ x = 0 :=
+  Iff.intro
+    (fun p =>
+      match x with
+      | 0 => Eq.refl 0
+      | _+1 => False.elim (not_lt_zero _ (Nat.lt_of_succ_lt_succ p)))
+    (fun p => by simp [p, Nat.zero_lt_succ])
+
+private theorem eq_0_of_lt (x : Nat) : x < 2^ 0 ↔ x = 0 := eq_0_of_lt_one x
+
+@[local simp]
+private theorem zero_lt_pow (n : Nat) : 0 < 2^n := by
+  induction n
+  case zero => simp [eq_0_of_lt]
+  case succ n hyp => simpa [pow_succ]
+
+private theorem div_two_le_of_lt_two {m n : Nat} (p : m < 2 ^ succ n) : m / 2 < 2^n := by
+  simp [div_lt_iff_lt_mul Nat.zero_lt_two]
+  exact p
+
+/-- This provides a bound on bitwise operations. -/
+theorem bitwise_lt_two_pow (left : x < 2^n) (right : y < 2^n) : (Nat.bitwise f x y) < 2^n := by
+  induction n generalizing x y with
+  | zero =>
+    simp only [eq_0_of_lt] at left right
+    unfold bitwise
+    simp [left, right]
+  | succ n hyp =>
+    unfold bitwise
+    if x_zero : x = 0 then
+      simp only [x_zero, if_pos]
+      by_cases p : f false true = true <;> simp [p, right]
+    else if y_zero : y = 0 then
+      simp only [x_zero, y_zero, if_neg, if_pos]
+      by_cases p : f true false = true <;> simp [p, left]
+    else
+      simp only [x_zero, y_zero, if_neg]
+      have hyp1 := hyp (div_two_le_of_lt_two left) (div_two_le_of_lt_two right)
+      by_cases p : f (decide (x % 2 = 1)) (decide (y % 2 = 1)) = true <;>
+        simp [p, pow_succ, mul_succ, Nat.add_assoc]
+      case pos =>
+        apply lt_of_succ_le
+        simp only [← Nat.succ_add]
+        apply Nat.add_le_add <;> exact hyp1
+      case neg =>
+        apply Nat.add_lt_add <;> exact hyp1
+
+/-! ### and -/
+
+@[simp] theorem testBit_and (x y i : Nat) : (x &&& y).testBit i = (x.testBit i && y.testBit i) := by
+  simp [HAnd.hAnd, AndOp.and, land, testBit_bitwise ]
+
+theorem and_lt_two_pow (x : Nat) {y n : Nat} (right : y < 2^n) : (x &&& y) < 2^n := by
+  apply lt_pow_two_of_testBit
+  intro i i_ge_n
+  have yf : testBit y i = false := by
+          apply Nat.testBit_lt_two_pow
+          apply Nat.lt_of_lt_of_le right
+          exact pow_le_pow_of_le_right Nat.zero_lt_two i_ge_n
+  simp [testBit_and, yf]
+
+@[simp] theorem and_pow_two_is_mod (x n : Nat) : x &&& (2^n-1) = x % 2^n := by
+  apply eq_of_testBit_eq
+  intro i
+  simp only [testBit_and, testBit_mod_two_pow]
+  cases testBit x i <;> simp
+
+theorem and_pow_two_identity {x : Nat} (lt : x < 2^n) : x &&& 2^n-1 = x := by
+  rw [and_pow_two_is_mod]
+  apply Nat.mod_eq_of_lt lt
+
+/-! ### lor -/
+
+@[simp] theorem or_zero (x : Nat) : 0 ||| x = x := by
+  simp only [HOr.hOr, OrOp.or, lor]
+  unfold bitwise
+  simp [@eq_comm _ 0]
+
+@[simp] theorem zero_or (x : Nat) : x ||| 0 = x := by
+  simp only [HOr.hOr, OrOp.or, lor]
+  unfold bitwise
+  simp [@eq_comm _ 0]
+
+@[simp] theorem testBit_or (x y i : Nat) : (x ||| y).testBit i = (x.testBit i || y.testBit i) := by
+  simp [HOr.hOr, OrOp.or, lor, testBit_bitwise ]
+
+theorem or_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ||| y < 2^n :=
+  bitwise_lt_two_pow left right
+
+/-! ### xor -/
+
+@[simp] theorem testBit_xor (x y i : Nat) :
+    (x ^^^ y).testBit i = Bool.xor (x.testBit i) (y.testBit i) := by
+  simp [HXor.hXor, Xor.xor, xor, testBit_bitwise ]
+
+theorem xor_lt_two_pow {x y n : Nat} (left : x < 2^n) (right : y < 2^n) : x ^^^ y < 2^n :=
+  bitwise_lt_two_pow left right
+
+/-! ### Arithmetic -/
+
+theorem testBit_mul_pow_two_add (a : Nat) {b i : Nat} (b_lt : b < 2^i) (j : Nat) :
+    testBit (2 ^ i * a + b) j =
+      if j < i then
+        testBit b j
+      else
+        testBit a (j - i) := by
+  cases Nat.lt_or_ge j i with
+  | inl j_lt =>
+    simp only [j_lt]
+    have i_ge := Nat.le_of_lt j_lt
+    have i_sub_j_nez : i-j ≠ 0 := Nat.sub_ne_zero_of_lt j_lt
+    have i_def : i = j + succ (pred (i-j)) :=
+          calc i = j + (i-j) := (Nat.add_sub_cancel' i_ge).symm
+               _ = j + succ (pred (i-j)) := by
+                 rw [← congrArg (j+·) (Nat.succ_pred i_sub_j_nez)]
+    rw [i_def]
+    simp only [testBit_to_div_mod, Nat.pow_add, Nat.mul_assoc]
+    simp only [Nat.mul_add_div (Nat.two_pow_pos _), Nat.mul_add_mod]
+    simp [Nat.pow_succ, Nat.mul_comm _ 2, Nat.mul_assoc, Nat.mul_add_mod]
+  | inr j_ge =>
+    have j_def : j = i + (j-i) := (Nat.add_sub_cancel' j_ge).symm
+    simp only [
+        testBit_to_div_mod,
+        Nat.not_lt_of_le,
+        j_ge,
+        ite_false]
+    simp [congrArg (2^·) j_def, Nat.pow_add,
+          ←Nat.div_div_eq_div_mul,
+          Nat.mul_add_div,
+          Nat.div_eq_of_lt b_lt,
+          Nat.two_pow_pos i]
+
+theorem testBit_mul_pow_two :
+    testBit (2 ^ i * a) j = (decide (j ≥ i) && testBit a (j-i)) := by
+  have gen := testBit_mul_pow_two_add a (Nat.two_pow_pos i) j
+  simp at gen
+  rw [gen]
+  cases Nat.lt_or_ge j i with
+  | _ p => simp [p, Nat.not_le_of_lt, Nat.not_lt_of_le]
+
+theorem mul_add_lt_is_or {b : Nat} (b_lt : b < 2^i) (a : Nat) : 2^i * a + b = 2^i * a ||| b := by
+  apply eq_of_testBit_eq
+  intro j
+  simp only [testBit_mul_pow_two_add _ b_lt,
+        testBit_or, testBit_mul_pow_two]
+  if j_lt : j < i then
+    simp [Nat.not_le_of_lt, j_lt]
+  else
+    have i_le : i ≤ j := Nat.le_of_not_lt j_lt
+    have b_lt_j :=
+            calc b < 2 ^ i := b_lt
+                 _ ≤ 2 ^ j := Nat.pow_le_pow_of_le_right Nat.zero_lt_two i_le
+    simp [i_le, j_lt, testBit_lt_two_pow, b_lt_j]
+
+/-! ### shiftLeft and shiftRight -/
+
+@[simp] theorem testBit_shiftLeft (x : Nat) : testBit (x <<< i) j =
+    (decide (j ≥ i) && testBit x (j-i)) := by
+  simp [shiftLeft_eq, Nat.mul_comm _ (2^_), testBit_mul_pow_two]
+
+@[simp] theorem testBit_shiftRight (x : Nat) : testBit (x >>> i) j = testBit x (i+j) := by
+  simp [testBit, ←shiftRight_add]

src/Init/Data/Nat/Dvd.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+-/
 prelude
 import Init.Data.Nat.Div
 
@@ -85,7 +90,6 @@ theorem emod_pos_of_not_dvd {a b : Nat} (h : ¬ a ∣ b) : 0 < b % a := by
   rw [dvd_iff_mod_eq_zero] at h
   exact Nat.pos_of_ne_zero h
 
-
 protected theorem mul_div_cancel' {n m : Nat} (H : n ∣ m) : n * (m / n) = m := by
   have := mod_add_div m n
   rwa [mod_eq_zero_of_dvd H, Nat.zero_add] at this

src/Init/Data/Nat/Lemmas.lean

@@ -996,11 +996,11 @@ theorem shiftRight_succ_inside : ∀m n, m >>> (n+1) = (m/2) >>> n
 
 @[simp] theorem zero_shiftLeft : ∀ n, 0 <<< n = 0
   | 0 => by simp [shiftLeft]
-  | n + 1 => by simp [shiftLeft, zero_shiftLeft, shiftLeft_succ]
+  | n + 1 => by simp [shiftLeft, zero_shiftLeft n, shiftLeft_succ]
 
 @[simp] theorem zero_shiftRight : ∀ n, 0 >>> n = 0
   | 0 => by simp [shiftRight]
-  | n + 1 => by simp [shiftRight, zero_shiftRight, shiftRight_succ]
+  | n + 1 => by simp [shiftRight, zero_shiftRight n, shiftRight_succ]
 
 theorem shiftRight_add (m n : Nat) : ∀ k, m >>> (n + k) = (m >>> n) >>> k
   | 0 => rfl
@@ -1020,11 +1020,8 @@ theorem mul_add_div {m : Nat} (m_pos : m > 0) (x y : Nat) : (m * x + y) / m = x
   match x with
   | 0 => simp
   | x + 1 =>
-    simp [Nat.mul_succ, Nat.add_assoc _ m,
-          mul_add_div m_pos x (m+y),
-          div_eq (m+y) m,
-          m_pos,
-          Nat.le_add_right m, Nat.add_succ, Nat.succ_add]
+    rw [Nat.mul_succ, Nat.add_assoc _ m, mul_add_div m_pos x (m+y), div_eq]
+    simp_arith [m_pos]; rw [Nat.add_comm, Nat.add_sub_cancel]
 
 theorem mul_add_mod (m x y : Nat) : (m * x + y) % m = y % m := by
   match x with

src/Init/Data/Nat/MinMax.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
+-/
 prelude
 import Init.ByCases
 

src/Init/Notation.lean

@@ -484,6 +484,9 @@ instance : Coe Syntax (TSyntax `rawStx) where
 /-- `with_annotate_term stx e` annotates the lexical range of `stx : Syntax` with term info for `e`. -/
 scoped syntax (name := withAnnotateTerm) "with_annotate_term " rawStx ppSpace term : term
 
+/-- Normalize casts in an expression using the same method as the `norm_cast` tactic. -/
+syntax (name := modCast) "mod_cast " term : term
+
 /--
 The attribute `@[deprecated]` on a declaration indicates that the declaration
 is discouraged for use in new code, and/or should be migrated away from in

src/Init/NotationExtra.lean

@@ -460,3 +460,9 @@ macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
   `(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))
 
 end Lean
+
+syntax "{" term,+ "}" : term
+
+macro_rules
+  | `({$x:term}) => `(singleton $x)
+  | `({$x:term, $xs:term,*}) => `(insert $x {$xs:term,*})

src/Init/Omega.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
 prelude
 import Init.Omega.Int
 import Init.Omega.IntList

src/Init/Prelude.lean

@@ -1814,6 +1814,8 @@ structure Fin (n : Nat) where
   /-- If `i : Fin n`, then `i.2` is a proof that `i.1 < n`. -/
   isLt : LT.lt val n
 
+attribute [coe] Fin.val
+
 theorem Fin.eq_of_val_eq {n} : ∀ {i j : Fin n}, Eq i.val j.val → Eq i j
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 

src/Init/Tactics.lean

@@ -1018,7 +1018,6 @@ macro "haveI" d:haveDecl : tactic => `(tactic| refine_lift haveI $d:haveDecl; ?_
 /-- `letI` behaves like `let`, but inlines the value instead of producing a `let_fun` term. -/
 macro "letI" d:haveDecl : tactic => `(tactic| refine_lift letI $d:haveDecl; ?_)
 
-
 /--
 The `omega` tactic, for resolving integer and natural linear arithmetic problems.
 
@@ -1052,6 +1051,74 @@ Currently, all of these are on by default.
 -/
 syntax (name := omega) "omega" (config)? : tactic
 
+/-- Implementation of `norm_cast` (the full `norm_cast` calls `trivial` afterwards). -/
+syntax (name := normCast0) "norm_cast0" (location)? : tactic
+
+/-- `assumption_mod_cast` is a variant of `assumption` that solves the goal
+using a hypothesis. Unlike `assumption`, it first pre-processes the goal and
+each hypothesis to move casts as far outwards as possible, so it can be used
+in more situations.
+
+Concretely, it runs `norm_cast` on the goal. For each local hypothesis `h`, it also
+normalizes `h` with `norm_cast` and tries to use that to close the goal. -/
+macro "assumption_mod_cast" : tactic => `(tactic| norm_cast0 at * <;> assumption)
+
+/--
+The `norm_cast` family of tactics is used to normalize casts inside expressions.
+It is basically a `simp` tactic with a specific set of lemmas to move casts
+upwards in the expression.
+Therefore even in situations where non-terminal `simp` calls are discouraged (because of fragility),
+`norm_cast` is considered safe.
+It also has special handling of numerals.
+
+For instance, given an assumption
+```lean
+a b : ℤ
+h : ↑a + ↑b < (10 : ℚ)
+```
+
+writing `norm_cast at h` will turn `h` into
+```lean
+h : a + b < 10
+```
+
+There are also variants of `exact`, `apply`, `rw`, and `assumption` that
+work modulo `norm_cast` - in other words, they apply `norm_cast` to make
+them more flexible. They are called `exact_mod_cast`, `apply_mod_cast`,
+`rw_mod_cast`, and `assumption_mod_cast`, respectively.
+Writing `exact_mod_cast h` and `apply_mod_cast h` will normalize casts
+in the goal and `h` before using `exact h` or `apply h`.
+Writing `assumption_mod_cast` will normalize casts in the goal and, for
+every hypothesis `h` in the context, it will try to normalize casts in `h` and use
+`exact h`.
+`rw_mod_cast` acts like the `rw` tactic but it applies `norm_cast` between steps.
+
+See also `push_cast`, which moves casts inwards rather than lifting them outwards.
+-/
+macro "norm_cast" loc:(location)? : tactic =>
+  `(tactic| norm_cast0 $[$loc]? <;> try trivial)
+
+/--
+`push_cast` rewrites the goal to move casts inward, toward the leaf nodes.
+This uses `norm_cast` lemmas in the forward direction.
+For example, `↑(a + b)` will be written to `↑a + ↑b`.
+It is equivalent to `simp only with push_cast`.
+It can also be used at hypotheses with `push_cast at h`
+and with extra simp lemmas with `push_cast [int.add_zero]`.
+
+```lean
+example (a b : ℕ) (h1 : ((a + b : ℕ) : ℤ) = 10) (h2 : ((a + b + 0 : ℕ) : ℤ) = 10) :
+  ((a + b : ℕ) : ℤ) = 10 :=
+begin
+  push_cast,
+  push_cast at h1,
+  push_cast [int.add_zero] at h2,
+end
+```
+-/
+syntax (name := pushCast) "push_cast" (config)? (discharger)? (&" only")?
+  (" [" (simpStar <|> simpErase <|> simpLemma),* "]")? (location)? : tactic
+
 end Tactic
 
 namespace Attr
@@ -1099,6 +1166,59 @@ If there are several with the same priority, it is uses the "most recent one". E
 ```
 -/
 syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (ppSpace prio)? : attr
+
+
+/-- The possible `norm_cast` kinds: `elim`, `move`, or `squash`. -/
+syntax normCastLabel := &"elim" <|> &"move" <|> &"squash"
+
+/--
+The `norm_cast` attribute should be given to lemmas that describe the
+behaviour of a coercion with respect to an operator, a relation, or a particular
+function.
+
+It only concerns equality or iff lemmas involving `↑`, `⇑` and `↥`, describing the behavior of
+the coercion functions.
+It does not apply to the explicit functions that define the coercions.
+
+Examples:
+```lean
+@[norm_cast] theorem coe_nat_inj' {m n : ℕ} : (↑m : ℤ) = ↑n ↔ m = n
+
+@[norm_cast] theorem coe_int_denom (n : ℤ) : (n : ℚ).denom = 1
+
+@[norm_cast] theorem cast_id : ∀ n : ℚ, ↑n = n
+
+@[norm_cast] theorem coe_nat_add (m n : ℕ) : (↑(m + n) : ℤ) = ↑m + ↑n
+
+@[norm_cast] theorem cast_coe_nat (n : ℕ) : ((n : ℤ) : α) = n
+
+@[norm_cast] theorem cast_one : ((1 : ℚ) : α) = 1
+```
+
+Lemmas tagged with `@[norm_cast]` are classified into three categories: `move`, `elim`, and
+`squash`. They are classified roughly as follows:
+
+* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
+* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
+* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
+
+`norm_cast` uses `move` and `elim` lemmas to factor coercions toward the root of an expression
+and to cancel them from both sides of an equation or relation. It uses `squash` lemmas to clean
+up the result.
+
+It is typically not necessary to specify these categories, as `norm_cast` lemmas are
+automatically classified by default. The automatic classification can be overridden by
+giving an optional `elim`, `move`, or `squash` parameter to the attribute.
+
+```lean
+@[simp, norm_cast elim] lemma nat_cast_re (n : ℕ) : (n : ℂ).re = n := by
+  rw [← of_real_nat_cast, of_real_re]
+```
+
+Don't do this unless you understand what you are doing.
+-/
+syntax (name := norm_cast) "norm_cast" (ppSpace normCastLabel)? (ppSpace num)? : attr
+
 end Attr
 
 end Parser

src/Init/TacticsExtra.lean

@@ -63,4 +63,24 @@ macro_rules
     | 0 => `(tactic| skip)
     | n+1 => `(tactic| ($seq:tacticSeq); iterate $(quote n) $seq:tacticSeq)
 
+/--
+Rewrites with the given rules, normalizing casts prior to each step.
+-/
+syntax "rw_mod_cast" (config)? rwRuleSeq (location)? : tactic
+macro_rules
+  | `(tactic| rw_mod_cast $[$config]? [$rules,*] $[$loc]?) => do
+    let tacs ← rules.getElems.mapM fun rule =>
+      `(tactic| (norm_cast at *; rw $[$config]? [$rule] $[$loc]?))
+    `(tactic| ($[$tacs]*))
+
+/--
+Normalize casts in the goal and the given expression, then close the goal with `exact`.
+-/
+macro "exact_mod_cast " e:term : tactic => `(tactic| exact mod_cast ($e : _))
+
+/--
+Normalize casts in the goal and the given expression, then `apply` the expression to the goal.
+-/
+macro "apply_mod_cast " e:term : tactic => `(tactic| apply mod_cast ($e : _))
+
 end Lean.Parser.Tactic

src/Lean/Data/Json/Elab.lean

@@ -1,7 +1,7 @@
 /-
- Copyright (c) 2022 E.W.Ayers. All rights reserved.
- Released under Apache 2.0 license as described in the file LICENSE.
- Authors: E.W.Ayers, Wojciech Nawrocki
+Copyright (c) 2022 E.W.Ayers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: E.W.Ayers, Wojciech Nawrocki
 -/
 prelude
 import Lean.Data.Json.FromToJson

src/Lean/Data/Xml.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2021 Daniel Fabian. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Daniel Fabian
+-/
 prelude
 import Lean.Data.Xml.Basic
 import Lean.Data.Xml.Parser

src/Lean/Data/Xml/Basic.lean

@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -38,4 +37,3 @@ private partial def cToString : Content → String
 end
 instance : ToString Element := ⟨eToString⟩
 instance : ToString Content := ⟨cToString⟩
-

src/Lean/Elab/MutualDef.lean

@@ -214,7 +214,7 @@ private def expandWhereStructInst : Macro
         `(structInstField|$id:ident := $val)
       | stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here"
       | _ => Macro.throwUnsupported
-    let body ← `({ $structInstFields,* })
+    let body ← `(structInst| { $structInstFields,* })
     match whereDecls? with
     | some whereDecls => expandWhereDecls whereDecls body
     | none => return body

src/Lean/Elab/Tactic.lean

@@ -32,3 +32,4 @@ import Lean.Elab.Tactic.Change
 import Lean.Elab.Tactic.FalseOrByContra
 import Lean.Elab.Tactic.Omega
 import Lean.Elab.Tactic.Simpa
+import Lean.Elab.Tactic.NormCast

src/Lean/Elab/Tactic/NormCast.lean

@@ -0,0 +1,265 @@
+/-
+Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
+-/
+import Lean.Meta.Tactic.NormCast
+import Lean.Elab.Tactic.Conv.Simp
+import Lean.Elab.ElabRules
+
+/-!
+# The `norm_cast` family of tactics.
+
+A full description of the tactic, and the use of each theorem category, can be found at
+<https://arxiv.org/abs/2001.10594>.
+-/
+namespace Lean.Elab.Tactic.NormCast
+open Lean Meta Simp NormCast
+
+-- TODO: trace name consistency
+builtin_initialize registerTraceClass `Tactic.norm_cast
+
+/-- Proves `a = b` using the given simp set. -/
+def proveEqUsing (s : SimpTheorems) (a b : Expr) : MetaM (Option Simp.Result) := do
+  let go : SimpM (Option Simp.Result) := do
+    let a' ← Simp.simp a
+    let b' ← Simp.simp b
+    unless ← isDefEq a'.expr b'.expr do return none
+    a'.mkEqTrans (← b'.mkEqSymm b)
+  withReducible do
+    (go (← Simp.mkDefaultMethods).toMethodsRef
+      { simpTheorems := #[s], congrTheorems := ← Meta.getSimpCongrTheorems }).run' {}
+
+/-- Proves `a = b` by simplifying using move and squash lemmas. -/
+def proveEqUsingDown (a b : Expr) : MetaM (Option Simp.Result) := do
+  withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} proving: {← mkEq a b}") do
+  proveEqUsing (← normCastExt.down.getTheorems) a b
+
+/-- Constructs the expression `(e : ty)`. -/
+def mkCoe (e : Expr) (ty : Expr) : MetaM Expr := do
+  let .some e' ← coerce? e ty | failure
+  return e'
+
+/--
+Checks whether an expression is the coercion of some other expression,
+and if so returns that expression.
+-/
+def isCoeOf? (e : Expr) : MetaM (Option Expr) := do
+  if let Expr.const fn .. := e.getAppFn then
+    if let some info ← getCoeFnInfo? fn then
+      if e.getAppNumArgs == info.numArgs then
+        return e.getArg! info.coercee
+  return none
+
+/--
+Checks whether an expression is a numeral in some type,
+and if so returns that type and the natural number.
+-/
+def isNumeral? (e : Expr) : Option (Expr × Nat) :=
+  -- TODO: cleanup, and possibly remove duplicate
+  if e.isConstOf ``Nat.zero then
+    (mkConst ``Nat, 0)
+  else if let Expr.app (Expr.app (Expr.app (Expr.const ``OfNat.ofNat ..) α ..)
+      (Expr.lit (Literal.natVal n) ..) ..) .. := e then
+    some (α, n)
+  else
+    none
+
+/--
+This is the main heuristic used alongside the elim and move lemmas.
+The goal is to help casts move past operators by adding intermediate casts.
+An expression of the shape:
+```
+op (↑(x : α) : γ) (↑(y : β) : γ)
+```
+is rewritten to:
+```
+op (↑(↑(x : α) : β) : γ) (↑(y : β) : γ)
+```
+when
+```
+(↑(↑(x : α) : β) : γ) = (↑(x : α) : γ)
+```
+can be proven with a squash lemma
+-/
+def splittingProcedure (expr : Expr) : MetaM Simp.Result := do
+  let Expr.app (Expr.app op x ..) y .. := expr | return {expr}
+
+  let Expr.forallE _ γ (Expr.forallE _ γ' ty ..) .. ← inferType op | return {expr}
+  if γ'.hasLooseBVars || ty.hasLooseBVars then return {expr}
+  unless ← isDefEq γ γ' do return {expr}
+
+  let msg := m!"splitting {expr}"
+  let msg
+    | .error _ => return m!"{bombEmoji} {msg}"
+    | .ok r => return if r.expr == expr then m!"{crossEmoji} {msg}" else
+      m!"{checkEmoji} {msg} to {r.expr}"
+  withTraceNode `Tactic.norm_cast msg do
+
+  try
+    let some x' ← isCoeOf? x | failure
+    let some y' ← isCoeOf? y | failure
+    let α ← inferType x'
+    let β ← inferType y'
+
+    -- TODO: fast timeout
+    (try
+      let x2 ← mkCoe (← mkCoe x' β) γ
+      let some x_x2 ← proveEqUsingDown x x2 | failure
+      Simp.mkCongrFun (← Simp.mkCongr {expr := op} x_x2) y
+    catch _ =>
+      let y2 ← mkCoe (← mkCoe y' α) γ
+      let some y_y2 ← proveEqUsingDown y y2 | failure
+      Simp.mkCongr {expr := mkApp op x} y_y2)
+  catch _ => try
+    let some (_, n) := isNumeral? y | failure
+    let some x' ← isCoeOf? x | failure
+    let α ← inferType x'
+    let y2 ← mkCoe (← mkNumeral α n) γ
+    let some y_y2 ← proveEqUsingDown y y2 | failure
+    Simp.mkCongr {expr := mkApp op x} y_y2
+  catch _ => try
+    let some (_, n) := isNumeral? x | failure
+    let some y' ← isCoeOf? y | failure
+    let β ← inferType y'
+    let x2 ← mkCoe (← mkNumeral β n) γ
+    let some x_x2 ← proveEqUsingDown x x2 | failure
+    Simp.mkCongrFun (← Simp.mkCongr {expr := op} x_x2) y
+  catch _ =>
+    return {expr}
+
+/--
+Discharging function used during simplification in the "squash" step.
+-/
+-- TODO: normCast takes a list of expressions to use as lemmas for the discharger
+-- TODO: a tactic to print the results the discharger fails to prove
+def prove (e : Expr) : SimpM (Option Expr) := do
+  withTraceNode `Tactic.norm_cast (return m!"{exceptOptionEmoji ·} discharging: {e}") do
+  return (← findLocalDeclWithType? e).map mkFVar
+
+/--
+Core rewriting function used in the "squash" step, which moves casts upwards
+and eliminates them.
+
+It tries to rewrite an expression using the elim and move lemmas.
+On failure, it calls the splitting procedure heuristic.
+-/
+partial def upwardAndElim (up : SimpTheorems) (e : Expr) : SimpM Simp.Step := do
+  let r ← withDischarger prove do
+    Simp.rewrite? e up.post up.erased (tag := "squash") (rflOnly := false)
+  let r := r.getD { expr := e }
+  let r ← r.mkEqTrans (← splittingProcedure r.expr)
+  if r.expr == e then return Simp.Step.done {expr := e}
+  return Simp.Step.visit r
+
+/--
+If possible, rewrites `(n : α)` to `(Nat.cast n : α)` where `n` is a numeral and `α ≠ ℕ`.
+Returns a pair of the new expression and proof that they are equal.
+-/
+def numeralToCoe (e : Expr) : MetaM Simp.Result := do
+  let some (α, n) := isNumeral? e | failure
+  if (← whnf α).isConstOf ``Nat then failure
+  let newE ← mkAppOptM ``Nat.cast #[α, none, toExpr n]
+  let some pr ← proveEqUsingDown e newE | failure
+  return pr
+
+/--
+The core simplification routine of `normCast`.
+-/
+def derive (e : Expr) : MetaM Simp.Result := do
+  withTraceNode `Tactic.norm_cast (fun _ => return m!"{e}") do
+  let e ← instantiateMVars e
+
+  let config : Simp.Config := {
+    zeta := false
+    beta := false
+    eta  := false
+    proj := false
+    iota := false
+  }
+  let congrTheorems ← Meta.getSimpCongrTheorems
+
+  let r : Simp.Result := { expr := e }
+
+  let withTrace phase := withTraceNode `Tactic.norm_cast fun
+    | .ok r => return m!"{r.expr} (after {phase})"
+    | .error _ => return m!"{bombEmoji} {phase}"
+
+  -- step 1: pre-processing of numerals
+  let r ← withTrace "pre-processing numerals" do
+    let post e := return Simp.Step.done (← try numeralToCoe e catch _ => pure {expr := e})
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+
+  -- step 2: casts are moved upwards and eliminated
+  let r ← withTrace "moving upward, splitting and eliminating" do
+    let post := upwardAndElim (← normCastExt.up.getTheorems)
+    r.mkEqTrans (← Simp.main r.expr { config, congrTheorems } (methods := { post })).1
+
+  -- step 3: casts are squashed
+  let r ← withTrace "squashing" do
+    let simpTheorems := #[← normCastExt.squash.getTheorems]
+    r.mkEqTrans (← simp r.expr { simpTheorems, config, congrTheorems }).1
+
+  return r
+
+open Term
+@[builtin_term_elab modCast] def elabModCast : TermElab := fun stx expectedType? => do
+  match stx with
+  | `(mod_cast $e:term) =>
+    withExpectedType expectedType? fun expectedType => do
+    if (← instantiateMVars expectedType).hasExprMVar then tryPostpone
+    let expectedType' ← derive expectedType
+    let e ← Term.elabTerm e expectedType'.expr
+    synthesizeSyntheticMVars
+    let eTy ← instantiateMVars (← inferType e)
+    if eTy.hasExprMVar then tryPostpone
+    let eTy' ← derive eTy
+    unless ← isDefEq eTy'.expr expectedType'.expr do
+      throwTypeMismatchError "mod_cast" expectedType'.expr eTy'.expr e
+    let eTy_eq_expectedType ← eTy'.mkEqTrans (← expectedType'.mkEqSymm expectedType )
+    eTy_eq_expectedType.mkCast e
+  | _ => throwUnsupportedSyntax
+
+/-- Implementation of the `norm_cast` tactic when operating on the main goal. -/
+def normCastTarget : TacticM Unit :=
+  liftMetaTactic1 fun goal => do
+    let tgt ← instantiateMVars (← goal.getType)
+    let prf ← derive tgt
+    applySimpResultToTarget goal tgt prf
+
+/-- Implementation of the `norm_cast` tactic when operating on a hypothesis. -/
+def normCastHyp (fvarId : FVarId) : TacticM Unit :=
+  liftMetaTactic1 fun goal => do
+    let hyp ← instantiateMVars (← fvarId.getDecl).type
+    let prf ← derive hyp
+    return (← applySimpResultToLocalDecl goal fvarId prf false).map (·.snd)
+
+@[builtin_tactic normCast0]
+def evalNormCast0 : Tactic := fun stx => do
+  match stx with
+  | `(tactic| norm_cast0 $[$loc?]?) =>
+    let loc := if let some loc := loc? then expandLocation loc else Location.targets #[] true
+    withMainContext do
+      match loc with
+      | Location.targets hyps target =>
+        if target then normCastTarget
+        (← getFVarIds hyps).forM normCastHyp
+      | Location.wildcard =>
+        normCastTarget
+        (← (← getMainGoal).getNondepPropHyps).forM normCastHyp
+  | _ => throwUnsupportedSyntax
+
+@[builtin_tactic Lean.Parser.Tactic.Conv.normCast]
+def evalConvNormCast : Tactic :=
+  open Elab.Tactic.Conv in fun _ => withMainContext do
+    applySimpResult (← derive (← getLhs))
+
+@[builtin_tactic pushCast]
+def evalPushCast : Tactic := fun stx => do
+  let { ctx, simprocs, dischargeWrapper } ← withMainContext do
+    mkSimpContext (simpTheorems := pushCastExt.getTheorems) stx (eraseLocal := false)
+  let ctx := { ctx with config := { ctx.config with failIfUnchanged := false } }
+  dischargeWrapper.with fun discharge? =>
+    discard <| simpLocation ctx simprocs discharge? (expandOptLocation stx[5])
+
+end Lean.Elab.Tactic.NormCast

src/Lean/Linter.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König
+-/
 prelude
 import Lean.Linter.Util
 import Lean.Linter.Builtin

src/Lean/Linter/Basic.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König
+-/
 prelude
 import Lean.Data.Options
 

src/Lean/Linter/Builtin.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König
+-/
 prelude
 import Lean.Linter.Util
 import Lean.Elab.Command

src/Lean/Linter/MissingDocs.lean

@@ -1,7 +1,6 @@
 /-
 Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
 Authors: Mario Carneiro
 -/
 prelude

src/Lean/Linter/UnusedVariables.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
 prelude
 import Lean.Elab.Command
 import Lean.Util.ForEachExpr

src/Lean/Linter/Util.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2022 Lars König. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lars König
+-/
 prelude
 import Lean.Data.Options
 import Lean.Server.InfoUtils

src/Lean/Meta/DiscrTree.lean

@@ -326,7 +326,26 @@ def reduceDT (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM Expr :=
 
 /- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
 
-private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) := do
+
+/--
+Append `n` wildcards to `todo`
+-/
+private def pushWildcards (n : Nat) (todo : Array Expr) : Array Expr :=
+  match n with
+  | 0   => todo
+  | n+1 => pushWildcards n (todo.push tmpStar)
+
+/--
+When `noIndexAtArgs := true`, `pushArgs` assumes function application arguments have a `no_index` annotation.
+That is, `f a b` is indexed as it was `f (no_index a) (no_index b)`.
+This feature is used when indexing local proofs in the simplifier. This is useful in examples like the one described on issue #2670.
+In this issue, we have a local hypotheses `(h : ∀ p : α × β, f p p.2 = p.2)`, and users expect it to be applicable to
+`f (a, b) b = b`. This worked in Lean 3 since no indexing was used. We can retrieve Lean 3 behavior by writing
+`(h : ∀ p : α × β, f p (no_index p.2) = p.2)`, but this is very inconvenient when the hypotheses was not written by the user in first place.
+For example, it was introduced by another tactic. Thus, when populating the discrimination tree explicit arguments provided to `simp` (e.g., `simp [h]`),
+we use `noIndexAtArgs := true`. See comment: https://github.com/leanprover/lean4/issues/2670#issuecomment-1758889365
+-/
+private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : WhnfCoreConfig) (noIndexAtArgs : Bool) : MetaM (Key × Array Expr) := do
   if hasNoindexAnnotation e then
     return (.star, todo)
   else
@@ -334,7 +353,10 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
     let fn := e.getAppFn
     let push (k : Key) (nargs : Nat) (todo : Array Expr): MetaM (Key × Array Expr) := do
       let info ← getFunInfoNArgs fn nargs
-      let todo ← pushArgsAux info.paramInfo (nargs-1) e todo
+      let todo ← if noIndexAtArgs then
+        pure <| pushWildcards nargs todo
+      else
+        pushArgsAux info.paramInfo (nargs-1) e todo
       return (k, todo)
     match fn with
     | .lit v     =>
@@ -378,22 +400,24 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
     | _ =>
       return (.other, todo)
 
-partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (config : WhnfCoreConfig) : MetaM (Array Key) := do
+@[inherit_doc pushArgs]
+partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (config : WhnfCoreConfig) (noIndexAtArgs : Bool) : MetaM (Array Key) := do
   if todo.isEmpty then
     return keys
   else
     let e    := todo.back
     let todo := todo.pop
-    let (k, todo) ← pushArgs root todo e config
-    mkPathAux false todo (keys.push k) config
+    let (k, todo) ← pushArgs root todo e config noIndexAtArgs
+    mkPathAux false todo (keys.push k) config noIndexAtArgs
 
 private def initCapacity := 8
 
-def mkPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
+@[inherit_doc pushArgs]
+def mkPath (e : Expr) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM (Array Key) := do
   withReducible do
     let todo : Array Expr := .mkEmpty initCapacity
     let keys : Array Key := .mkEmpty initCapacity
-    mkPathAux (root := true) (todo.push e) keys config
+    mkPathAux (root := true) (todo.push e) keys config noIndexAtArgs
 
 private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
   if h : i < keys.size then
@@ -447,22 +471,21 @@ def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTr
       let c := insertAux keys v 1 c
       { root := d.root.insert k c }
 
-def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) : MetaM (DiscrTree α) := do
-  let keys ← mkPath e config
+def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
+  let keys ← mkPath e config noIndexAtArgs
   return d.insertCore keys v
 
 /--
 Inserts a value into a discrimination tree,
 but only if its key is not of the form `#[*]` or `#[=, *, *, *]`.
 -/
-def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) : MetaM (DiscrTree α) := do
-  let keys ← mkPath e config
+def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
+  let keys ← mkPath e config noIndexAtArgs
   return if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
     d
   else
     d.insertCore keys v
 
-
 private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) := do
   let e ← reduceDT e root config
   unless root do

src/Lean/Meta/Tactic.lean

@@ -32,3 +32,4 @@ import Lean.Meta.Tactic.AC
 import Lean.Meta.Tactic.Refl
 import Lean.Meta.Tactic.Congr
 import Lean.Meta.Tactic.Repeat
+import Lean.Meta.Tactic.NormCast

src/Lean/Meta/Tactic/NormCast.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2019 Paul-Nicolas Madelaine. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul-Nicolas Madelaine, Robert Y. Lewis, Mario Carneiro, Gabriel Ebner
+-/
+import Lean.Meta.CongrTheorems
+import Lean.Meta.Tactic.Simp.SimpTheorems
+import Lean.Meta.CoeAttr
+
+namespace Lean.Meta.NormCast
+/--
+`Label` is a type used to classify `norm_cast` lemmas.
+* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
+* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
+* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
+-/
+inductive Label
+  /-- elim lemma: LHS has 0 head coes and ≥ 1 internal coe -/
+  | elim
+  /-- move lemma: LHS has 1 head coe and 0 internal coes,
+  RHS has 0 head coes and ≥ 1 internal coes -/
+  | move
+  /-- squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes -/
+  | squash
+  deriving DecidableEq, Repr, Inhabited
+
+/-- Assuming `e` is an application, returns the list of subterms that `simp` will rewrite in. -/
+def getSimpArgs (e : Expr) : MetaM (Array Expr) := do
+  match ← mkCongrSimp? e.getAppFn with
+  | none => return e.getAppArgs
+  | some {argKinds, ..} =>
+    let mut args := #[]
+    for a in e.getAppArgs, k in argKinds do
+      if k matches .eq then
+        args := args.push a
+    return args
+
+/-- Counts how many coercions are at the head of the expression. -/
+partial def countHeadCoes (e : Expr) : MetaM Nat := do
+  if let Expr.const fn .. := e.getAppFn then
+    if let some info ← getCoeFnInfo? fn then
+      if e.getAppNumArgs >= info.numArgs then
+        return (← countHeadCoes (e.getArg! info.coercee)) + 1
+  return 0
+
+/-- Counts how many coercions are inside the expression, including the head ones. -/
+partial def countCoes (e : Expr) : MetaM Nat :=
+  lambdaTelescope e fun _ e => do
+    if let Expr.const fn .. := e.getAppFn then
+      if let some info ← getCoeFnInfo? fn then
+        if e.getAppNumArgs >= info.numArgs then
+          let mut coes := (← countHeadCoes (e.getArg! info.coercee)) + 1
+          for i in [info.numArgs:e.getAppNumArgs] do
+            coes := coes + (← countCoes (e.getArg! i))
+          return coes
+    return (← (← getSimpArgs e).mapM countCoes).foldl (·+·) 0
+
+/-- Counts how many coercions are inside the expression, excluding the head ones. -/
+def countInternalCoes (e : Expr) : MetaM Nat :=
+  return (← countCoes e) - (← countHeadCoes e)
+
+/-- Classifies a declaration of type `ty` as a `norm_cast` rule. -/
+def classifyType (ty : Expr) : MetaM Label :=
+  forallTelescopeReducing ty fun _ ty => do
+    let ty ← whnf ty
+    let (lhs, rhs) ←
+      if ty.isAppOfArity ``Eq 3 then pure (ty.getArg! 1, ty.getArg! 2)
+      else if ty.isAppOfArity ``Iff 2 then pure (ty.getArg! 0, ty.getArg! 1)
+      else throwError "norm_cast: lemma must be = or ↔, but is{indentExpr ty}"
+    let lhsCoes ← countCoes lhs
+    if lhsCoes = 0 then
+      throwError "norm_cast: badly shaped lemma, lhs must contain at least one coe{indentExpr lhs}"
+    let lhsHeadCoes ← countHeadCoes lhs
+    let rhsHeadCoes ← countHeadCoes rhs
+    let rhsInternalCoes ← countInternalCoes rhs
+    if lhsHeadCoes = 0 then
+      return Label.elim
+    else if lhsHeadCoes = 1 then do
+      unless rhsHeadCoes = 0 do
+        throwError "norm_cast: badly shaped lemma, rhs can't start with coe{indentExpr rhs}"
+      if rhsInternalCoes = 0 then
+        return Label.squash
+      else
+        return Label.move
+    else if rhsHeadCoes < lhsHeadCoes then do
+      return Label.squash
+    else do
+      throwError "\
+        norm_cast: badly shaped shaped squash lemma, \
+        rhs must have fewer head coes than lhs{indentExpr ty}"
+
+/-- The `push_cast` simp attribute. -/
+initialize pushCastExt : SimpExtension ←
+  registerSimpAttr `push_cast "\
+    The `push_cast` simp attribute uses `norm_cast` lemmas \
+    to move casts toward the leaf nodes of the expression."
+
+/--  The `norm_cast` attribute stores a simp set for each of the three types of `norm_cast` lemma. -/
+structure NormCastExtension where
+  /-- A simp set which lifts coercions to the top level. -/
+  up : SimpExtension
+  /-- A simp set which pushes coercions to the leaves. -/
+  down : SimpExtension
+  /-- A simp set which simplifies transitive coercions. -/
+  squash : SimpExtension
+deriving Inhabited
+
+/-- The `norm_cast` extension data. -/
+builtin_initialize normCastExt : NormCastExtension ← pure {
+  up := ← mkSimpExt (decl_name% ++ `up)
+  down := ← mkSimpExt (decl_name% ++ `down)
+  squash := ← mkSimpExt (decl_name% ++ `squash)
+}
+
+/-- `addElim decl` adds `decl` as an `elim` lemma to be used by `norm_cast`. -/
+def addElim (decl : Name)
+    (kind := AttributeKind.global) (prio := eval_prio default) : MetaM Unit :=
+  addSimpTheorem normCastExt.up decl (post := true) (inv := false) kind prio
+
+/-- `addMove decl` adds `decl` as a `move` lemma to be used by `norm_cast`. -/
+def addMove (decl : Name)
+    (kind := AttributeKind.global) (prio := eval_prio default) : MetaM Unit := do
+  addSimpTheorem pushCastExt decl (post := true) (inv := false) kind prio
+  addSimpTheorem normCastExt.up decl (post := true) (inv := true) kind prio
+  addSimpTheorem normCastExt.down decl (post := true) (inv := false) kind prio
+
+/-- `addSquash decl` adds `decl` as a `squash` lemma to be used by `norm_cast`. -/
+def addSquash (decl : Name)
+    (kind := AttributeKind.global) (prio := eval_prio default) : MetaM Unit := do
+  addSimpTheorem pushCastExt decl (post := true) (inv := false) kind prio
+  addSimpTheorem normCastExt.squash decl (post := true) (inv := false) kind prio
+  addSimpTheorem normCastExt.down decl (post := true) (inv := false) kind prio
+
+/-- `addInfer decl` infers the label of `decl` (`elim`, `move`, or `squash`) and arranges for it to
+be used by `norm_cast`.
+
+* elim lemma:   LHS has 0 head coes and ≥ 1 internal coe
+* move lemma:   LHS has 1 head coe and 0 internal coes,    RHS has 0 head coes and ≥ 1 internal coes
+* squash lemma: LHS has ≥ 1 head coes and 0 internal coes, RHS has fewer head coes
+-/
+def addInfer (decl : Name)
+    (kind := AttributeKind.global) (prio := eval_prio default) : MetaM Unit := do
+  let ty := (← getConstInfo decl).type
+  match ← classifyType ty with
+  | Label.elim => addElim decl kind prio
+  | Label.squash => addSquash decl kind prio
+  | Label.move => addMove decl kind prio
+
+builtin_initialize registerBuiltinAttribute {
+  name := `norm_cast
+  descr := "attribute for norm_cast"
+  add := fun decl stx kind => MetaM.run' do
+    let `(attr| norm_cast $[$label:normCastLabel]? $[$prio]?) := stx | unreachable!
+    let prio := (prio.bind (·.1.isNatLit?)).getD (eval_prio default)
+    match label.bind (·.1.isStrLit?) with
+    | "elim" => addElim decl kind prio
+    | "move" => addMove decl kind prio
+    | "squash" => addSquash decl kind prio
+    | none => addInfer decl kind prio
+    | _ => unreachable!
+}
+
+end Lean.Meta.NormCast

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean

@@ -11,3 +11,4 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -0,0 +1,299 @@
+/-
+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
+-/
+prelude
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
+import Init.Data.BitVec.Basic
+
+namespace Std.BitVec
+open Lean Meta Simp
+
+/-- A bit-vector literal -/
+structure Literal where
+  /-- Size. -/
+  n     : Nat
+  /-- Actual value. -/
+  value : BitVec n
+
+/--
+Try to convert an `OfNat.ofNat`-application into a bitvector literal.
+-/
+private def fromOfNatExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  guard (e.isAppOfArity ``OfNat.ofNat 3)
+  let type ← whnf e.appFn!.appFn!.appArg!
+  guard (type.isAppOfArity ``BitVec 1)
+  let n ← Nat.fromExpr? type.appArg!
+  let v ← Nat.fromExpr? e.appFn!.appArg!
+  return { n, value := BitVec.ofNat n v }
+
+/--
+Try to convert an `Std.BitVec.ofNat`-application into a bitvector literal.
+-/
+private def fromBitVecExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  guard (e.isAppOfArity ``Std.BitVec.ofNat 2)
+  let n ← Nat.fromExpr? e.appFn!.appArg!
+  let v ← Nat.fromExpr? e.appArg!
+  return { n, value := BitVec.ofNat n v }
+
+/--
+Try to convert `OfNat.ofNat`/`Std.BitVec.OfNat` application into a
+bitvector literal.
+-/
+def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
+  fromBitVecExpr? e <|> fromOfNatExpr? e
+
+/--
+Convert a bitvector literal into an expression.
+-/
+-- Using `Std.BitVec.ofNat` because it is being used in `simp` theorems
+def Literal.toExpr (lit : Literal) : Expr :=
+  mkApp2 (mkConst ``Std.BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
+
+/--
+Helper function for reducing homogenous unary bitvector operators.
+-/
+@[inline] def reduceUnary (declName : Name) (arity : Nat)
+    (op : {n : Nat} → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let v := { v with value := op v.value }
+  return .done { expr := v.toExpr }
+
+/--
+Helper function for reducing homogenous binary bitvector operators.
+-/
+@[inline] def reduceBin (declName : Name) (arity : Nat)
+    (op : {n : Nat} → BitVec n → BitVec n → BitVec n) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  if h : v₁.n = v₂.n then
+    trace[Meta.debug] "reduce [{declName}] {v₁.value}, {v₂.value}"
+    let v := { v₁ with value := op v₁.value (h ▸ v₂.value) }
+    return .done { expr := v.toExpr }
+  else
+    return .continue
+
+/-- Simplification procedure for `zeroExtend` and `signExtend` on `BitVec`s. -/
+@[inline] def reduceExtend (declName : Name)
+    (op : {n : Nat} → (m : Nat) → BitVec n → BitVec m) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName 3 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n, value := op n v.value }
+  return .done { expr := lit.toExpr }
+
+/--
+Helper function for reducing bitvector functions such as `getLsb` and `getMsb`.
+-/
+@[inline] def reduceGetBit (declName : Name) (op : {n : Nat} → BitVec n → Nat → Bool) (e : Expr)
+    : SimpM Step := do
+  unless e.isAppOfArity declName 3 do return .continue
+  let some v ← fromExpr? e.appFn!.appArg! | return .continue
+  let some i ← Nat.fromExpr? e.appArg! | return .continue
+  let b := op v.value i
+  return .done { expr := toExpr b }
+
+/--
+Helper function for reducing bitvector functions such as `shiftLeft` and `rotateRight`.
+-/
+@[inline] def reduceShift (declName : Name) (arity : Nat)
+    (op : {n : Nat} → BitVec n → Nat → BitVec n) (e : Expr) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v ← fromExpr? e.appFn!.appArg! | return .continue
+  let some i ← Nat.fromExpr? e.appArg! | return .continue
+  let v := { v with value := op v.value i }
+  return .done { expr := v.toExpr }
+
+/--
+Helper function for reducing bitvector predicates.
+-/
+@[inline] def reduceBinPred (declName : Name) (arity : Nat)
+    (op : {n : Nat} → BitVec n → BitVec n → Bool) (e : Expr) (isProp := true) : SimpM Step := do
+  unless e.isAppOfArity declName arity do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  if h : v₁.n = v₂.n then
+    let b := op v₁.value (h ▸ v₂.value)
+    if isProp then
+      evalPropStep e b
+    else
+      return .done { expr := toExpr b }
+  else
+    return .continue
+
+/-- Simplification procedure for negation of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceNeg ((- _ : BitVec _)) := reduceUnary ``Neg.neg 3 (- ·)
+/-- Simplification procedure for bitwise not of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceNot ((~~~ _ : BitVec _)) :=
+  reduceUnary ``Complement.complement 3 (~~~ ·)
+/-- Simplification procedure for absolute value of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceAbs (BitVec.abs _) := reduceUnary ``BitVec.abs 2 BitVec.abs
+/-- Simplification procedure for bitwise and of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceAnd ((_ &&& _ : BitVec _)) := reduceBin ``HAnd.hAnd 6 (· &&& ·)
+/-- Simplification procedure for bitwise or of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceOr ((_ ||| _ : BitVec _)) := reduceBin ``HOr.hOr 6 (· ||| ·)
+/-- Simplification procedure for bitwise xor of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceXOr ((_ ^^^ _ : BitVec _)) := reduceBin ``HXor.hXor 6 (· ^^^ ·)
+/-- Simplification procedure for addition of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceAdd ((_ + _ : BitVec _)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+/-- Simplification procedure for multiplication of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceMul ((_ * _ : BitVec _)) := reduceBin ``HMul.hMul 6 (· * ·)
+/-- Simplification procedure for subtraction of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSub ((_ - _ : BitVec _)) := reduceBin ``HSub.hSub 6 (· - ·)
+/-- Simplification procedure for division of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceDiv ((_ / _ : BitVec _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+/-- Simplification procedure for the modulo operation on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceMod ((_ % _ : BitVec _)) := reduceBin ``HMod.hMod 6 (· % ·)
+/-- Simplification procedure for for the unsigned modulo operation on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceUMod ((umod _ _ : BitVec _)) := reduceBin ``umod 3 umod
+/-- Simplification procedure for unsigned division of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceUDiv ((udiv _ _ : BitVec _)) := reduceBin ``udiv 3 udiv
+/-- Simplification procedure for division of `BitVec`s using the SMT-Lib conventions. -/
+builtin_simproc [simp, seval] reduceSMTUDiv ((smtUDiv _ _ : BitVec _)) := reduceBin ``smtUDiv 3 smtUDiv
+/-- Simplification procedure for the signed modulo operation on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSMod ((smod _ _ : BitVec _)) := reduceBin ``smod 3 smod
+/-- Simplification procedure for signed remainder of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSRem ((srem _ _ : BitVec _)) := reduceBin ``srem 3 srem
+/-- Simplification procedure for signed t-division of `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSDiv ((sdiv _ _ : BitVec _)) := reduceBin ``sdiv 3 sdiv
+/-- Simplification procedure for signed division of `BitVec`s using the SMT-Lib conventions. -/
+builtin_simproc [simp, seval] reduceSMTSDiv ((smtSDiv _ _ : BitVec _)) := reduceBin ``smtSDiv 3 smtSDiv
+/-- Simplification procedure for `getLsb` (lowest significant bit) on `BitVec`. -/
+builtin_simproc [simp, seval] reduceGetLsb (getLsb _ _) := reduceGetBit ``getLsb getLsb
+/-- Simplification procedure for `getMsb` (most significant bit) on `BitVec`. -/
+builtin_simproc [simp, seval] reduceGetMsb (getMsb _ _) := reduceGetBit ``getMsb getMsb
+
+/-- Simplification procedure for shift left on `BitVec`. -/
+builtin_simproc [simp, seval] reduceShiftLeft (BitVec.shiftLeft _ _) :=
+  reduceShift ``BitVec.shiftLeft 3 BitVec.shiftLeft
+/-- Simplification procedure for unsigned shift right on `BitVec`. -/
+builtin_simproc [simp, seval] reduceUShiftRight (BitVec.ushiftRight _ _) :=
+  reduceShift ``BitVec.ushiftRight 3 BitVec.ushiftRight
+/-- Simplification procedure for signed shift right on `BitVec`. -/
+builtin_simproc [simp, seval] reduceSShiftRight (BitVec.sshiftRight _ _) :=
+  reduceShift ``BitVec.sshiftRight 3 BitVec.sshiftRight
+/-- Simplification procedure for shift left on `BitVec`. -/
+builtin_simproc [simp, seval] reduceHShiftLeft ((_ <<< _ : BitVec _)) :=
+  reduceShift ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+/-- Simplification procedure for shift right on `BitVec`. -/
+builtin_simproc [simp, seval] reduceHShiftRight ((_ >>> _ : BitVec _)) :=
+  reduceShift ``HShiftRight.hShiftRight 6 (· >>> ·)
+/-- Simplification procedure for rotate left on `BitVec`. -/
+builtin_simproc [simp, seval] reduceRotateLeft (BitVec.rotateLeft _ _) :=
+  reduceShift ``BitVec.rotateLeft 3 BitVec.rotateLeft
+/-- Simplification procedure for rotate right on `BitVec`. -/
+builtin_simproc [simp, seval] reduceRotateRight (BitVec.rotateRight _ _) :=
+  reduceShift ``BitVec.rotateRight 3 BitVec.rotateRight
+
+/-- Simplification procedure for append on `BitVec`. -/
+builtin_simproc [simp, seval] reduceAppend ((_ ++ _ : BitVec _)) := fun e => do
+  unless e.isAppOfArity ``HAppend.hAppend 6 do return .continue
+  let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
+  let some v₂ ← fromExpr? e.appArg! | return .continue
+  let v : Literal := { n := v₁.n + v₂.n, value := v₁.value ++ v₂.value }
+  return .done { expr := v.toExpr }
+
+/-- Simplification procedure for casting `BitVec`s along an equality of the size. -/
+builtin_simproc [simp, seval] reduceCast (cast _ _) := fun e => do
+  unless e.isAppOfArity ``cast 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some m ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let v : Literal := { n := m, value := BitVec.ofNat m v.value.toNat }
+  return .done { expr := v.toExpr }
+
+/-- Simplification procedure for `BitVec.toNat`. -/
+builtin_simproc [simp, seval] reduceToNat (BitVec.toNat _) := fun e => do
+  unless e.isAppOfArity ``BitVec.toNat 2 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  return .done { expr := mkNatLit v.value.toNat }
+
+/-- Simplification procedure for `BitVec.toInt`. -/
+builtin_simproc [simp, seval] reduceToInt (BitVec.toInt _) := fun e => do
+  unless e.isAppOfArity ``BitVec.toInt 2 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  return .done { expr := Int.toExpr v.value.toInt }
+
+/-- Simplification procedure for `BitVec.ofInt`. -/
+builtin_simproc [simp, seval] reduceOfInt (BitVec.ofInt _ _) := fun e => do
+  unless e.isAppOfArity ``BitVec.ofInt 2 do return .continue
+  let some n ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let some i ← Int.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n, value := BitVec.ofInt n i }
+  return .done { expr := lit.toExpr }
+
+/-- Simplification procedure for `<` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceLT (( _ : BitVec _) < _)  := reduceBinPred ``LT.lt 4 (· < ·)
+/-- Simplification procedure for `≤` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceLE (( _ : BitVec _) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+/-- Simplification procedure for `>` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceGT (( _ : BitVec _) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+/-- Simplification procedure for `≥` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceGE (( _ : BitVec _) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+
+/-- Simplification procedure for unsigned less than `ult` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceULT (BitVec.ult _ _) :=
+  reduceBinPred ``BitVec.ult 3 BitVec.ult (isProp := false)
+/-- Simplification procedure for unsigned less than or equal `ule` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceULE (BitVec.ule _ _) :=
+  reduceBinPred ``BitVec.ule 3 BitVec.ule (isProp := false)
+/-- Simplification procedure for signed less than `slt` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSLT (BitVec.slt _ _) :=
+  reduceBinPred ``BitVec.slt 3 BitVec.slt (isProp := false)
+/-- Simplification procedure for signed less than or equal `sle` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSLE (BitVec.sle _ _) :=
+  reduceBinPred ``BitVec.sle 3 BitVec.sle (isProp := false)
+
+/-- Simplification procedure for `zeroExtend'` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
+  unless e.isAppOfArity ``zeroExtend' 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some w ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  if h : v.n ≤ w then
+    let lit : Literal := { n := w, value := v.value.zeroExtend' h }
+    return .done { expr := lit.toExpr }
+  else
+    return .continue
+
+/-- Simplification procedure for `shiftLeftZeroExtend` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceShiftLeftZeroExtend (shiftLeftZeroExtend _ _) := fun e => do
+  unless e.isAppOfArity ``shiftLeftZeroExtend 3 do return .continue
+  let some v ← fromExpr? e.appFn!.appArg! | return .continue
+  let some m ← Nat.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n := v.n + m, value := v.value.shiftLeftZeroExtend m }
+  return .done { expr := lit.toExpr }
+
+/-- Simplification procedure for `extractLsb'` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceExtracLsb' (extractLsb' _ _ _) := fun e => do
+  unless e.isAppOfArity ``extractLsb' 4 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some start ← Nat.fromExpr? e.appFn!.appFn!.appArg! | return .continue
+  let some len ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n := len, value := v.value.extractLsb' start len }
+  return .done { expr := lit.toExpr }
+
+/-- Simplification procedure for `replicate` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
+  unless e.isAppOfArity ``replicate 3 do return .continue
+  let some v ← fromExpr? e.appArg! | return .continue
+  let some w ← Nat.fromExpr? e.appFn!.appArg! | return .continue
+  let lit : Literal := { n := v.n * w, value := v.value.replicate w }
+  return .done { expr := lit.toExpr }
+
+/-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
+
+/-- Simplification procedure for `signExtend` on `BitVec`s. -/
+builtin_simproc [simp, seval] reduceSignExtend (signExtend _ _) := reduceExtend ``signExtend signExtend
+
+/-- Simplification procedure for `allOnes` -/
+builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
+  unless e.isAppOfArity ``allOnes 1 do return .continue
+  let some n ← Nat.fromExpr? e.appArg! | return .continue
+  let lit : Literal := { n, value := allOnes n }
+  return .done { expr := lit.toExpr }
+
+end Std.BitVec

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -319,7 +319,7 @@ private def checkTypeIsProp (type : Expr) : MetaM Unit :=
   unless (← isProp type) do
     throwError "invalid 'simp', proposition expected{indentExpr type}"
 
-private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr) (post : Bool) (prio : Nat) : MetaM SimpTheorem := do
+private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array Name) (proof : Expr) (post : Bool) (prio : Nat) (noIndexAtArgs : Bool) : MetaM SimpTheorem := do
   assert! origin != .fvar ⟨.anonymous⟩
   let type ← instantiateMVars (← inferType e)
   withNewMCtxDepth do
@@ -327,7 +327,7 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
     let type ← whnfR type
     let (keys, perm) ←
       match type.eq? with
-      | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs simpDtConfig, ← isPerm lhs rhs)
+      | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs simpDtConfig noIndexAtArgs, ← isPerm lhs rhs)
       | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"
     return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) }
 
@@ -341,10 +341,10 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool)
       let mut r := #[]
       for (val, type) in (← preprocess val type inv (isGlobal := true)) do
         let auxName ← mkAuxLemma cinfo.levelParams type val
-        r := r.push <| (← mkSimpTheoremCore (.decl declName post inv) (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio)
+        r := r.push <| (← mkSimpTheoremCore (.decl declName post inv) (mkConst auxName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst auxName) post prio (noIndexAtArgs := false))
       return r
     else
-      return #[← mkSimpTheoremCore (.decl declName post inv) (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio]
+      return #[← mkSimpTheoremCore (.decl declName post inv) (mkConst declName (cinfo.levelParams.map mkLevelParam)) #[] (mkConst declName) post prio (noIndexAtArgs := false)]
 
 inductive SimpEntry where
   | thm      : SimpTheorem → SimpEntry
@@ -455,7 +455,7 @@ private def preprocessProof (val : Expr) (inv : Bool) : MetaM (Array Expr) := do
 /-- Auxiliary method for creating simp theorems from a proof term `val`. -/
 def mkSimpTheorems (id : Origin) (levelParams : Array Name) (proof : Expr) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM (Array SimpTheorem) :=
   withReducible do
-    (← preprocessProof proof inv).mapM fun val => mkSimpTheoremCore id val levelParams val post prio
+    (← preprocessProof proof inv).mapM fun val => mkSimpTheoremCore id val levelParams val post prio (noIndexAtArgs := true)
 
 /-- Auxiliary method for adding a local simp theorem to a `SimpTheorems` datastructure. -/
 def SimpTheorems.add (s : SimpTheorems) (id : Origin) (levelParams : Array Name) (proof : Expr) (inv := false) (post := true) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -37,6 +37,13 @@ def mkEqTransOptProofResult (h? : Option Expr) (cache : Bool) (r : Result) : Met
 def Result.mkEqTrans (r₁ r₂ : Result) : MetaM Result :=
   mkEqTransOptProofResult r₁.proof? r₁.cache r₂
 
+/-- Flip the proof in a `Simp.Result`. -/
+def Result.mkEqSymm (e : Expr) (r : Simp.Result) : MetaM Simp.Result :=
+  ({ expr := e, proof? := · }) <$>
+  match r.proof? with
+  | none => pure none
+  | some p => some <$> Meta.mkEqSymm p
+
 abbrev Cache := ExprMap Result
 
 abbrev CongrCache := ExprMap (Option CongrTheorem)
@@ -277,6 +284,10 @@ def Result.getProof' (source : Expr) (r : Result) : MetaM Expr := do
          are not definitionally equal at `TransparencyMode.reducible` -/
       mkExpectedTypeHint (← mkEqRefl r.expr) (← mkEq source r.expr)
 
+/-- Construct the `Expr` `cast h e`, from a `Simp.Result` with proof `h`. -/
+def Result.mkCast (r : Simp.Result) (e : Expr) : MetaM Expr := do
+  mkAppM ``cast #[← r.getProof, e]
+
 def mkCongrFun (r : Result) (a : Expr) : MetaM Result :=
   match r.proof? with
   | none   => return { expr := mkApp r.expr a, proof? := none }

src/Lean/Server/Rpc/Deriving.lean

@@ -41,7 +41,6 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
       decInits := decInits.push (← `(structInstField| $fid:ident := ← rpcDecode a.$fid))
 
   let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName
-
   let indName := mkIdent indVal.name
   `(-- Workaround for https://github.com/leanprover/lean4/issues/2044
     namespace $indName
@@ -57,7 +56,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr
       enc a := return toJson { $[$encInits],* : RpcEncodablePacket }
       dec j := do
         let a : RpcEncodablePacket ← fromJson? j
-        return { $[$decInits],* }
+        return { $decInits:structInstField,* }
     end $indName
   )
 

src/Lean/Util/TestExtern.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2023 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
 prelude
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.Command

src/Lean/Widget/Basic.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2022 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
 prelude
 import Lean.Elab.InfoTree
 import Lean.Message

src/Leanc.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2022 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
 import Lean.Compiler.FFI
 
 open Lean.Compiler.FFI

src/lake/Lake/Config/LeanConfig.lean

@@ -1,10 +1,10 @@
-import Lean.Util.LeanOptions
-
 /-
 Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lean.Util.LeanOptions
+
 namespace Lake
 
 /--

src/lake/lakefile.lean

@@ -1,3 +1,8 @@
+/-
+Copyright (c) 2022 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
 import Lake.DSL
 open System Lake DSL