From 27fdfd1e6851a36dec90d5a50b36348e4b415494 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Mon, 31 Mar 2025 11:21:31 +0200
Subject: [PATCH 1/9] implement BitVec.splitBE, BitVec.splitLE,
 Vector.flatMapBitVec, and Vector.flattenBitVec

---
 src/Init/Data/BitVec/Basic.lean | 33 +++++++++++++++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index dc2689bdd39f..07f93f0dd56a 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -9,6 +9,7 @@ import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Nat.Power2
 import Init.Data.Int.Bitwise
 import Init.Data.BitVec.BasicAux
+import Init.Data.Vector.Basic
 
 /-!
 We define the basic algebraic structure of bitvectors. We choose the `Fin` representation over
@@ -704,8 +705,8 @@ treating `x` and `y` as 2's complement signed bitvectors.
 def ssubOverflow {w : Nat} (x y : BitVec w) : Bool :=
   (x.toInt - y.toInt ≥ 2 ^ (w - 1)) || (x.toInt - y.toInt < - 2 ^ (w - 1))
 
-/-- `negOverflow x` returns `true` if the negation of `x` results in overflow. 
-For a BitVec `x` with width `0 < w`, this only happens if `x = intMin`. 
+/-- `negOverflow x` returns `true` if the negation of `x` results in overflow.
+For a BitVec `x` with width `0 < w`, this only happens if `x = intMin`.
 
   SMT-Lib name: `bvnego`.
 -/
@@ -719,4 +720,32 @@ def reverse : {w : Nat} → BitVec w → BitVec w
   | 0, x => x
   | w + 1, x => concat (reverse (x.truncate w)) (x.msb)
 
+/- ### vectors of bitvectors -/
+
+/-- Split a bitvector into a vector of bitvectors of equal length where the vector ends on the
+most significant part. -/
+def splitBE (m n : Nat) (x : BitVec (m * n)) : Vector (BitVec m) n :=
+  let rec v n' := match n' with
+  | 0 => .emptyWithCapacity n
+  | n' + 1 => (v n').push (x.extractLsb' (m * n') m)
+  v n
+
+/-- Split a bitvector into a vector of bitvectors of equal length where the vector ends on the
+least significant part. -/
+def splitLE (m n : Nat) (x : BitVec (m * n)) : Vector (BitVec m) n :=
+  let rec v n' := match n' with
+  | 0 => .emptyWithCapacity n
+  | n' + 1 => (v n').push (x.extractLsb' (m * (n - n' - 1)) m)
+  v n
+
 end BitVec
+
+/-- Flatten a `Vector α n` to a `BitVec (m * n)` using a function `f : α → BitVec m`. -/
+def Vector.flatMapBitVec (v : Vector α n) (f : α → BitVec m) : BitVec (m * n) :=
+  match n with
+  | 0 => 0#0
+  | n + 1 => ((v.pop.flatMapBitVec f).cast (by simp) : BitVec (m * n)) ++ f v.back
+
+/-- Flatten a vector of bitvectors of equal length to a single bitvector. -/
+def Vector.flattenBitVec (v : Vector (BitVec m) n) : BitVec (m * n) :=
+  v.flatMapBitVec id

From e0648484fcd485296b9432301761950200ae5c9c Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Mon, 31 Mar 2025 11:29:52 +0200
Subject: [PATCH 2/9] add big-endian versions of flattening functions

---
 src/Init/Data/BitVec/Basic.lean | 26 ++++++++++++++++++++------
 1 file changed, 20 insertions(+), 6 deletions(-)

diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 07f93f0dd56a..867dc2c0b34f 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -740,12 +740,26 @@ def splitLE (m n : Nat) (x : BitVec (m * n)) : Vector (BitVec m) n :=
 
 end BitVec
 
-/-- Flatten a `Vector α n` to a `BitVec (m * n)` using a function `f : α → BitVec m`. -/
-def Vector.flatMapBitVec (v : Vector α n) (f : α → BitVec m) : BitVec (m * n) :=
+/-- Flatten a `Vector α n` to a `BitVec (m * n)` using a function `f : α → BitVec m`.
+The most significant bits are expected to be at the start of the vector. -/
+def Vector.flatMapBitVecLE (m : Nat) (v : Vector α n) (f : α → BitVec m) : BitVec (m * n) :=
   match n with
   | 0 => 0#0
