diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
index a4d78ede..72fffeab 100644
--- a/Arm/BitVec.lean
+++ b/Arm/BitVec.lean
@@ -294,7 +294,7 @@ abbrev partInstall (hi lo : Nat) (val : BitVec (hi - lo + 1)) (x : BitVec n): Bi
   let x_with_hole := x &&& mask_with_hole
   x_with_hole ||| val_aligned
 
-example : (partInstall 3 0 0xC#4 0xAB0D#16 = 0xAB0C#16) := by native_decide
+example : (partInstall 3 0 0xC#4 0xAB0D#16 = 0xAB0C#16) := rfl
 
 def flattenTR {n : Nat} (xs : List (BitVec n)) (i : Nat)
   (acc : BitVec len) (H : n > 0) : BitVec len :=
@@ -308,37 +308,30 @@ def flattenTR {n : Nat} (xs : List (BitVec n)) (i : Nat)
 /-- Reverse bits of a bit-vector. -/
 def reverse (x : BitVec n) : BitVec n :=
   let rec reverseTR (x : BitVec n) (i : Nat) (acc : BitVec n) :=
-    if i < n then
-      let xi := extractLsb i i x
-      have h : i - i + 1 = (n - i - 1) - (n - i - 1) + 1 := by omega
-      let acc := BitVec.partInstall (n - i - 1) (n - i - 1) (BitVec.cast h xi) acc
-      reverseTR x (i + 1) acc
-    else acc
-  reverseTR x 0 $ BitVec.zero n
-
-example : reverse 0b11101#5 = 0b10111#5 := by
-  -- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
-  simp [reverse, reverse.reverseTR]
-  rfl
+    match i with
+    | 0 => acc
+    | j + 1 =>
+      let xi : BitVec 1 := extractLsb' (i - 1) 1 x
+      let acc := BitVec.partInstall (n - i) (n - i) (xi.cast (by omega)) acc
+      reverseTR x j acc
+  reverseTR x n $ BitVec.zero n
+
+example : reverse 0b11101#5 = 0b10111#5 := rfl
 
 /-- Split a bit-vector into sub vectors of size e. -/
 def split (x : BitVec n) (e : Nat) (h : 0 < e): List (BitVec e) :=
   let rec splitTR (x : BitVec n) (e : Nat) (h : 0 < e)
     (i : Nat) (acc : List (BitVec e)) : List (BitVec e) :=
-    if i < n/e then
-      let lo := i * e
-      let hi := lo + e - 1
-      have h₀ : hi - lo + 1 = e := by simp only [hi, lo]; omega
-      let part : BitVec e := BitVec.cast h₀ (extractLsb hi lo x)
+    match i with
+    | 0 => acc
+    | j + 1 =>
+      let lo := (n / e - i) * e
+      let part : BitVec e := extractLsb' lo e x
       let newacc := part :: acc
-      splitTR x e h (i + 1) newacc
-    else acc
-  splitTR x e h 0 []
+      splitTR x e h j newacc
+  splitTR x e h (n / e) []
 
-example : split 0xabcd1234#32 8 (by omega) = [0xab#8, 0xcd#8, 0x12#8, 0x34#8] :=
-  by
-  -- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
-  simp [split, split.splitTR]
+example : split 0xabcd1234#32 8 (by omega) = [0xab#8, 0xcd#8, 0x12#8, 0x34#8] := rfl
 
 /-- Reverse a list of bit vectors and flatten the list. -/
 def revflat (x : List (BitVec n)) : BitVec (n * x.length) :=
@@ -398,10 +391,10 @@ theorem bitvec_zero_is_unique (x : BitVec 0) :
   simp only [Nat.pow_zero, Fin.fin_one_eq_zero, Nat.le_refl]
 
 theorem fin_bitvec_add (x y : BitVec n) :
-  (x.toFin + y.toFin) = (x + y).toFin := by rfl
+  (x.toFin + y.toFin) = (x + y).toFin := rfl
 
 theorem fin_bitvec_sub (x y : BitVec n) :
-  (x.toFin - y.toFin) = (x - y).toFin := by rfl
+  (x.toFin - y.toFin) = (x - y).toFin := rfl
 
 theorem fin_bitvec_or (x y : BitVec n) :
   (x ||| y).toFin = (x.toFin ||| y.toFin) := by
diff --git a/Arm/Decode.lean b/Arm/Decode.lean
index 5bdc491f..36578c0b 100644
--- a/Arm/Decode.lean
+++ b/Arm/Decode.lean
@@ -172,156 +172,135 @@ def decode_raw_inst (i : BitVec 32) : Option ArmInst :=
 example : decode_raw_inst 0x91000421#32 =
           (ArmInst.DPI (DataProcImmInst.Add_sub_imm
           {sf := 1#1, op := 0#1, S := 0#1, sh := 0#1,
-            imm12 := 1#12, Rn := 1#5, Rd := 1#5})) := by
-        rfl
+            imm12 := 1#12, Rn := 1#5, Rd := 1#5})) := rfl
 
 -- adc x1, x1, x0
 example : decode_raw_inst 0b00011010000000000000000000100001#32 =
           (ArmInst.DPR (DataProcRegInst.Add_sub_carry
                { sf := 0#1, op := 0#1, S := 0#1, Rm := 0#5,
-                 Rn := 1#5, Rd := 1#5 })) := by
-        rfl
+                 Rn := 1#5, Rd := 1#5 })) := rfl
 
 -- sha512h q3, q5, v6.2d
 example : decode_raw_inst 0xce6680a3#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_three_reg_sha512
                { Rm := 6#5, O := 0#1, opcode := 0#2,
-                 Rn := 5#5, Rd := 3#5 })) := by
-        rfl
+                 Rn := 5#5, Rd := 3#5 })) := rfl
 
 -- sha512h2 q3, q1, v0.2d
 example : decode_raw_inst 0xce608423#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_three_reg_sha512
                { Rm := 0#5, O := 0#1, opcode := 1#2,
-                 Rn := 1#5, Rd := 3#5 })) := by
-        rfl
+                 Rn := 1#5, Rd := 3#5 })) := rfl
 
 -- sha512su1 v16.2d, v23.2d, v7.2d
 example : decode_raw_inst 0xce678af0#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_three_reg_sha512
           { Rm := 7#5, O := 0#1, opcode := 2#2,
-            Rn := 23#5, Rd := 16#5 })) := by
-        rfl
+            Rn := 23#5, Rd := 16#5 })) := rfl
 
 -- sha512su0 v16.2d, v17.2d
 example : decode_raw_inst 0xcec08230#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_two_reg_sha512
-               { opcode := 0#2, Rn := 17#5, Rd := 16#5 })) := by
-        rfl
+               { opcode := 0#2, Rn := 17#5, Rd := 16#5 })) := rfl
 
 -- ldr	q16, [x0], #16
 example : decode_raw_inst 0x3cc10410#32 =
           (ArmInst.LDST (LDSTInst.Reg_imm_post_indexed
                { size := 0x0#2, V := 0x1#1, opc := 0x3#2, imm9 := 0x010#9,
-                 Rn := 0x00#5, Rt := 0x10#5 })) := by
-        rfl
+                 Rn := 0x00#5, Rt := 0x10#5 })) := rfl
 
 -- stp	x29, x30, [sp, #-16]!
 example : decode_raw_inst 0xa9bf7bfd#32 =
           (ArmInst.LDST (LDSTInst.Reg_pair_pre_indexed
                { opc := 0x2#2, V := 0x0#1, L := 0x0#1, imm7 := 0x7e#7,
-                 Rt2 := 0x1e#5, Rn := 0x1f#5, Rt := 0x1d#5 })) := by
-        rfl
+                 Rt2 := 0x1e#5, Rn := 0x1f#5, Rt := 0x1d#5 })) := rfl
 
 -- ld1	{v16.16b-v19.16b}, [x1], #64
 example : decode_raw_inst 0x4cdf2030#32 =
           (ArmInst.LDST
                (LDSTInst.Advanced_simd_multiple_struct_post_indexed
                  { Q := 0x1#1, L := 0x1#1, Rm := 0x1f#5, opcode := 0x2#4,
-                   size := 0x0#2, Rn := 0x01#5, Rt := 0x10#5 })) := by
-        rfl
+                   size := 0x0#2, Rn := 0x01#5, Rt := 0x10#5 })) := rfl
 
 -- ld1	{v24.2d}, [x3], #16
 example : decode_raw_inst 0x4cdf7c78#32 =
           (ArmInst.LDST
                (LDSTInst.Advanced_simd_multiple_struct_post_indexed
                  { Q := 0x1#1, L := 0x1#1, Rm := 0x1f#5, opcode := 0x7#4,
-                   size := 0x3#2, Rn := 0x03#5, Rt := 0x18#5 })) := by
-        rfl
+                   size := 0x3#2, Rn := 0x03#5, Rt := 0x18#5 })) := rfl
 
 -- ld1	{v0.2d-v3.2d}, [x0]
 example : decode_raw_inst 0x4c402c00#32 =
           (ArmInst.LDST
           (LDSTInst.Advanced_simd_multiple_struct
             { Q := 0x1#1, L := 0x1#1, opcode := 0x2#4,
-              size := 0x3#2, Rn := 0x00#5, Rt := 0x00#5 })) := by
-        rfl
+              size := 0x3#2, Rn := 0x00#5, Rt := 0x00#5 })) := rfl
 
 -- st1	{v0.2d-v3.2d}, [x0]
 example :  decode_raw_inst 0x4c002c00#32 =
            (ArmInst.LDST
                 (LDSTInst.Advanced_simd_multiple_struct
                   { Q := 0x1#1, L := 0x0#1, opcode := 0x2#4, size := 0x3#2,
-                    Rn := 0x00#5, Rt := 0x00#5 })) := by rfl
+                    Rn := 0x00#5, Rt := 0x00#5 })) := rfl
 
 -- add	v24.2d, v24.2d, v16.2d
 example : decode_raw_inst 0x4ef08718#32 =
   (ArmInst.DPSFP (DataProcSFPInst.Advanced_simd_three_same
        { Q := 0x1#1, U := 0x0#1, size := 0x3#2, Rm := 0x10#5,
-         opcode := 0x10#5, Rn := 0x18#5, Rd := 0x18#5 })) := by
-  rfl
+         opcode := 0x10#5, Rn := 0x18#5, Rd := 0x18#5 })) := rfl
 
 -- adrp x3, ...
 example : decode_raw_inst 0xd0000463#32 =
           (ArmInst.DPI (DataProcImmInst.PC_rel_addressing
                { op := 0x1#1, immlo := 0x2#2, immhi := 0x00023#19,
-                 Rd := 0x03#5 })) := by
-        rfl
+                 Rd := 0x03#5 })) := rfl
 
 -- csel	x1, x1, x4, ne
 example : decode_raw_inst 0x9a841021#32 =
           (ArmInst.DPR (DataProcRegInst.Conditional_select
                { sf := 0x1#1, op := 0x0#1, S := 0x0#1, Rm := 0x04#5,
                  cond := 0x1#4, op2 := 0x0#2, Rn := 0x01#5,
-                 Rd := 0x01#5 })) := by
-        rfl
+                 Rd := 0x01#5 })) := rfl
 
 -- b ...
 example : decode_raw_inst 0x14000001#32 =
           (ArmInst.BR (BranchInst.Uncond_branch_imm
-               { op := 0x0#1, imm26 := 0x0000001#26 })) := by
-        rfl
+               { op := 0x0#1, imm26 := 0x0000001#26 })) := rfl
 
 -- b.le ...
 example : decode_raw_inst 0x5400000d#32 =
           (ArmInst.BR (BranchInst.Cond_branch_imm
-               { imm19 := 0x00000#19, o0 := 0, cond := 0xd#4})) := by
-        rfl
+               { imm19 := 0x00000#19, o0 := 0, cond := 0xd#4})) := rfl
 
 -- ret
 example : decode_raw_inst 0xd65f03c0#32 =
           (ArmInst.BR (BranchInst.Uncond_branch_reg
                { opc := 0x2#4, op2 := 0x1f#5, op3 := 0x00#6,
-                 Rn := 0x1e#5, op4 := 0x00#5 })) := by
-        rfl
+                 Rn := 0x1e#5, op4 := 0x00#5 })) := rfl
 
 -- cbnz	x2, ...
 example : decode_raw_inst 0xb5ffc382#32 =
           (ArmInst.BR (BranchInst.Compare_branch
                { sf := 0x1#1, op := 0x1#1, imm19 := 0x7fe1c#19,
-                 Rt := 0x02#5 })) := by
-        rfl
+                 Rt := 0x02#5 })) := rfl
 
 -- ext	v24.16b, v24.16b, v24.16b, #8
 example : decode_raw_inst 0x6e184318#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Advanced_simd_extract
                { Q := 0x1#1, op2 := 0x0#2, Rm := 0x18#5, imm4 := 0x8#4,
-                 Rn := 0x18#5, Rd := 0x18#5 })) := by
-        rfl
+                 Rn := 0x18#5, Rd := 0x18#5 })) := rfl
 
 -- mov	x29, sp
 example : decode_raw_inst 0x910003fd#32 =
           (ArmInst.DPI (DataProcImmInst.Add_sub_imm
                { sf := 0x1#1, op := 0x0#1, S := 0x0#1, sh := 0x0#1,
-                 imm12 := 0x000#12, Rn := 0x1f#5, Rd := 0x1d#5 })) := by
-        rfl
+                 imm12 := 0x000#12, Rn := 0x1f#5, Rd := 0x1d#5 })) := rfl
 
 -- ldr	q0, [x4]
 example : decode_raw_inst 0x3dc00080#32 =
           (ArmInst.LDST (LDSTInst.Reg_unsigned_imm
                { size := 0x0#2, V := 0x1#1, opc := 0x3#2,
-                 imm12 := 0x000#12, Rn := 0x04#5, Rt := 0x00#5 })) := by
-        rfl
+                 imm12 := 0x000#12, Rn := 0x04#5, Rt := 0x00#5 })) := rfl
 
 -- str	q4, [x2], #16
 example : decode_raw_inst 0x3c810444#32 =
@@ -335,29 +314,25 @@ example : decode_raw_inst 0x4e200800#32 =
           (ArmInst.DPSFP
                (DataProcSFPInst.Advanced_simd_two_reg_misc
                  { Q := 0x1#1, U := 0x0#1, size := 0x0#2, opcode := 0x00#5,
-                   Rn := 0x00#5, Rd := 0x00#5 })) := by
-        rfl
+                   Rn := 0x00#5, Rd := 0x00#5 })) := rfl
 
 -- aese	v0.16b, v16.16b
 example : decode_raw_inst 0x4e284a00#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_aes
                { size := 0x0#2, opcode := 0x04#5,
-                 Rn := 0x10#5, Rd := 0x00#5 })) := by
-        rfl
+                 Rn := 0x10#5, Rd := 0x00#5 })) := rfl
 
 -- aesmc v0.16b, v0.16b
 example : decode_raw_inst 0x4e286800#32 =
           (ArmInst.DPSFP (DataProcSFPInst.Crypto_aes
                { size := 0x0#2, opcode := 0x06#5,
-                 Rn := 0x00#5, Rd := 0x00#5 })) := by
-        rfl
+                 Rn := 0x00#5, Rd := 0x00#5 })) := rfl
 
 -- mov	x28, v0.d[0]
 example : decode_raw_inst 0x4e083c1c#32 =
           ArmInst.DPSFP (DataProcSFPInst.Advanced_simd_copy
               { Q := 0x1#1, op := 0x0#1, imm5 := 0x08#5,
-                imm4 := 0x7#4, Rn := 0x00#5, Rd := 0x1c#5 }) := by
-        rfl
+                imm4 := 0x7#4, Rn := 0x00#5, Rd := 0x1c#5 }) := rfl
 
 -- ext v16.8B, v10.8B, v24.8B, #2
 example : decode_raw_inst 0x2e181150#32 =
@@ -368,8 +343,7 @@ example : decode_raw_inst 0x2e181150#32 =
               Rm := 0x18#5,
               imm4 := 0x2#4,
               Rn := 0x0a#5,
-              Rd := 0x10#5 })) := by
-        rfl
+              Rd := 0x10#5 })) := rfl
 
 -- lsr w0, w0, #1
 example : decode_raw_inst 0x53017c00#32 =
@@ -382,8 +356,7 @@ example : decode_raw_inst 0x53017c00#32 =
                 immr := 0x01#6,
                 imms := 0x1f#6,
                 Rn := 0x00#5,
-                Rd := 0x00#5 })) := by
-        rfl
+                Rd := 0x00#5 })) := rfl
 
 -- ands x30, x3, x17, asr #35
 example : decode_raw_inst 0xea918c7e#32 =
@@ -396,8 +369,7 @@ example : decode_raw_inst 0xea918c7e#32 =
             Rm := 0x11#5,
             imm6 := 0x23#6,
             Rn := 0x03#5,
-            Rd := 0x1e#5})) := by
-        rfl
+            Rd := 0x1e#5})) := rfl
 
 -- eor x15, x28, #0xffffc00000000001
 example : decode_raw_inst 0xd2524b8f#32 =
@@ -409,8 +381,7 @@ example : decode_raw_inst 0xd2524b8f#32 =
             immr := 0x12#6,
             imms := 0x12#6,
             Rn := 0x1c#5,
-            Rd := 0x0f#5 })) := by
-        rfl
+            Rd := 0x0f#5 })) := rfl
 
 -- sub x9, x27, x15, lsl #55
 example : decode_raw_inst 0xcb0fdf69 =
@@ -424,8 +395,7 @@ example : decode_raw_inst 0xcb0fdf69 =
             Rm := 0x0f#5,
             imm6 := 0x37#6,
             Rn := 0x1b#5,
-            Rd := 0x09#5 })) := by
-        rfl
+            Rd := 0x09#5 })) := rfl
 
 -- orr v5.8h, #0x77, lsl #8
 example : decode_raw_inst 0x4f03b6e5 =
@@ -446,8 +416,7 @@ example : decode_raw_inst 0x4f03b6e5 =
             f := 0x1#1,
             g := 0x1#1,
             h := 0x1#1,
-            Rd := 0x05#5 })) := by
-        rfl
+            Rd := 0x05#5 })) := rfl
 
 -- mov v10.h[0] v17.h[6]
 example : decode_raw_inst 0x6e026e2a =
@@ -462,8 +431,7 @@ example : decode_raw_inst 0x6e026e2a =
             imm4 := 0xd#4,
             _fixed4 := 0x1#1,
             Rn := 0x11#5,
-            Rd := 0x0a#5 })) := by
-          rfl
+            Rd := 0x0a#5 })) := rfl
 
 -- fmov v25.d[1], x5
 example : decode_raw_inst 0x9eaf00b9 =
@@ -479,8 +447,7 @@ example : decode_raw_inst 0x9eaf00b9 =
               opcode := 0x7#3,
               _fixed4 := 0x00#6,
               Rn := 0x05#5,
-              Rd := 0x19#5 })) := by
-            rfl
+              Rd := 0x19#5 })) := rfl
 
 -- rev x0, x25
 example : decode_raw_inst 0xdac00f20 =
@@ -493,10 +460,9 @@ example : decode_raw_inst 0xdac00f20 =
               opcode2 := 0x00#5,
               opcode := 0x03#6,
               Rn := 0x19#5,
-              Rd := 0x00#5 })) := by
-          rfl
+              Rd := 0x00#5 })) := rfl
 
 -- Unimplemented
-example : decode_raw_inst 0x00000000#32 = none := by rfl
+example : decode_raw_inst 0x00000000#32 = none := rfl
 
 end Decode
diff --git a/Arm/Exec.lean b/Arm/Exec.lean
index bbadc43a..18ff7562 100644
--- a/Arm/Exec.lean
+++ b/Arm/Exec.lean
@@ -132,8 +132,7 @@ def run (n : Nat) (s : ArmState) : ArmState :=
     run n' s'
 
 theorem run_opener_zero (s : ArmState) :
-  run 0 s = s := by
-  rfl
+  run 0 s = s := rfl
 
 theorem run_opener_general
   (n : Nat) (s : ArmState) :
diff --git a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
index ed098368..308ff95b 100644
--- a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
+++ b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
@@ -27,12 +27,12 @@ theorem Nat_lt_of_le_of_le (x y z : Nat) (h1 : x < y) (h2 : y <= z) : x <= z :=
   exact Nat.lt_of_lt_of_le h1 h2
 
 theorem pow2_helper1 (i : Nat) : 8 * 2 ^ i = 2 ^ (3 + i) := by
-  have h : 8 = 2^3 := by rfl
+  have h : 8 = 2^3 := rfl
   rw [h]
   exact (Nat.pow_add 2 3 i).symm
 
 theorem pow2_helper2 (j : Nat) (h : j <= 6) : 64 / 2 ^ j = 2 ^ (6 - j) := by
-  have h0 : 64 = 2^6 := by rfl
+  have h0 : 64 = 2^6 := rfl
   rw [h0]
   refine Nat.pow_div ?h ?hx
   repeat simp_all!
diff --git a/Arm/MinTheory.lean b/Arm/MinTheory.lean
index 07defec4..602f47ee 100644
--- a/Arm/MinTheory.lean
+++ b/Arm/MinTheory.lean
@@ -136,7 +136,7 @@ attribute [minimal_theory] Nat.le_refl
 
 @[minimal_theory]
 theorem option_get_bang_of_some [Inhabited α] (v : α) :
-  Option.get! (some v) = v := by rfl
+  Option.get! (some v) = v := rfl
 attribute [minimal_theory] Option.isNone_some
 
 attribute [minimal_theory] Fin.isValue
diff --git a/Arm/State.lean b/Arm/State.lean
index 31a29724..bc21f695 100644
--- a/Arm/State.lean
+++ b/Arm/State.lean
@@ -367,19 +367,19 @@ These mnemonics make it much easier to read and write theorems about assembly pr
 
 @[state_simp_rules] abbrev ArmState.N (s : ArmState) : BitVec 1 := r (StateField.FLAG PFlag.N) s
 
-def ArmState.r_GPR_0_eq_x0 (s : ArmState) : r (StateField.GPR 0) s = s.x0 := by rfl
+def ArmState.r_GPR_0_eq_x0 (s : ArmState) : r (StateField.GPR 0) s = s.x0 := rfl
 
-def ArmState.r_GPR_1_eq_x1 (s : ArmState) : r (StateField.GPR 1) s = s.x1 := by rfl
+def ArmState.r_GPR_1_eq_x1 (s : ArmState) : r (StateField.GPR 1) s = s.x1 := rfl
 
-def ArmState.r_GPR_31_eq_sp (s : ArmState) : r (StateField.GPR 31) s = s.sp := by rfl
+def ArmState.r_GPR_31_eq_sp (s : ArmState) : r (StateField.GPR 31) s = s.sp := rfl
 
-def ArmState.r_FLAG_V_eq_V (s : ArmState) : r (StateField.FLAG PFlag.V) s = s.V := by rfl
+def ArmState.r_FLAG_V_eq_V (s : ArmState) : r (StateField.FLAG PFlag.V) s = s.V := rfl
 
-def ArmState.r_FLAG_C_eq_C (s : ArmState) : r (StateField.FLAG PFlag.C) s = s.C := by rfl
+def ArmState.r_FLAG_C_eq_C (s : ArmState) : r (StateField.FLAG PFlag.C) s = s.C := rfl
 
-def ArmState.r_FLAG_Z_eq_Z (s : ArmState) : r (StateField.FLAG PFlag.Z) s = s.Z := by rfl
+def ArmState.r_FLAG_Z_eq_Z (s : ArmState) : r (StateField.FLAG PFlag.Z) s = s.Z := rfl
 
-def ArmState.r_FLAG_N_eq_N (s : ArmState) : r (StateField.FLAG PFlag.N) s = s.N := by rfl
+def ArmState.r_FLAG_N_eq_N (s : ArmState) : r (StateField.FLAG PFlag.N) s = s.N := rfl
 
 
 @[irreducible]
diff --git a/Correctness/Correctness.lean b/Correctness/Correctness.lean
index 14eeb978..1ec8b9c9 100644
--- a/Correctness/Correctness.lean
+++ b/Correctness/Correctness.lean
@@ -501,7 +501,7 @@ theorem cassert_when_cut_exists [Sys σ] [Spec' σ] (s0 si : σ) (n i : Nat)
           simp only [run_run, Nat.add_comm, h_cut]
         have := @cassert_lower_bound σ (i+1)
                 (cassert s0 (run si 1) (i + 1)).fst _ _ s0 (run si 1)
-                n this (by rfl)
+                n this rfl
         omega
       rw [this] at h_inv''
       rw [cassert_eq]
@@ -630,7 +630,7 @@ theorem termination_from_decreasing_rank [Sys σ] [Spec' σ] (rank : σ → Nat)
       intro x
       exact h_not_exit (n' + x)
     exact h_inv (rank (run s n')) (h_rank ▸ h_term_helper.right) (run s n')
-                 h_exit_assump (h_term_helper.left) (by rfl)
+                 h_exit_assump (h_term_helper.left) rfl
     done
 
 ----------------------------------------------------------------------
diff --git a/Proofs/Experiments/SHA512MemoryAliasing.lean b/Proofs/Experiments/SHA512MemoryAliasing.lean
index 75b27e7f..680c567c 100644
--- a/Proofs/Experiments/SHA512MemoryAliasing.lean
+++ b/Proofs/Experiments/SHA512MemoryAliasing.lean
@@ -149,7 +149,7 @@ theorem sha512_block_armv8_loop_sym_ktbl_access (s1 : ArmState)
   simp_all only [memory_rules]
   -- @bollu: we need 'hSHA2_k512_length' to allow omega to reason about
   -- SHA2.k_512.length, which is otherwise treated as an unintepreted constant.
-  have hSHA2_k512_length : SHA2.k_512.length = 80 := by rfl
+  have hSHA2_k512_length : SHA2.k_512.length = 80 := rfl
   simp_mem -- It should fail if it makes no progress. Also, make small examples that demonstrate such failures.
   rfl
 
diff --git a/Specs/GCMV8.lean b/Specs/GCMV8.lean
index c2fda1e7..7483e332 100644
--- a/Specs/GCMV8.lean
+++ b/Specs/GCMV8.lean
@@ -37,83 +37,73 @@ def lo (x : BitVec 128) : BitVec 64 :=
 def pmult (x: BitVec (m + 1)) (y : BitVec (n + 1)) : BitVec (m + n + 1) :=
   let rec pmultTR (x: BitVec (m + 1)) (y : BitVec (n + 1)) (i : Nat)
     (acc : BitVec (m + n + 1)) : BitVec (m + n + 1) :=
-    if i < n + 1 then
+    match i with
+    | 0 => acc
+    | j + 1 =>
       let acc := acc <<< 1
-      have h : m + n + 1 = n + (m + 1) := by omega
-      let tmp := if getMsbD y i
+      let tmp := if getMsbD y (n + 1 - i)
                  then (BitVec.zero n) ++ x
-                 else BitVec.cast h (BitVec.zero (m + n + 1))
+                 else BitVec.zero (n + (m + 1))
+      have h : m + n + 1 = n + (m + 1) := by omega
       let acc := (BitVec.cast h acc) ^^^ tmp
-      pmultTR x y (i + 1) (BitVec.cast h.symm acc)
-    else acc
-  pmultTR x y 0 (BitVec.zero (m + n + 1))
+      pmultTR x y j (BitVec.cast h.symm acc)
+  pmultTR x y (n + 1) (BitVec.zero (m + n + 1))
 
-example: pmult 0b1101#4 0b10#2 = 0b11010#5 := by 
-  -- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
-  native_decide
+example: pmult 0b1101#4 0b10#2 = 0b11010#5 := rfl
 
 /-- Degree of x. -/
 private def degree (x : BitVec n) : Nat :=
   let rec degreeTR (x : BitVec n) (n : Nat) : Nat :=
-    if n = 0 then 0
-    else if getLsbD x n then n else degreeTR x (n - 1)
+    match n with
+    | 0 => 0
+    | m + 1 =>
+      if getLsbD x n then n else degreeTR x m
   degreeTR x (n - 1)
-example: GCMV8.degree 0b0101#4 = 2 := by
-  -- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
-  native_decide
+example: GCMV8.degree 0b0101#4 = 2 := rfl
 
 /-- Subtract x from y if y's x-degree-th bit is 1. -/
 private def reduce (x : BitVec n) (y : BitVec n) : BitVec n :=
   if getLsbD y (GCMV8.degree x) then y ^^^ x else y
 
 /-- Performs division of polynomials over GF(2). -/
-def pdiv (x: BitVec n) (y : BitVec m) (h : 0 < m): BitVec n :=
+def pdiv (x: BitVec n) (y : BitVec m): BitVec n :=
   let rec pdivTR (x : BitVec n) (y : BitVec m) (i : Nat) (z : BitVec m)
     (acc : BitVec n) : BitVec n :=
-    if i < n then
-      have h2 : (n - i - 1) - (n - i - 1) + 1 = 1 := by omega
-      let xi : BitVec 1 := BitVec.cast h2 (extractLsb (n - i - 1) (n - i - 1) x)
-      have h3 : m - 1 - 0 + 1 = m := by omega
-      let zi : BitVec m :=
-        BitVec.cast h3 (extractLsb (m - 1) 0 ((GCMV8.reduce y z) ++ xi))
-      have h1 : GCMV8.degree y - GCMV8.degree y + 1 = 1 := by omega
-      let bit : BitVec 1 :=
-        BitVec.cast h1 $ extractLsb (GCMV8.degree y) (GCMV8.degree y) zi
-      have h4 : 1 = (n - i - 1) - (n - i - 1) + 1 := by omega
+    match i with
+    | 0 => acc
+    | j + 1 =>
+      let xi := extractLsb' (i - 1) 1 x
+      let zi := extractLsb' 0 m ((GCMV8.reduce y z) ++ xi)
+      let bit := extractLsb' (GCMV8.degree y) 1 zi
       let newacc : BitVec n :=
-        partInstall (n - i - 1) (n - i - 1) (BitVec.cast h4 bit) acc
-      pdivTR x y (i + 1) zi newacc
-    else acc
-  pdivTR x y 0 (BitVec.zero m) (BitVec.zero n)
+        partInstall (i - 1) (i - 1) (bit.cast (by omega)) acc
+      pdivTR x y j zi newacc
+  pdivTR x y n (BitVec.zero m) (BitVec.zero n)
 
--- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
-example : pdiv 0b1101#4 0b10#2 (by omega) = 0b110#4 := by native_decide
-example : pdiv 0x1a#5 0b10#2 (by omega) = 0b1101#5 := by native_decide
-example : pdiv 0b1#1 0b10#2 (by omega) = 0b0#1 := by native_decide
+example : pdiv 0b1101#4 0b10#2 = 0b110#4 := rfl
+example : pdiv 0x1a#5 0b10#2 = 0b1101#5 := rfl
+example : pdiv 0b1#1 0b10#2 = 0b0#1 := rfl
 
 /-- Performs modulus of polynomials over GF(2). -/
 def pmod (x : BitVec n) (y : BitVec (m + 1)) (H : 0 < m) : BitVec m :=
   let rec pmodTR (x : BitVec n) (y : BitVec (m + 1)) (p : BitVec (m + 1))
     (i : Nat) (r : BitVec m) (H : 0 < m) : BitVec m :=
-    if i < n then
-      let xi := getLsbD x i
-      have h : m - 1 + 1 = m := by omega
-      let tmp : BitVec (m - 1 + 1) :=
-        if xi
-        then extractLsb (m - 1) 0 p
-        else BitVec.cast h.symm (BitVec.zero m)
-      let r := (BitVec.cast h.symm r) ^^^ tmp
-      pmodTR x y (GCMV8.reduce y (p <<< 1)) (i + 1) (BitVec.cast h r) H
-    else r
-  if y = 0 then 0 else pmodTR x y (GCMV8.reduce y 1) 0 (BitVec.zero m) H
-
--- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
-example: pmod 0b011#3 0b00#2 (by omega) = 0b0#1 := by native_decide
-example: pmod 0b011#3 0b01#2 (by omega) = 0b0#1 := by native_decide
-example: pmod 0b011#3 0b10#2 (by omega) = 0b1#1 := by native_decide
-example: pmod 0b011#3 0b11#2 (by omega) = 0b0#1 := by native_decide
-example: pmod 0b011#3 0b100#3 (by omega) = 0b11#2 := by native_decide
-example: pmod 0b011#3 0b1001#4 (by omega) = 0b11#3 := by native_decide
+    match i with
+    | 0 => r
+    | j + 1 =>
+      let xi := getLsbD x (n - i)
+      let tmp :=
+        if xi then extractLsb' 0 m p else BitVec.zero m
+      let r := r ^^^ tmp
+      pmodTR x y (GCMV8.reduce y (p <<< 1)) j r H
+  if y = 0 then 0 else pmodTR x y (GCMV8.reduce y 1) n (BitVec.zero m) H
+
+example: pmod 0b011#3 0b00#2 (by omega) = 0b0#1 := rfl
+example: pmod 0b011#3 0b01#2 (by omega) = 0b0#1 := rfl
+example: pmod 0b011#3 0b10#2 (by omega) = 0b1#1 := rfl
+example: pmod 0b011#3 0b11#2 (by omega) = 0b0#1 := rfl
+example: pmod 0b011#3 0b100#3 (by omega) = 0b11#2 := rfl
+example: pmod 0b011#3 0b1001#4 (by omega) = 0b11#3 := rfl
 
 ------------------------------------------------------------------------------
 -- Functions related to GCM
@@ -188,10 +178,7 @@ def GCMInitV8 (H : BitVec 128) : (List (BitVec 128)) :=
   [H0_rev, H1, H2_rev, H3_rev, H4, H5_rev, H6_rev,
    H7, H8_rev, H9_rev, H10, H11_rev]
 
--- set_option profiler true in
--- set_option maxRecDepth 20000 in
--- set_option maxHeartbeats 2000000 in
--- unseal pmod.pmodTR degree.degreeTR reverse.reverseTR pmult.pmultTR Nat.bitwise in
+set_option maxRecDepth 8000 in
 example :  GCMInitV8 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 ==
   [ 0x1099f4b39468565ccdd297a9df145877#128,
     0x62d81a7fe5da3296dd4b631a4b7c0e2b#128,
@@ -204,7 +191,7 @@ example :  GCMInitV8 0x66e94bd4ef8a2c3b884cfa59ca342b2e#128 ==
     0x4af32418184aee1eec87cfb0e19d1c4e#128,
     0xf109e6e0b31d1eee7d1998bcfc545474#128,
     0x7498729da40cd2808c107e5c4f494a9a#128,
-    0xa47c653dfbeac924d0e417a05fe61ba4#128 ] := by native_decide
+    0xa47c653dfbeac924d0e417a05fe61ba4#128 ] := rfl
 
 /-- GCMGmultV8 specification:
     H  : [128] -- the first element in Htable, not the initial H input to GCMInitV8
@@ -216,12 +203,12 @@ def GCMGmultV8 (H : BitVec 128) (Xi : List (BitVec 8)) (h : 8 * Xi.length = 128)
   let H := (lo H) ++ (hi H)
   split (GCMV8.gcm_polyval H (BitVec.cast h (BitVec.flatten Xi))) 8 (by omega)
 
--- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
+set_option maxRecDepth 8000 in
 example : GCMGmultV8 0x1099f4b39468565ccdd297a9df145877#128
   [ 0x10#8, 0x54#8, 0x43#8, 0xb0#8, 0x2c#8, 0x4b#8, 0x1f#8, 0x24#8,
     0x3b#8, 0xcd#8, 0xd4#8, 0x87#8, 0x16#8, 0x65#8, 0xb3#8, 0x2b#8 ] (by decide) =
   [ 0xa2#8, 0xc9#8, 0x9c#8, 0x56#8, 0xeb#8, 0xa7#8, 0x91#8, 0xf6#8,
-    0x9e#8, 0x15#8, 0xa6#8, 0x00#8, 0x67#8, 0x29#8, 0x7e#8, 0x0f#8 ] := by native_decide
+    0x9e#8, 0x15#8, 0xa6#8, 0x00#8, 0x67#8, 0x29#8, 0x7e#8, 0x0f#8 ] := rfl
 
 
 private def gcm_ghash_block (H : BitVec 128) (Xi : BitVec 128)
@@ -240,26 +227,25 @@ def GCMGhashV8 (H : BitVec 128) (Xi : List (BitVec 8))
   : List (BitVec 8) :=
   let rec GCMGhashV8TR {m : Nat} (H : BitVec 128) (Xi : BitVec 128)
     (inp : BitVec m) (i : Nat) (h1 : 128 ∣ m) : BitVec 128 :=
-    if i < m / 128 then
-      let lo := m - (i + 1) * 128
-      let hi := lo + 127
-      have h2 : hi - lo + 1 = 128 := by omega
-      let inpi : BitVec 128 := BitVec.cast h2 $ extractLsb hi lo inp
+    match i with
+    | 0 => Xi
+    | j + 1 =>
+      let lo := (i - 1) * 128
+      let inpi := extractLsb' lo 128 inp
       let Xj := GCMV8.gcm_ghash_block H Xi inpi
-      GCMGhashV8TR H Xj inp (i + 1) h1
-    else Xi
+      GCMGhashV8TR H Xj inp j h1
   have h3 : 128 ∣ 8 * inp.length := by omega
   have h4 : 8 * Xi.length = 128 := by omega
   let flat_Xi := BitVec.cast h4 $ BitVec.flatten Xi
   let flat_inp := BitVec.flatten inp
-  split (GCMGhashV8TR H flat_Xi flat_inp 0 h3) 8 (by omega)
+  split (GCMGhashV8TR H flat_Xi flat_inp (8 * inp.length / 128) h3) 8 (by omega)
 
--- (FIXME) With leanprover/lean4:nightly-2024-08-29, just `rfl` sufficed here.
+set_option maxRecDepth 8000 in
 example : GCMGhashV8 0x1099f4b39468565ccdd297a9df145877#128
   [ 0xa2#8, 0xc9#8, 0x9c#8, 0x56#8, 0xeb#8, 0xa7#8, 0x91#8, 0xf6#8,
     0x9e#8, 0x15#8, 0xa6#8, 0x00#8, 0x67#8, 0x29#8, 0x7e#8, 0x0f#8 ]
   (List.replicate 16 0x2a#8) (by simp) (by simp only [List.length_replicate]; omega) =
   [ 0x20#8, 0x60#8, 0x2e#8, 0x75#8, 0x7a#8, 0x4e#8, 0xec#8, 0x90#8,
-    0xc0#8, 0x9d#8, 0x49#8, 0xfd#8, 0xdc#8, 0xf2#8, 0xc9#8, 0x35#8 ] := by native_decide
+    0xc0#8, 0x9d#8, 0x49#8, 0xfd#8, 0xdc#8, 0xf2#8, 0xc9#8, 0x35#8 ] := rfl
 
 end GCMV8