-  | n + 1 => ((v.pop.flatMapBitVec f).cast (by simp) : BitVec (m * n)) ++ f v.back
+  | n + 1 => ((v.pop.flatMapBitVecLE m f).cast (by simp) : BitVec (m * n)) ++ f v.back
 
-/-- Flatten a vector of bitvectors of equal length to a single bitvector. -/
-def Vector.flattenBitVec (v : Vector (BitVec m) n) : BitVec (m * n) :=
-  v.flatMapBitVec id
+/-- Flatten a vector of bitvectors of equal length to a single bitvector.
+The most significant bits are expected to be at the start of the vector. -/
+def Vector.flattenBitVecLE (m : Nat) (v : Vector (BitVec m) n) : BitVec (m * n) :=
+  v.flatMapBitVecLE m id
+
+/-- Flatten a `Vector α n` to a `BitVec (m * n)` using a function `f : α → BitVec m`.
+The most significant bits are expected to be at the start of the vector. -/
+def Vector.flatMapBitVecBE (m : Nat) (v : Vector α n) (f : α → BitVec m) : BitVec (m * n) :=
+  match n with
+  | 0 => 0#0
+  | n + 1 => ((v.tail.flatMapBitVecBE m f).cast (by simp) : BitVec (m * n)) ++ f v.head
+
+/-- Flatten a vector of bitvectors of equal length to a single bitvector.
+The most significant bits are expected to be at the start of the vector. -/
+def Vector.flattenBitVecBE (m : Nat) (v : Vector (BitVec m) n) : BitVec (m * n) :=
+  v.flatMapBitVecBE m id

From de8a1fdc1c7684abc49963e4d68f0fb9ae9208c0 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Mon, 31 Mar 2025 13:50:51 +0200
Subject: [PATCH 3/9] prove flattenBitVecLE_splitLE

---
 src/Init/Data/BitVec/Basic.lean  | 10 ++------
 src/Init/Data/BitVec/Lemmas.lean | 39 ++++++++++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 8 deletions(-)

diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index 867dc2c0b34f..eeb975f9a111 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -725,18 +725,12 @@ def reverse : {w : Nat} → BitVec w → BitVec w
 /-- Split a bitvector into a vector of bitvectors of equal length where the vector ends on the
 most significant part. -/
 def splitBE (m n : Nat) (x : BitVec (m * n)) : Vector (BitVec m) n :=
-  let rec v n' := match n' with
-  | 0 => .emptyWithCapacity n
-  | n' + 1 => (v n').push (x.extractLsb' (m * n') m)
-  v n
+  (Vector.range n).map (fun i => x.extractLsb' (m * i) m)
 
 /-- Split a bitvector into a vector of bitvectors of equal length where the vector ends on the
 least significant part. -/
 def splitLE (m n : Nat) (x : BitVec (m * n)) : Vector (BitVec m) n :=
-  let rec v n' := match n' with
-  | 0 => .emptyWithCapacity n
-  | n' + 1 => (v n').push (x.extractLsb' (m * (n - n' - 1)) m)
-  v n
+  (Vector.range n).map (fun i => x.extractLsb' (m * (n - i - 1)) m)
 
 end BitVec
 
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index d80fc889377c..f02d4cb0575d 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -16,6 +16,7 @@ import Init.Data.Int.Bitwise.Lemmas
 import Init.Data.Int.LemmasAux
 import Init.Data.Int.Pow
 import Init.Data.Int.LemmasAux
+import Init.Data.Vector.Lemmas
 
 set_option linter.missingDocs true
 
@@ -5127,6 +5128,44 @@ theorem msb_replicate {n w : Nat} {x : BitVec w} :
   simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod]
   cases n <;> cases w <;> simp
 
+@[simp]
+theorem splitLE_pop : (splitLE m (n + 1) x).pop = splitLE m n (x.extractLsb' m _) := by
+  ext k hk i hi
+  simp at hk
+  have : m * (n - k - 1) + i < m * n := by
+    apply Nat.lt_of_lt_of_le (Nat.add_lt_add_left hi _)
+    rw [← Nat.mul_add_one]
+    apply Nat.mul_le_mul_left
+    omega
+  simp only [Nat.add_one_sub_one, splitLE, Vector.range, Vector.map_mk, Vector.pop_mk,
+    Vector.getElem_mk, Array.getElem_pop, Array.getElem_map, Array.getElem_range,
+    getElem_extractLsb', this, getLsbD_eq_getElem, ← Nat.add_assoc]
+  rw [Nat.sub_add_comm (Nat.le_of_lt hk), Nat.sub_add_comm (Nat.le_sub_of_add_le' hk)]
+  rw [Nat.mul_add m (n - k - 1), Nat.add_comm m]
+  simp
+
+@[simp]
+theorem splitLE_back : (splitLE m (n + 1) x).back = x.extractLsb' 0 m := by
+  ext i hi
+  simp [splitLE, Vector.back, Vector.range, Nat.add_sub_cancel_left]
+
+@[simp]
+theorem flattenBitVecLE_splitLE {m n : Nat} {x : BitVec (m * n)} :
+    (x.splitLE m n).flattenBitVecLE m = x := by
+  induction n with
+  | zero =>
+    simp [splitLE, Vector.flattenBitVecLE, Vector.flatMapBitVecLE, of_length_zero]
+  | succ n ih =>
+    simp only [Vector.flattenBitVecLE, Vector.flatMapBitVecLE, Nat.add_one_sub_one, splitLE_pop,
+      cast_eq, splitLE_back, id_eq] at ih ⊢
+    rw [ih]
+    ext i hi
+    by_cases hi' : i < m
+    · simp [getElem_append, hi']
+      rfl
+    · simp [getElem_append, hi', Nat.add_sub_of_le (Nat.le_of_not_lt hi')]
+      rfl
+
 /-! ### Decidable quantifiers -/
 
 theorem forall_zero_iff {P : BitVec 0 → Prop} :

From f54923de7889ea4cf371d0ef249c9bfa8951c7ab Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Tue, 1 Apr 2025 08:59:39 +0200
Subject: [PATCH 4/9] address @bollu's suggestions

Co-authored-by: Siddharth <siddu.druid@gmail.com>
---
 src/Init/Data/BitVec/Basic.lean  | 4 ++--
 src/Init/Data/BitVec/Lemmas.lean | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index c0ec0d99f62d..a7a40deea361 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -764,12 +764,12 @@ def reverse : {w : Nat} → BitVec w → BitVec w
 /- ### vectors of bitvectors -/
 
 /-- Split a bitvector into a vector of bitvectors of equal length where the vector ends on the
-most significant part. -/
+most significant part ('BE' for 'big endian'). See also `BitVec.splitLE`. -/
 def splitBE (m n : Nat) (x : BitVec (m * n)) : Vector (BitVec m) n :=
   (Vector.range n).map (fun i => x.extractLsb' (m * i) m)
 
 /-- Split a bitvector into a vector of bitvectors of equal length where the vector ends on the
-least significant part. -/
+least significant part ('LE' for 'little endian'). See also `BitVec.splitGE`. -/
 def splitLE (m n : Nat) (x : BitVec (m * n)) : Vector (BitVec m) n :=
   (Vector.range n).map (fun i => x.extractLsb' (m * (n - i - 1)) m)
 
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index f02d4cb0575d..6c7eb470c07f 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -5140,8 +5140,8 @@ theorem splitLE_pop : (splitLE m (n + 1) x).pop = splitLE m n (x.extractLsb' m _
   simp only [Nat.add_one_sub_one, splitLE, Vector.range, Vector.map_mk, Vector.pop_mk,
     Vector.getElem_mk, Array.getElem_pop, Array.getElem_map, Array.getElem_range,
     getElem_extractLsb', this, getLsbD_eq_getElem, ← Nat.add_assoc]
-  rw [Nat.sub_add_comm (Nat.le_of_lt hk), Nat.sub_add_comm (Nat.le_sub_of_add_le' hk)]
-  rw [Nat.mul_add m (n - k - 1), Nat.add_comm m]
+  rw [Nat.sub_add_comm (Nat.le_of_lt hk), Nat.sub_add_comm (Nat.le_sub_of_add_le' hk),
+    Nat.mul_add m (n - k - 1), Nat.add_comm m]
   simp
 
 @[simp]

From decb724acddc45e9ab589f7ab3ef43cd7254267b Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Tue, 1 Apr 2025 10:26:24 +0200
Subject: [PATCH 5/9] getElem_flattenBitVecLE and getElem_splitLE

---
 src/Init/Data/BitVec/Basic.lean  |  2 +-
 src/Init/Data/BitVec/Lemmas.lean | 39 +++++++++++++++++++++++++-------
 2 files changed, 32 insertions(+), 9 deletions(-)

diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index a7a40deea361..e888a2251b64 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -769,7 +769,7 @@ def splitBE (m n : Nat) (x : BitVec (m * n)) : Vector (BitVec m) n :=
   (Vector.range n).map (fun i => x.extractLsb' (m * i) m)
 
 /-- Split a bitvector into a vector of bitvectors of equal length where the vector ends on the
-least significant part ('LE' for 'little endian'). See also `BitVec.splitGE`. -/
+least significant part ('LE' for 'little endian'). See also `BitVec.splitBE`. -/
 def splitLE (m n : Nat) (x : BitVec (m * n)) : Vector (BitVec m) n :=
   (Vector.range n).map (fun i => x.extractLsb' (m * (n - i - 1)) m)
 
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 6c7eb470c07f..3af86ee36928 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -5128,8 +5128,10 @@ theorem msb_replicate {n w : Nat} {x : BitVec w} :
   simp only [BitVec.msb, getMsbD_replicate, Nat.zero_mod]
   cases n <;> cases w <;> simp
 
+/-! ### Vectors of bitvectors -/
+
 @[simp]
-theorem splitLE_pop : (splitLE m (n + 1) x).pop = splitLE m n (x.extractLsb' m _) := by
+theorem pop_splitLE : (splitLE m (n + 1) x).pop = splitLE m n (x.extractLsb' m _) := by
   ext k hk i hi
   simp at hk
   have : m * (n - k - 1) + i < m * n := by
@@ -5145,7 +5147,7 @@ theorem splitLE_pop : (splitLE m (n + 1) x).pop = splitLE m n (x.extractLsb' m _
   simp
 
 @[simp]
-theorem splitLE_back : (splitLE m (n + 1) x).back = x.extractLsb' 0 m := by
+theorem back_splitLE : (splitLE m (n + 1) x).back = x.extractLsb' 0 m := by
   ext i hi
   simp [splitLE, Vector.back, Vector.range, Nat.add_sub_cancel_left]
 
@@ -5156,15 +5158,36 @@ theorem flattenBitVecLE_splitLE {m n : Nat} {x : BitVec (m * n)} :
   | zero =>
     simp [splitLE, Vector.flattenBitVecLE, Vector.flatMapBitVecLE, of_length_zero]
   | succ n ih =>
-    simp only [Vector.flattenBitVecLE, Vector.flatMapBitVecLE, Nat.add_one_sub_one, splitLE_pop,
-      cast_eq, splitLE_back, id_eq] at ih ⊢
+    simp only [Vector.flattenBitVecLE, Vector.flatMapBitVecLE, Nat.add_one_sub_one, pop_splitLE,
+      cast_eq, back_splitLE, id_eq] at ih ⊢
     rw [ih]
     ext i hi
     by_cases hi' : i < m
-    · simp [getElem_append, hi']
-      rfl
-    · simp [getElem_append, hi', Nat.add_sub_of_le (Nat.le_of_not_lt hi')]
-      rfl
+    · simp [getElem_append, hi', BitVec.getLsbD_eq_getElem hi]
+    · simp [getElem_append, hi', Nat.add_sub_of_le (Nat.le_of_not_lt hi'),
+        BitVec.getLsbD_eq_getElem hi]
+
+theorem getElem_flattenBitVecLE {m n : Nat} [NeZero m] (v : Vector (BitVec m) n) (i : Nat)
+    (hi : i < m * n) :
+    (v.flattenBitVecLE m)[i] =
+      (v[n - (i / m + 1)]'(Nat.sub_lt (n.pos_of_ne_zero fun hn => by subst hn; omega) (i / m).zero_lt_succ))[i % m]'(Nat.mod_lt _ m.pos_of_neZero) := by
+  induction n generalizing i with
+  | zero =>
+    simp at hi
+  | succ n ih =>
+    simp only [Vector.flattenBitVecLE, Vector.flatMapBitVecLE, Nat.add_one_sub_one, cast_eq, id_eq]
+    rw [Nat.mul_add, Nat.mul_one] at hi
+    apply (BitVec.getElem_append hi).trans
+    by_cases hi' : i < m
+    · simp [hi', Vector.back, Nat.mod_eq_of_lt hi', Nat.div_eq_of_lt hi']
+    · simp only [Vector.flattenBitVecLE] at ih
+      simp only [hi', ↓reduceDIte, ih v.pop (i - m) (by omega)]
+      simp [Vector.pop, ← Nat.mod_eq_sub_mod (Nat.ge_of_not_lt hi'),
+        ← Nat.div_eq_sub_div m.pos_of_neZero (Nat.ge_of_not_lt hi')]
+
+theorem getElem_splitLE {i : Nat} (hi : i < n) (x : BitVec (m * n)) :
+    (x.splitLE m n)[i] = x.extractLsb' (m * (n - i - 1)) m := by
+  simp [splitLE, Vector.range]
 
 /-! ### Decidable quantifiers -/
 

From 8e78bed392c06f95cdeb814dfa910b9e483593c6 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Tue, 1 Apr 2025 10:47:28 +0200
Subject: [PATCH 6/9] splitLE_flattenBitVecLE

---
 src/Init/Data/BitVec/Lemmas.lean | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 3af86ee36928..718d69fc9f8c 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -5170,7 +5170,8 @@ theorem flattenBitVecLE_splitLE {m n : Nat} {x : BitVec (m * n)} :
 theorem getElem_flattenBitVecLE {m n : Nat} [NeZero m] (v : Vector (BitVec m) n) (i : Nat)
     (hi : i < m * n) :
     (v.flattenBitVecLE m)[i] =
-      (v[n - (i / m + 1)]'(Nat.sub_lt (n.pos_of_ne_zero fun hn => by subst hn; omega) (i / m).zero_lt_succ))[i % m]'(Nat.mod_lt _ m.pos_of_neZero) := by
+      (v[n - (i / m + 1)]'(Nat.sub_lt (n.pos_of_ne_zero fun hn =>
+        by subst hn; omega) (i / m).zero_lt_succ))[i % m]'(Nat.mod_lt _ m.pos_of_neZero) := by
   induction n generalizing i with
   | zero =>
     simp at hi
@@ -5189,6 +5190,22 @@ theorem getElem_splitLE {i : Nat} (hi : i < n) (x : BitVec (m * n)) :
     (x.splitLE m n)[i] = x.extractLsb' (m * (n - i - 1)) m := by
   simp [splitLE, Vector.range]
 
+@[simp]
+theorem splitLE_flattenBitVecLE {m n : Nat} [NeZero m] {v : Vector (BitVec m) n} :
+    (v.flattenBitVecLE m).splitLE m n = v := by
+  ext i hi j hj
+  have : m * (n - i - 1) + j < m * n := by
+    apply Nat.lt_of_lt_of_le (Nat.add_lt_add_left hj _)
+    rw [← Nat.mul_add_one]
+    apply Nat.mul_le_mul_left
+    omega
+  simp only [getElem_splitLE, getElem_extractLsb', getLsbD_eq_getElem this, getElem_flattenBitVecLE,
+    Nat.mul_add_mod_self_left, Nat.mod_eq_of_lt hj]
+  simp [Nat.add_div m.pos_of_neZero, Nat.div_eq_of_lt hj, Nat.mul_div_cancel_left _ m.pos_of_neZero,
+    Nat.not_le_of_gt (m := j % m) (n := m) (Nat.mod_lt_of_lt hj)]
+  congr
+  omega
+
 /-! ### Decidable quantifiers -/
 
 theorem forall_zero_iff {P : BitVec 0 → Prop} :

From 59656ad705a846618f5a3287dc4e185482e28698 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Tue, 1 Apr 2025 11:43:20 +0200
Subject: [PATCH 7/9] address @bollu's suggestions

---
 src/Init/Data/BitVec/Lemmas.lean | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 718d69fc9f8c..4dc9c2e285ee 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -5167,31 +5167,32 @@ theorem flattenBitVecLE_splitLE {m n : Nat} {x : BitVec (m * n)} :
     · simp [getElem_append, hi', Nat.add_sub_of_le (Nat.le_of_not_lt hi'),
         BitVec.getLsbD_eq_getElem hi]
 
-theorem getElem_flattenBitVecLE {m n : Nat} [NeZero m] (v : Vector (BitVec m) n) (i : Nat)
+theorem getElem_flattenBitVecLE {m n : Nat} (v : Vector (BitVec m) n) (i : Nat)
     (hi : i < m * n) :
     (v.flattenBitVecLE m)[i] =
-      (v[n - (i / m + 1)]'(Nat.sub_lt (n.pos_of_ne_zero fun hn =>
-        by subst hn; omega) (i / m).zero_lt_succ))[i % m]'(Nat.mod_lt _ m.pos_of_neZero) := by
+      (v[n - (i / m + 1)]'(Nat.sub_lt (Nat.pos_of_lt_mul_left hi) (i / m).zero_lt_succ))[i % m]'
+        (Nat.mod_lt i (Nat.pos_of_lt_mul_right hi)) := by
   induction n generalizing i with
   | zero =>
     simp at hi
   | succ n ih =>
     simp only [Vector.flattenBitVecLE, Vector.flatMapBitVecLE, Nat.add_one_sub_one, cast_eq, id_eq]
+    have hi' := hi
     rw [Nat.mul_add, Nat.mul_one] at hi
     apply (BitVec.getElem_append hi).trans
-    by_cases hi' : i < m
-    · simp [hi', Vector.back, Nat.mod_eq_of_lt hi', Nat.div_eq_of_lt hi']
+    by_cases him : i < m
+    · simp [him, Vector.back, Nat.mod_eq_of_lt him, Nat.div_eq_of_lt him]
     · simp only [Vector.flattenBitVecLE] at ih
-      simp only [hi', ↓reduceDIte, ih v.pop (i - m) (by omega)]
-      simp [Vector.pop, ← Nat.mod_eq_sub_mod (Nat.ge_of_not_lt hi'),
-        ← Nat.div_eq_sub_div m.pos_of_neZero (Nat.ge_of_not_lt hi')]
+      simp only [him, ↓reduceDIte, ih v.pop (i - m) (by omega)]
+      simp [Vector.pop, ← Nat.mod_eq_sub_mod (Nat.ge_of_not_lt him),
+        ← Nat.div_eq_sub_div (Nat.pos_of_lt_mul_right hi') (Nat.ge_of_not_lt him)]
 
 theorem getElem_splitLE {i : Nat} (hi : i < n) (x : BitVec (m * n)) :
     (x.splitLE m n)[i] = x.extractLsb' (m * (n - i - 1)) m := by
   simp [splitLE, Vector.range]
 
 @[simp]
-theorem splitLE_flattenBitVecLE {m n : Nat} [NeZero m] {v : Vector (BitVec m) n} :
+theorem splitLE_flattenBitVecLE {m n : Nat} {v : Vector (BitVec m) n} :
     (v.flattenBitVecLE m).splitLE m n = v := by
   ext i hi j hj
   have : m * (n - i - 1) + j < m * n := by
@@ -5201,7 +5202,8 @@ theorem splitLE_flattenBitVecLE {m n : Nat} [NeZero m] {v : Vector (BitVec m) n}
     omega
   simp only [getElem_splitLE, getElem_extractLsb', getLsbD_eq_getElem this, getElem_flattenBitVecLE,
     Nat.mul_add_mod_self_left, Nat.mod_eq_of_lt hj]
-  simp [Nat.add_div m.pos_of_neZero, Nat.div_eq_of_lt hj, Nat.mul_div_cancel_left _ m.pos_of_neZero,
+  simp [Nat.add_div (Nat.pos_of_lt_mul_right this), Nat.div_eq_of_lt hj,
+    Nat.mul_div_cancel_left _ (Nat.pos_of_lt_mul_right this),
     Nat.not_le_of_gt (m := j % m) (n := m) (Nat.mod_lt_of_lt hj)]
   congr
   omega

From 95017a7da78830841875c792457737033c136c37 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Tue, 1 Apr 2025 11:46:49 +0200
Subject: [PATCH 8/9] argument implicitness

---
 src/Init/Data/BitVec/Lemmas.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 4dc9c2e285ee..dbe089776c63 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -5167,8 +5167,7 @@ theorem flattenBitVecLE_splitLE {m n : Nat} {x : BitVec (m * n)} :
     · simp [getElem_append, hi', Nat.add_sub_of_le (Nat.le_of_not_lt hi'),
         BitVec.getLsbD_eq_getElem hi]
 
-theorem getElem_flattenBitVecLE {m n : Nat} (v : Vector (BitVec m) n) (i : Nat)
-    (hi : i < m * n) :
+theorem getElem_flattenBitVecLE {m n : Nat} (v : Vector (BitVec m) n) {i : Nat} (hi : i < m * n) :
     (v.flattenBitVecLE m)[i] =
       (v[n - (i / m + 1)]'(Nat.sub_lt (Nat.pos_of_lt_mul_left hi) (i / m).zero_lt_succ))[i % m]'
         (Nat.mod_lt i (Nat.pos_of_lt_mul_right hi)) := by
@@ -5183,11 +5182,11 @@ theorem getElem_flattenBitVecLE {m n : Nat} (v : Vector (BitVec m) n) (i : Nat)
     by_cases him : i < m
     · simp [him, Vector.back, Nat.mod_eq_of_lt him, Nat.div_eq_of_lt him]
     · simp only [Vector.flattenBitVecLE] at ih
-      simp only [him, ↓reduceDIte, ih v.pop (i - m) (by omega)]
+      simp only [him, ↓reduceDIte, ih v.pop (i := i - m) (by omega)]
       simp [Vector.pop, ← Nat.mod_eq_sub_mod (Nat.ge_of_not_lt him),
         ← Nat.div_eq_sub_div (Nat.pos_of_lt_mul_right hi') (Nat.ge_of_not_lt him)]
 
-theorem getElem_splitLE {i : Nat} (hi : i < n) (x : BitVec (m * n)) :
+theorem getElem_splitLE {i : Nat} (x : BitVec (m * n)) (hi : i < n) :
     (x.splitLE m n)[i] = x.extractLsb' (m * (n - i - 1)) m := by
   simp [splitLE, Vector.range]
 

From 033b801947b36acfdb9828eddc922575a76f50af Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Wed, 2 Apr 2025 09:56:19 +0200
Subject: [PATCH 9/9] address @bollu's suggestions

Co-authored-by: Siddharth <siddu.druid@gmail.com>
---
 src/Init/Data/BitVec/Lemmas.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index dbe089776c63..7ccbc08c1b27 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -5201,9 +5201,10 @@ theorem splitLE_flattenBitVecLE {m n : Nat} {v : Vector (BitVec m) n} :
     omega
   simp only [getElem_splitLE, getElem_extractLsb', getLsbD_eq_getElem this, getElem_flattenBitVecLE,
     Nat.mul_add_mod_self_left, Nat.mod_eq_of_lt hj]
-  simp [Nat.add_div (Nat.pos_of_lt_mul_right this), Nat.div_eq_of_lt hj,
-    Nat.mul_div_cancel_left _ (Nat.pos_of_lt_mul_right this),
-    Nat.not_le_of_gt (m := j % m) (n := m) (Nat.mod_lt_of_lt hj)]
+  simp only [Nat.add_div (Nat.pos_of_lt_mul_right this),
+    Nat.mul_div_cancel_left _ (Nat.pos_of_lt_mul_right this), Nat.div_eq_of_lt hj, Nat.add_zero,
+    Nat.mul_mod_right, Nat.zero_add, Nat.not_le_of_gt (m := j % m) (n := m) (Nat.mod_lt_of_lt hj),
+    ↓reduceIte]
   congr
   omega