diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean
index 57364dac39..5faeff7aec 100644
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -1478,7 +1478,7 @@ theorem forall_mem_filter {p : α → Bool} {xs : Array α} {P : α → Prop} :
 
 theorem getElem?_filter {xs : Array α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).size)
     (w : (xs.filter p)[i]? = some a) : p a := by
-  rw [getElem?_eq_getElem] at w
+  rw [getElem?_eq_getElem h] at w
   simp only [Option.some.injEq] at w
   rw [← w]
   apply getElem_filter h
@@ -4470,10 +4470,10 @@ theorem back!_eq_back? [Inhabited α] {xs : Array α} : xs.back! = xs.back?.getD
 
 theorem getElem?_push_lt {xs : Array α} {x : α} {i : Nat} (h : i < xs.size) :
     (xs.push x)[i]? = some xs[i] := by
-  rw [getElem?_pos, getElem_push_lt]
+  rw [getElem?_pos (xs.push x) i (size_push _ ▸ Nat.lt_succ_of_lt h), getElem_push_lt]
 
 theorem getElem?_push_eq {xs : Array α} {x : α} : (xs.push x)[xs.size]? = some x := by
-  rw [getElem?_pos, getElem_push_eq]
+  rw [getElem?_pos (xs.push x) xs.size (size_push _ ▸ Nat.lt_succ_self xs.size), getElem_push_eq]
 
 @[simp] theorem getElem?_size {xs : Array α} : xs[xs.size]? = none := by
   simp only [getElem?_def, Nat.lt_irrefl, dite_false]
diff --git a/src/Init/Data/Fin/Fold.lean b/src/Init/Data/Fin/Fold.lean
index 1b6b9722f1..5b6c9fdb29 100644
--- a/src/Init/Data/Fin/Fold.lean
+++ b/src/Init/Data/Fin/Fold.lean
@@ -122,7 +122,7 @@ private theorem foldlM_loop [Monad m] (f : α → Fin (n+1) → m α) (x) (h : i
     rw [foldlM_loop_lt _ _ h', foldlM_loop]; rfl
   else
     cases Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.not_lt.1 h')
-    rw [foldlM_loop_lt]
+    rw [foldlM_loop_lt _ _ h]
     congr; funext
     rw [foldlM_loop_eq, foldlM_loop_eq]
 termination_by n - i
diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
index 3a33e1a81f..1e3a671b76 100644
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -939,8 +939,8 @@ theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.len
   | nil => simp
   | cons _ _ =>
     apply getLast!_of_getLast?
-    rw [getElem!_pos, getElem_cons_length (h := by simp)]
-    rfl
+    rw [getLast?_eq_getElem?]
+    simp
 
 /-! ## Head and tail -/
 
@@ -1344,7 +1344,7 @@ grind_pattern getElem_filter => (xs.filter p)[i]
 
 theorem getElem?_filter {xs : List α} {p : α → Bool} {i : Nat} (h : i < (xs.filter p).length)
     (w : (xs.filter p)[i]? = some a) : p a := by
-  rw [getElem?_eq_getElem] at w
+  rw [getElem?_eq_getElem h] at w
   simp only [Option.some.injEq] at w
   rw [← w]
   apply getElem_filter h
diff --git a/src/Init/Data/List/Nat/TakeDrop.lean b/src/Init/Data/List/Nat/TakeDrop.lean
index 440b952232..06e3c2b1ce 100644
--- a/src/Init/Data/List/Nat/TakeDrop.lean
+++ b/src/Init/Data/List/Nat/TakeDrop.lean
@@ -567,9 +567,10 @@ theorem getElem_zipWith {f : α → β → γ} {l : List α} {l' : List β}
       f (l[i]'(lt_length_left_of_zipWith h))
         (l'[i]'(lt_length_right_of_zipWith h)) := by
   rw [← Option.some_inj, ← getElem?_eq_getElem, getElem?_zipWith_eq_some]
+  have := lt_length_right_of_zipWith h
   exact
-    ⟨l[i]'(lt_length_left_of_zipWith h), l'[i]'(lt_length_right_of_zipWith h),
-      by rw [getElem?_eq_getElem], by rw [getElem?_eq_getElem]; exact ⟨rfl, rfl⟩⟩
+    ⟨l[i]'(lt_length_left_of_zipWith h), l'[i],
+      by rw [getElem?_eq_getElem], by rw [getElem?_eq_getElem this]; exact ⟨rfl, rfl⟩⟩
 
 theorem zipWith_eq_zipWith_take_min : ∀ {l₁ : List α} {l₂ : List β},
     zipWith f l₁ l₂ = zipWith f (l₁.take (min l₁.length l₂.length)) (l₂.take (min l₁.length l₂.length))
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 7d2cb96d14..4a0fd95340 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -284,7 +284,8 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
   liftMetaTactic fun mvarId => do mvarId.contradiction; pure []
 
 @[builtin_tactic Lean.Parser.Tactic.eqRefl] def evalRefl : Tactic := fun _ =>
-  liftMetaTactic fun mvarId => do mvarId.refl; pure []
+  -- Allow assigning synthetic opaque so that it is as capable as `exact rfl`.
+  liftMetaTactic fun mvarId => do withAssignableSyntheticOpaque mvarId.refl; pure []
 
 @[builtin_tactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do
   match stx with
diff --git a/src/Lean/Elab/Tactic/Conv/Rewrite.lean b/src/Lean/Elab/Tactic/Conv/Rewrite.lean
index fa535095d1..934530d415 100644
--- a/src/Lean/Elab/Tactic/Conv/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Conv/Rewrite.lean
@@ -6,7 +6,6 @@ Authors: Leonardo de Moura
 module
 
 prelude
-public import Lean.Meta.Tactic.Rewrite
 public import Lean.Elab.Tactic.Rewrite
 public import Lean.Elab.Tactic.Conv.Basic
 
@@ -17,11 +16,11 @@ open Meta
 
 @[builtin_tactic Lean.Parser.Tactic.Conv.rewrite] def evalRewrite : Tactic := fun stx => do
   let config ← Tactic.elabRewriteConfig stx[1]
-  withRWRulesSeq stx[0] stx[2] fun symm term => do
-    Term.withSynthesize <| withMainContext do
-      let e ← elabTerm term none true
-      let r ←  (← getMainGoal).rewrite (← getLhs) e symm (config := config)
-      updateLhs r.eNew r.eqProof
-      replaceMainGoal ((← getMainGoal) :: r.mvarIds)
+  withRWRulesSeq stx[0] stx[2] fun symm term => withMainContext do
+    let r ← Term.withSynthesize do
+      elabRewrite (← getMainGoal) (← getLhs) term symm (config := config)
+    let r ← finishElabRewrite r
+    updateLhs r.eNew r.eqProof
+    replaceMainGoal ((← getMainGoal) :: r.mvarIds)
 
 end Lean.Elab.Tactic.Conv
diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean
index f0a4ca1358..04274f20e4 100644
--- a/src/Lean/Elab/Tactic/Rewrite.lean
+++ b/src/Lean/Elab/Tactic/Rewrite.lean
@@ -17,25 +17,53 @@ public section
 namespace Lean.Elab.Tactic
 open Meta
 
+/--
+Runs `Lean.MVarId.rewrite`, and also handles filtering out the old metavariables in the rewrite result.
+This should be used from within `withSynthesize`.
+Use `finishElabRewrite` once elaboration is complete to make final updates to `RewriteResult`.
+-/
+def elabRewrite (mvarId : MVarId) (e : Expr) (stx : Syntax)
+    (symm : Bool := false) (config := { : Rewrite.Config }) : TacticM RewriteResult := do
+  let mvarCounterSaved := (← getMCtx).mvarCounter
+  let thm ← elabTerm stx none true
+  if thm.hasSyntheticSorry then
+    throwAbortTactic
+  unless ← occursCheck mvarId thm do
+    throwErrorAt stx "Occurs check failed: Expression{indentExpr thm}\ncontains the goal {Expr.mvar mvarId}"
+  let r ← mvarId.rewrite e thm symm (config := config)
+  let mctx ← getMCtx
+  let mvarIds := r.mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved
+
+  return { r with mvarIds }
+
+/--
+Makes new goals be synthetic opaque, to be done once elaboration of the rewrite theorem is complete.
+
+Workaround note: we are only doing this for proof goals, not data goals,
+since there are many downstream cases of tactic proofs that later assign data goals by unification.
+-/
+def finishElabRewrite (r : RewriteResult) : MetaM RewriteResult := do
+  let mvarIds ← r.mvarIds.filterM (not <$> ·.isAssigned)
+  mvarIds.forM fun newMVarId => newMVarId.withContext do
+    if ← Meta.isProp (← newMVarId.getType) then
+      newMVarId.setKind .syntheticOpaque
+  return { r with mvarIds }
+
 def rewriteTarget (stx : Syntax) (symm : Bool) (config : Rewrite.Config := {}) : TacticM Unit := do
-  Term.withSynthesize <| withMainContext do
-    let e ← elabTerm stx none true
-    if e.hasSyntheticSorry then
-      throwAbortTactic
-    let r ← (← getMainGoal).rewrite (← getMainTarget) e symm (config := config)
-    let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
-    replaceMainGoal (mvarId' :: r.mvarIds)
+  let r ← Term.withSynthesize <| withMainContext do
+    elabRewrite (← getMainGoal) (← getMainTarget) stx symm (config := config)
+  let r ← finishElabRewrite r
+  let mvarId' ← (← getMainGoal).replaceTargetEq r.eNew r.eqProof
+  replaceMainGoal (mvarId' :: r.mvarIds)
 
 def rewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Rewrite.Config := {}) :
     TacticM Unit := withMainContext do
   -- Note: we cannot execute `replaceLocalDecl` inside `Term.withSynthesize`.
   -- See issues #2711 and #2727.
   let rwResult ← Term.withSynthesize <| withMainContext do
-    let e ← elabTerm stx none true
-    if e.hasSyntheticSorry then
-      throwAbortTactic
     let localDecl ← fvarId.getDecl
-    (← getMainGoal).rewrite localDecl.type e symm (config := config)
+    elabRewrite (← getMainGoal) localDecl.type stx symm (config := config)
+  let rwResult ← finishElabRewrite rwResult
   let replaceResult ← (← getMainGoal).replaceLocalDecl fvarId rwResult.eNew rwResult.eqProof
   replaceMainGoal (replaceResult.mvarId :: rwResult.mvarIds)
 
diff --git a/src/Lean/Meta/Tactic/Rewrite.lean b/src/Lean/Meta/Tactic/Rewrite.lean
index 531c51120b..723b3ced35 100644
--- a/src/Lean/Meta/Tactic/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Rewrite.lean
@@ -24,7 +24,8 @@ structure RewriteResult where
   mvarIds  : List MVarId -- new goals
 
 /--
-Rewrite goal `mvarId`
+Rewrite `e` using `heq` in the context of `mvarId`.
+Returns the result of the rewrite, the metavariable `mvarId` is not assigned.
 -/
 def _root_.Lean.MVarId.rewrite (mvarId : MVarId) (e : Expr) (heq : Expr)
     (symm : Bool := false) (config := { : Rewrite.Config }) : MetaM RewriteResult :=
diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
index 98ad00628b..2757c188ae 100644
--- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean
+++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean
@@ -394,7 +394,7 @@ theorem containsThenInsert_fst [TransOrd α] (h : t.WF) {k : α} {v : β k} :
 
 theorem containsThenInsert!_fst [TransOrd α] (h : t.WF) {k : α} {v : β k} :
     (t.containsThenInsert! k v).1 = t.contains k := by
-  rw [containsThenInsert!_fst_eq_containsThenInsert_fst, containsThenInsert_fst h]
+  rw [containsThenInsert!_fst_eq_containsThenInsert_fst _ h.balanced, containsThenInsert_fst h]
 
 theorem containsThenInsert_snd [TransOrd α] (h : t.WF) {k : α} {v : β k} :
     (t.containsThenInsert k v h.balanced).2.impl = (t.insert k v h.balanced).impl := by
@@ -411,7 +411,7 @@ theorem containsThenInsertIfNew_fst [TransOrd α] (h : t.WF) {k : α} {v : β k}
 
 theorem containsThenInsertIfNew!_fst [TransOrd α] (h : t.WF) {k : α} {v : β k} :
     (t.containsThenInsertIfNew! k v).1 = t.contains k := by
-  rw [containsThenInsertIfNew!_fst_eq_containsThenInsertIfNew_fst, containsThenInsertIfNew_fst h]
+  rw [containsThenInsertIfNew!_fst_eq_containsThenInsertIfNew_fst _ h.balanced, containsThenInsertIfNew_fst h]
 
 theorem containsThenInsertIfNew_snd [TransOrd α] (h : t.WF) {k : α} {v : β k} :
     (t.containsThenInsertIfNew k v h.balanced).2.impl = (t.insertIfNew k v h.balanced).impl := by
diff --git a/src/Std/Sat/AIG/CachedGatesLemmas.lean b/src/Std/Sat/AIG/CachedGatesLemmas.lean
index d3ae258b8a..c39d853c88 100644
--- a/src/Std/Sat/AIG/CachedGatesLemmas.lean
+++ b/src/Std/Sat/AIG/CachedGatesLemmas.lean
@@ -124,8 +124,8 @@ theorem mkXorCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : id
   simp only [mkXorCached]
   rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
   rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
-  · rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
-    apply LawfulOperator.lt_size_of_lt_aig_size
+  rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
+  · apply LawfulOperator.lt_size_of_lt_aig_size
     assumption
   · apply LawfulOperator.lt_size_of_lt_aig_size
     apply LawfulOperator.lt_size_of_lt_aig_size
@@ -159,8 +159,8 @@ theorem mkBEqCached_decl_eq idx (aig : AIG α) (input : BinaryInput aig) {h : id
   simp only [mkBEqCached]
   rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
   rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
-  · rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
-    apply LawfulOperator.lt_size_of_lt_aig_size
+  rw [AIG.LawfulOperator.decl_eq (f := mkGateCached)]
+  · apply LawfulOperator.lt_size_of_lt_aig_size
     assumption
   · apply LawfulOperator.lt_size_of_lt_aig_size
     apply LawfulOperator.lt_size_of_lt_aig_size
diff --git a/src/Std/Sat/AIG/If.lean b/src/Std/Sat/AIG/If.lean
index 767a58207e..1d81490302 100644
--- a/src/Std/Sat/AIG/If.lean
+++ b/src/Std/Sat/AIG/If.lean
@@ -103,12 +103,12 @@ theorem denote_mkIfCached {aig : AIG α} {input : TernaryInput aig} :
   simp only [TernaryInput.cast, Ref.cast_eq, denote_mkOrCached,
     denote_projected_entry, denote_mkAndCached, denote_mkNotCached]
   congr 2
-  · rw [LawfulOperator.denote_mem_prefix]
+  · rw [LawfulOperator.denote_mem_prefix (LawfulOperator.lt_size ..)]
     rw [LawfulOperator.denote_mem_prefix]
     · simp
     · simp [Ref.hgate]
   · rw [LawfulOperator.denote_mem_prefix]
-  · rw [LawfulOperator.denote_mem_prefix]
+  · rw [LawfulOperator.denote_mem_prefix (LawfulOperator.lt_size_of_lt_aig_size _ _ input.rhs.hgate)]
     rw [LawfulOperator.denote_mem_prefix]
 
 namespace RefVec
@@ -198,13 +198,11 @@ theorem go_get_aux {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (d
   split at hgo
   · rw [← hgo]
     intros
-    rw [go_get_aux]
-    rw [AIG.RefVec.get_push_ref_lt]
-    · simp only [Ref.cast, Ref.mk.injEq]
-      rw [AIG.RefVec.get_cast]
-      · simp
-      · assumption
-    · apply go_le_size
+    rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := go_le_size ..)]
+    rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)]
+    simp only [Ref.cast, Ref.mk.injEq]
+    rw [AIG.RefVec.get_cast]
+    simp
   · rw [← hgo]
     simp only [Nat.le_refl, get]
     have : curr = w := by omega
@@ -261,7 +259,7 @@ theorem denote_go {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (di
     | inl heq =>
       subst heq
       rw [← hgo]
-      rw [go_get]
+      rw [go_get]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_eq']
       · rw [go_denote_mem_prefix]
         · simp
diff --git a/src/Std/Sat/AIG/RefVecOperator/Map.lean b/src/Std/Sat/AIG/RefVecOperator/Map.lean
index 2826d86994..d3bdb9c2f2 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Map.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Map.lean
@@ -148,12 +148,11 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVe
   · dsimp only at hgo
     rw [← hgo]
     intro hfoo
-    rw [go_get_aux]
-    rw [AIG.RefVec.get_push_ref_lt]
+    rw [go_get_aux]; case hidx => omega
+    rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)]
     · simp only [Ref.cast, Ref.mk.injEq]
       rw [AIG.RefVec.get_cast]
-      · simp
-      · assumption
+      simp
     · apply go_le_size
   · dsimp only at hgo
     rw [← hgo]
@@ -209,13 +208,12 @@ theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec
     cases Nat.eq_or_lt_of_le hidx2 with
     | inl heq =>
       rw [← hgo]
-      rw [go_get]
-      rw [AIG.RefVec.get_push_ref_eq']
-      · simp only [← heq]
-        rw [go_denote_mem_prefix]
-        · simp
-        · simp [Ref.hgate]
-      · rw [heq]
+      rw [go_get]; case hidx => omega
+      rw [AIG.RefVec.get_push_ref_eq' (hidx := heq.symm)]
+      simp only [← heq]
+      rw [go_denote_mem_prefix]
+      · simp
+      · simp [Ref.hgate]
     | inr hlt =>
       rw [← hgo]
       rw [denote_go]
diff --git a/src/Std/Sat/AIG/RefVecOperator/Zip.lean b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
index 61d6973715..d6663baf49 100644
--- a/src/Std/Sat/AIG/RefVecOperator/Zip.lean
+++ b/src/Std/Sat/AIG/RefVecOperator/Zip.lean
@@ -197,13 +197,11 @@ theorem go_get_aux {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVe
   · dsimp only at hgo
     rw [← hgo]
     intro hfoo
-    rw [go_get_aux]
-    rw [AIG.RefVec.get_push_ref_lt]
-    · simp only [Ref.cast, Ref.mk.injEq]
-      rw [AIG.RefVec.get_cast]
-      · simp
-      · assumption
-    · apply go_le_size
+    rw [go_get_aux (hfoo := go_le_size ..)]; case hidx => omega
+    rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)]
+    simp only [Ref.cast, Ref.mk.injEq]
+    rw [AIG.RefVec.get_cast]
+    simp
   · dsimp only at hgo
     rw [← hgo]
     simp only [Nat.le_refl, get, Ref.cast_eq, Ref.mk.injEq, true_implies]
@@ -262,7 +260,7 @@ theorem denote_go {aig : AIG α} (curr : Nat) (hcurr : curr ≤ len) (s : RefVec
     cases Nat.eq_or_lt_of_le hidx2 with
     | inl heq =>
       rw [← hgo]
-      rw [go_get]
+      rw [go_get]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_eq']
       · simp only [← heq]
         rw [go_denote_mem_prefix]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
index 82b38302c0..9be7f49fee 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean
@@ -333,14 +333,14 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
     | .and | .or | .xor =>
       rw [AIG.RefVec.zip_decl_eq]
       rw [goCache_decl_eq, goCache_decl_eq]
-      · omega
+      · exact Nat.lt_of_lt_of_le h1 hl
       · apply Nat.lt_of_lt_of_le
         · exact h1
         · apply Nat.le_trans <;> assumption
     | .add | .mul | .udiv | .umod =>
       rw [AIG.LawfulVecOperator.decl_eq]
       rw [goCache_decl_eq, goCache_decl_eq]
-      · omega
+      · exact Nat.lt_of_lt_of_le h1 hl
       · apply Nat.lt_of_lt_of_le
         · exact h1
         · apply Nat.le_trans <;> assumption
@@ -350,13 +350,13 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
       rw [AIG.LawfulVecOperator.decl_eq]
       rw [goCache_decl_eq]
       have := (goCache aig expr cache).result.property
-      omega
+      exact Nat.lt_of_lt_of_le h1 this
   next lhsExpr rhsExpr h =>
     have hl := (goCache aig lhsExpr cache).result.property
     have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property
     rw [AIG.LawfulVecOperator.decl_eq]
     rw [goCache_decl_eq, goCache_decl_eq]
-    · omega
+    · exact Nat.lt_of_lt_of_le h1 hl
     · apply Nat.lt_of_lt_of_le
       · exact h1
       · apply Nat.le_trans <;> assumption
@@ -364,18 +364,18 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
     rw [AIG.LawfulVecOperator.decl_eq (f := blastReplicate)]
     rw [goCache_decl_eq]
     have := (goCache aig inner cache).result.property
-    omega
+    exact Nat.lt_of_lt_of_le h1 this
   next hi lo inner =>
     rw [AIG.LawfulVecOperator.decl_eq (f := blastExtract)]
     rw [goCache_decl_eq]
     have := (goCache aig inner cache).result.property
-    omega
+    exact Nat.lt_of_lt_of_le h1 this
   next rhsExpr lhsExpr =>
     have hl := (goCache aig lhsExpr cache).result.property
     have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property
     rw [AIG.LawfulVecOperator.decl_eq (f := blastShiftLeft)]
     rw [goCache_decl_eq, goCache_decl_eq]
-    · omega
+    · exact Nat.lt_of_lt_of_le h1 hl
     · apply Nat.lt_of_lt_of_le
       · exact h1
       · apply Nat.le_trans <;> assumption
@@ -384,7 +384,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
     have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property
     rw [AIG.LawfulVecOperator.decl_eq (f := blastShiftRight)]
     rw [goCache_decl_eq, goCache_decl_eq]
-    · omega
+    · exact Nat.lt_of_lt_of_le h1 hl
     · apply Nat.lt_of_lt_of_le
       · exact h1
       · apply Nat.le_trans <;> assumption
@@ -393,7 +393,7 @@ theorem go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) (cache : Cache aig) :
     have hr := (goCache (goCache aig lhsExpr cache).1.1.aig rhsExpr (goCache aig lhsExpr cache).cache).result.property
     rw [AIG.LawfulVecOperator.decl_eq (f := blastArithShiftRight)]
     rw [goCache_decl_eq, goCache_decl_eq]
-    · omega
+    · exact Nat.lt_of_lt_of_le h1 hl
     · apply Nat.lt_of_lt_of_le
       · exact h1
       · apply Nat.le_trans <;>  assumption
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
index 6fd4874e8f..4a43303a78 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Add.lean
@@ -220,17 +220,19 @@ theorem go_decl_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : AIG.R
   unfold go at hgo
   dsimp only at hgo
   split at hgo
-  · rw [← hgo]
-    intros
-    rw [go_decl_eq]
+  next h =>
+    rw [← hgo]
+    intro idx h1 h2
+    have h3 : idx < (mkFullAdderOut aig { lhs := lhs.get curr h, rhs := rhs.get curr h, cin := cin }).aig.decls.size := by
+      apply AIG.LawfulOperator.lt_size_of_lt_aig_size
+      exact h1
+    have h4 : idx < (mkFullAdder aig { lhs := lhs.get curr h, rhs := rhs.get curr h, cin := cin }).aig.decls.size := by
+      apply AIG.LawfulOperator.lt_size_of_lt_aig_size
+      exact h3
+    rw [go_decl_eq (w := w) (curr := curr + 1) (h1 := h4)]
     unfold mkFullAdder
-    rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry)]
+    rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry) (h1 := h3)]
     rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderOut)]
-    · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
-      assumption
-    · apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry)
-      apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
-      assumption
   · simp [← hgo]
 termination_by w - curr
 
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
index fa1d2e9f82..a9bf1c6dcf 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas.lean
@@ -82,7 +82,7 @@ theorem go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExp
     all_goals
       simp [go, Gate.eval]
       congr 1
-      · rw [go_denote_mem_prefix]
+      · rw [go_denote_mem_prefix (hstart := Ref.hgate _)]
         apply lih
         exact hinv
       · apply rih
@@ -92,13 +92,15 @@ theorem go_eval_eq_eval (expr : BVLogicalExpr) (aig : AIG BVBit) (assign : BVExp
     simp only [go, Ref.cast_eq, denote_mkIfCached, denote_projected_entry,
       eval_ite, Bool.ite_eq_cond_iff]
     apply ite_congr
-    · rw [go_denote_mem_prefix]
-      rw [go_denote_mem_prefix]
-      · specialize dih _ _ hinv
-        simp [dih]
-      · simp [Ref.hgate]
+    · rw [go_denote_mem_prefix (hstart := ?h)]
+      case h =>
+        apply go_lt_size_of_lt_aig_size
+        exact Ref.hgate _
+      rw [go_denote_mem_prefix (hstart := Ref.hgate _)]
+      specialize dih _ _ hinv
+      simp [dih]
     · intro h
-      rw [go_denote_mem_prefix]
+      rw [go_denote_mem_prefix (hstart := Ref.hgate _)]
       apply lih
       apply go_Inv_of_Inv
       exact hinv
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
index 03f1058bbd..4636917ba2 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Const.lean
@@ -41,7 +41,7 @@ theorem go_get_aux (aig : AIG α) (c : BitVec w) (curr : Nat) (hcurr : curr ≤
   · dsimp only at hgo
     rw [← hgo]
     intro hfoo
-    rw [go_get_aux]
+    rw [go_get_aux (hfoo := hfoo) (hidx := Nat.lt_succ_of_lt hidx)]
     rw [AIG.RefVec.get_push_ref_lt]
   · dsimp only at hgo
     rw [← hgo]
@@ -74,7 +74,7 @@ theorem go_denote_eq (aig : AIG α) (c : BitVec w) (assign : α → Bool)
     cases Nat.eq_or_lt_of_le hidx2 with
     | inl heq =>
       rw [← hgo]
-      rw [go_get]
+      rw [go_get]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_eq']
       · rw [← heq]
         simp
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
index 4d27259e15..38e30ca329 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean
@@ -313,7 +313,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
       simp only [RefVec.denote_zip, RefVec.get_cast, Ref.cast_eq, denote_mkAndCached, eval_bin,
         BVBinOp.eval_and, BitVec.getLsbD_and]
       congr 1
-      · rw [goCache_denote_mem_prefix]
+      · rw [goCache_denote_mem_prefix (hstart := Ref.hgate _)]
         rw [goCache_denote_eq]
         exact hinv
       · rw [goCache_denote_eq]
@@ -323,7 +323,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
       simp only [RefVec.denote_zip, RefVec.get_cast, Ref.cast_eq, denote_mkOrCached, eval_bin,
         BVBinOp.eval_or, BitVec.getLsbD_or]
       congr 1
-      · rw [goCache_denote_mem_prefix]
+      · rw [goCache_denote_mem_prefix (hstart := Ref.hgate _)]
         rw [goCache_denote_eq]
         exact hinv
       · rw [goCache_denote_eq]
@@ -333,7 +333,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
       simp only [RefVec.denote_zip, RefVec.get_cast, Ref.cast_eq, denote_mkXorCached, eval_bin,
         BVBinOp.eval_xor, BitVec.getLsbD_xor]
       congr 1
-      · rw [goCache_denote_mem_prefix]
+      · rw [goCache_denote_mem_prefix (hstart := Ref.hgate _)]
         rw [goCache_denote_eq]
         exact hinv
       · rw [goCache_denote_eq]
@@ -444,7 +444,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment)
     · rw [goCache_denote_eq]
       apply goCache_Inv_of_Inv
       exact hinv
-    · rw [goCache_denote_mem_prefix]
+    · rw [goCache_denote_mem_prefix (hstart := Ref.hgate _)]
       rw [goCache_denote_eq]
       exact hinv
   next h =>
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
index 52f67b9797..6d1c306c6f 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Add.lean
@@ -75,7 +75,7 @@ theorem mkFullAdder_denote_mem_prefix (aig : AIG α) (input : FullAdderInput aig
     ⟦aig, ⟨start, inv, hstart⟩, assign⟧ := by
   unfold mkFullAdder
   dsimp only
-  rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry)]
+  rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderCarry) (LawfulOperator.lt_size_of_lt_aig_size aig input hstart)]
   rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)]
 
 theorem go_denote_mem_prefix (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
@@ -110,13 +110,11 @@ theorem go_get_aux (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref a
   split at hgo
   · rw [← hgo]
     intro hfoo
-    rw [go_get_aux]
-    rw [AIG.RefVec.get_push_ref_lt]
-    · simp only [Ref.cast, Ref.mk.injEq]
-      rw [AIG.RefVec.get_cast]
-      · simp
-      · assumption
-    · apply go_le_size
+    rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := go_le_size ..)]
+    rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)]
+    simp only [Ref.cast, Ref.mk.injEq]
+    rw [AIG.RefVec.get_cast]
+    simp
   · rw [← hgo]
     simp only [Nat.le_refl]
     obtain rfl : curr = w := by omega
@@ -196,9 +194,9 @@ theorem go_denote_eq (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref
         simp only [Ref.cast_eq, denote_projected_entry, denote_mkFullAdderCarry,
           FullAdderInput.lhs_cast, FullAdderInput.rhs_cast, FullAdderInput.cin_cast,
           BitVec.carry_succ]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)]
-        rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut)]
+        rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut) (h := Ref.hgate _)]
+        rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut) (h := Ref.hgate _)]
+        rw [AIG.LawfulOperator.denote_mem_prefix (f := mkFullAdderOut) (h := Ref.hgate _)]
         rw [hleft, hright, hcin]
         simp [atLeastTwo_eq_halfAdder]
       · omega
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
index d8c4f28172..6241193f62 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Extract.lean
@@ -37,7 +37,7 @@ theorem go_get_aux (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat)
   split at hgo
   · dsimp only at hgo
     rw [← hgo]
-    rw [go_get_aux]
+    rw [go_get_aux]; case hidx1 => omega
     rw [AIG.RefVec.get_push_ref_lt]
   · dsimp only at hgo
     rw [← hgo]
@@ -62,7 +62,7 @@ theorem go_get (aig : AIG α) (input : RefVec aig w) (lo : Nat) (curr : Nat)
   · rw [← hgo]
     cases Nat.eq_or_lt_of_le hidx2 with
     | inl heq =>
-      rw [go_get_aux]
+      rw [go_get_aux]; case hidx1 => omega
       rw [AIG.RefVec.get_push_ref_eq']
       · simp [heq]
       · simp [heq]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
index 7bfebb9856..d7e7b94940 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Mul.lean
@@ -61,7 +61,7 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤
       · intro idx hidx
         rw [BitVec.mulRec_succ_eq]
         have : rexpr.getLsbD (curr + 1) = false := by
-          rw [← hright]
+          rw [← hright _ ‹curr + 1 < w›]
           exact of_isConstant hconstant
         simp [this, hacc]
     · dsimp only at hgo
@@ -74,12 +74,18 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
         rw [hleft]
+        all_goals
+          repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+          exact Ref.hgate _
       · intro idx hidx
         simp only [RefVec.get_cast, Ref.cast_eq]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := RefVec.ite)]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
         rw [hright]
+        all_goals
+          repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+          exact Ref.hgate _
       · intro idx hidx
         rw [BitVec.mulRec_succ_eq]
         simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq, BitVec.ofNat_eq_ofNat]
@@ -90,11 +96,14 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤
             rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr
             rw [hright] at hdiscr
             exact hdiscr
+            all_goals
+              repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+              exact Ref.hgate _
           simp only [this, ↓reduceIte]
           rw [denote_blastAdd]
           · intros
             simp only [RefVec.get_cast, Ref.cast_eq]
-            rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
+            rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst) (h := Ref.hgate _)]
             rw [hacc]
           · intros
             simp only [denote_blastShiftLeftConst, BitVec.getLsbD_shiftLeft]
@@ -109,10 +118,16 @@ theorem go_denote_eq {w : Nat} (aig : AIG α) (curr : Nat) (hcurr : curr + 1 ≤
             rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)] at hdiscr
             rw [hright] at hdiscr
             simp [hdiscr]
+            all_goals
+              repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+              exact Ref.hgate _
           simp only [this, Bool.false_eq_true, ↓reduceIte, BitVec.add_zero]
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastAdd)]
           rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
           rw [hacc]
+          all_goals
+            repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+            exact Ref.hgate _
   · have : curr + 1 = w := by omega
     subst this
     rw [← hgo]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
index fa8c6c2484..9b1abb6d16 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
@@ -59,10 +59,9 @@ theorem go_get_aux (aig : AIG α) (n : Nat) (curr : Nat) (hcurr : curr ≤ n)
   unfold go
   split
   · dsimp only
-    rw [go_get_aux]
+    rw [go_get_aux]; case hidx => rw [Nat.mul_add]; omega
     rw [AIG.RefVec.get_append]
     simp only [hidx, ↓reduceDIte]
-    omega
   · dsimp only
     simp only [RefVec.get, Ref.mk.injEq]
     have : curr = n := by omega
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean
index 6e4cc79cd2..237a651f03 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateLeft.lean
@@ -39,9 +39,9 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
   split
   · dsimp only
     split
-    · rw [go_get_aux]
+    · rw [go_get_aux]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_lt]
-    · rw [go_get_aux]
+    · rw [go_get_aux]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_lt]
   · dsimp only
     simp only [RefVec.get, Ref.mk.injEq]
@@ -69,14 +69,14 @@ theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
     | inl heq =>
       split
       · split
-        · rw [go_get_aux]
+        · rw [go_get_aux]; case hidx => omega
           rw [AIG.RefVec.get_push_ref_eq']
           · simp [heq]
           · omega
         · omega
       · split
         · omega
-        · rw [go_get_aux]
+        · rw [go_get_aux]; case hidx => omega
           rw [AIG.RefVec.get_push_ref_eq']
           · simp [heq]
           · omega
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean
index 407e9738c8..fa6f5dcf29 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean
@@ -39,9 +39,9 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
   split
   · dsimp only
     split
-    · rw [go_get_aux]
+    · rw [go_get_aux]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_lt]
-    · rw [go_get_aux]
+    · rw [go_get_aux]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_lt]
   · dsimp only
     simp only [RefVec.get, Ref.mk.injEq]
@@ -70,14 +70,14 @@ theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
     | inl heq =>
       split
       · split
-        · rw [go_get_aux]
+        · rw [go_get_aux]; case hidx => omega
           rw [AIG.RefVec.get_push_ref_eq']
           · simp [heq]
           · omega
         · omega
       · split
         · omega
-        · rw [go_get_aux]
+        · rw [go_get_aux]; case hidx => omega
           rw [AIG.RefVec.get_push_ref_eq']
           · simp [heq]
           · omega
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
index 8ef4025859..166926819f 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
@@ -43,11 +43,11 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
     split at hgo
     · rw [← hgo]
       intros
-      rw [go_get_aux]
+      rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := ‹_›)]
       rw [AIG.RefVec.get_push_ref_lt]
     · rw [← hgo]
       intros
-      rw [go_get_aux]
+      rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := ‹_›)]
       rw [AIG.RefVec.get_push_ref_lt]
   · dsimp only at hgo
     rw [← hgo]
@@ -107,7 +107,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
       split at hgo
       · split
         · rw [← hgo]
-          rw [go_get]
+          rw [go_get]; case hidx => omega
           rw [AIG.RefVec.get_push_ref_eq']
           · rw [go_denote_mem_prefix]
             · simp only [Ref.cast_eq]
@@ -118,7 +118,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
       · split
         · omega
         · rw [← hgo]
-          rw [go_get]
+          rw [go_get]; case hidx => omega
           rw [AIG.RefVec.get_push_ref_eq']
           · rw [go_denote_mem_prefix]
             · simp [heq]
@@ -195,7 +195,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [← hg]
       simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq,
         denote_blastShiftLeftConst]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst) (h := Ref.hgate _)]
       rw [hright]
       simp only [hif1, ↓reduceIte]
       have hmod : 2 ^ pow % 2 ^ n = 2 ^ pow := by
@@ -218,10 +218,10 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [← hg]
       simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq,
         denote_blastShiftLeftConst]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst) (h := Ref.hgate _)]
       rw [hright]
       simp only [hif1, Bool.false_eq_true, ↓reduceIte]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftLeftConst) (h := Ref.hgate _)]
       rw [hleft]
       simp
   · have : rhs.getLsbD pow = false := by
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
index 91e36f8801..cc09e862d5 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
@@ -43,11 +43,11 @@ theorem go_get_aux (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
     split at hgo
     · rw [← hgo]
       intros
-      rw [go_get_aux]
+      rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := ‹_›)]
       rw [AIG.RefVec.get_push_ref_lt]
     · rw [← hgo]
       intros
-      rw [go_get_aux]
+      rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx) (hfoo := ‹_›)]
       rw [AIG.RefVec.get_push_ref_lt]
   · dsimp only at hgo
     rw [← hgo]
@@ -107,7 +107,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
       split at hgo
       · split
         · rw [← hgo]
-          rw [go_get]
+          rw [go_get]; case hidx => omega
           rw [AIG.RefVec.get_push_ref_eq']
           · rw [go_denote_mem_prefix]
             · simp [heq]
@@ -117,7 +117,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
       · split
         · omega
         · rw [← hgo]
-          rw [go_get]
+          rw [go_get]; case hidx => omega
           rw [AIG.RefVec.get_push_ref_eq']
           · rw [go_denote_mem_prefix]
             · simp only [Ref.cast_eq]
@@ -178,7 +178,7 @@ theorem go_get (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
   split
   · split
     all_goals
-      rw [go_get]
+      rw [go_get]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_lt]
   · simp only
     have : curr = w := by omega
@@ -213,7 +213,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
         simp only [hlt, ↓reduceDIte]
         dsimp only at hgo
         rw [← hgo]
-        rw [go_get]
+        rw [go_get]; case hidx => omega
         rw [AIG.RefVec.get_push_ref_eq']
         · simp [heq]
         · omega
@@ -222,7 +222,7 @@ theorem go_denote_eq (aig : AIG α) (distance : Nat) (input : AIG.RefVec aig w)
         simp only [hlt, ↓reduceDIte]
         dsimp only at hgo
         rw [← hgo]
-        rw [go_get]
+        rw [go_get]; case hidx => omega
         rw [AIG.RefVec.get_push_ref_eq']
         · simp [heq]
     | inr =>
@@ -285,7 +285,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [← hg]
       simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq,
         denote_blastShiftRightConst]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst) (h := Ref.hgate _)]
       rw [hright]
       simp only [hif1, ↓reduceIte]
       have hmod : 2 ^ pow % 2 ^ n = 2 ^ pow := by
@@ -303,10 +303,10 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [← hg]
       simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq,
         denote_blastShiftRightConst]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst) (h := Ref.hgate _)]
       rw [hright]
       simp only [hif1, Bool.false_eq_true, ↓reduceIte]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftRightConst) (h := Ref.hgate _)]
       rw [hleft]
       simp
   · have : rhs.getLsbD pow = false := by
@@ -418,7 +418,7 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [← hg]
       simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq,
         denote_blastArithShiftRightConst]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst) (h := Ref.hgate _)]
       rw [hright]
       simp only [hif1, ↓reduceIte]
       have hmod : 2 ^ pow % 2 ^ n = 2 ^ pow := by
@@ -436,10 +436,10 @@ theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs :
       rw [← hg]
       simp only [RefVec.denote_ite, RefVec.get_cast, Ref.cast_eq,
         denote_blastArithShiftRightConst]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst) (h := Ref.hgate _)]
       rw [hright]
       simp only [hif1, Bool.false_eq_true, ↓reduceIte]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastArithShiftRightConst) (h := Ref.hgate _)]
       rw [hleft]
       simp
   · have : rhs.getLsbD pow = false := by
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
index 9864f47499..00817da70c 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Udiv.lean
@@ -109,9 +109,16 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
       · simp [Std.Tactic.BVDecide.Normalize.BitVec.lt_ult]
       · intro idx hidx
         simp only [RefVec.get_cast, Ref.cast_eq]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h)]
+        case h =>
+          apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+          apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+          exact Ref.hgate _
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h)]
+        case h =>
+          apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+          exact Ref.hgate _
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := Ref.hgate _)]
         rw [denote_blastShiftConcat_eq_shiftConcat]
         · simp [hr]
         · rw [BVPred.denote_getD_eq_getLsbD]
@@ -125,11 +132,21 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
         · simp [hright]
         · simp [Ref.hgate]
+        all_goals
+          repeat apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+          exact Ref.hgate _
     · intro h
       simp only [RefVec.get_cast, Ref.cast_eq]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt) (h := ?h)]
+      case h =>
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        exact Ref.hgate _
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h)]
+      case h =>
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        exact Ref.hgate _
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := Ref.hgate _)]
       rw [denote_blastShiftConcat_eq_shiftConcat]
       · intro idx hidx
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
@@ -138,11 +155,18 @@ theorem denote_blastDivSubtractShift_q (aig : AIG α) (assign : α → Bool) (lh
       · rw [denote_mkConstCached]
     · intro h
       simp only [RefVec.get_cast, Ref.cast_eq]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
+      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt) (h := ?h)]
+      case h =>
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        exact Ref.hgate _
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := Ref.hgate _)]
       rw [denote_blastShiftConcat_eq_shiftConcat]
       · intro idx hidx
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h2)]
+        case h2 =>
+          simp only [RefVec.get_cast, Ref.cast_eq]
+          apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+          exact Ref.hgate _
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
         · simp [hq]
         · simp [Ref.hgate]
@@ -172,11 +196,29 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
     next hdiscr =>
       rw [← Normalize.BitVec.lt_ult] at hdiscr
       simp only [Ref.cast_eq, hdiscr, ↓reduceIte]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite) (h := ?h)]
+      case h =>
+        apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkUlt)
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        exact Ref.hgate _
+      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt) (h := ?h)]
+      case h =>
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        exact Ref.hgate _
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h)]
+      case h =>
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        exact Ref.hgate _
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h)]
+      case h =>
+        apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size
+        exact Ref.hgate _
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := Ref.hgate _)]
       rw [denote_blastShiftConcat_eq_shiftConcat]
       · intro idx hidx
         simp [hr]
@@ -186,27 +228,47 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
     next hdiscr =>
       rw [← Normalize.BitVec.lt_ult] at hdiscr
       simp only [Ref.cast_eq, hdiscr, ↓reduceIte]
-      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite)]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt)]
+      rw [AIG.LawfulVecOperator.denote_mem_prefix (f := AIG.RefVec.ite) (h := ?h2)]
+      case h2 =>
+        apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkUlt)
+        exact Ref.hgate _
+      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkUlt) (h := Ref.hgate _)]
       rw [denote_blastSub]
       · intro idx hidx
         simp only [RefVec.get_cast, Ref.cast_eq]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h2)]
+        case h2 =>
+          apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+          exact Ref.hgate _
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := Ref.hgate _)]
         rw [denote_blastShiftConcat_eq_shiftConcat]
         · simp [hr]
         · rw [BVPred.denote_getD_eq_getLsbD]
           · exact hleft
           · simp
       · intro idx hidx
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h3)]
+        case h3 =>
+          apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+          apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+          simp [Ref.hgate]
+        rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h3)]
+        case h3 =>
+          apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+          simp [Ref.hgate]
         rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
         · simp [hright]
         · simp [Ref.hgate]
   · intro idx hidx
-    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
-    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h4)]
+    case h4 =>
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+      simp [Ref.hgate]
+    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h4)]
+    case h4 =>
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+      simp [Ref.hgate]
     rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
     . simp only [Ref.cast_eq, RefVec.get_cast]
       rw [denote_blastShiftConcat_eq_shiftConcat]
@@ -217,9 +279,21 @@ theorem denote_blastDivSubtractShift_r (aig : AIG α) (assign : α → Bool) (lh
         · simp
     . simp [Ref.hgate]
   · intro idx hidx
-    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub)]
-    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
-    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
+    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastSub) (h := ?h5)]
+    case h5 =>
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+      simp [Ref.hgate]
+    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h5)]
+    case h5 =>
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+      simp [Ref.hgate]
+    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat) (h := ?h5)]
+    case h5 =>
+      apply AIG.LawfulVecOperator.lt_size_of_lt_aig_size (f := blastShiftConcat)
+      simp [Ref.hgate]
     rw [AIG.LawfulVecOperator.denote_mem_prefix (f := blastShiftConcat)]
     . simp [hright]
     . simp [Ref.hgate]
@@ -381,12 +455,15 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
     RefVec.get_cast]
   split
   next hdiscr =>
-    rw [blastUdiv.go_denote_mem_prefix] at hdiscr
+    rw [blastUdiv.go_denote_mem_prefix (hstart := Ref.hgate _)] at hdiscr
     rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr
     · simp only [beq_iff_eq] at hdiscr
       rw [hdiscr]
       rw [blastUdiv.go_denote_mem_prefix]
-      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
+      case hstart =>
+        apply LawfulOperator.le_size_of_le_aig_size (f := BVPred.mkEq)
+        exact Ref.hgate _
+      rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq) (h := Ref.hgate _)]
       rw [denote_blastConst]
       simp
     · intro idx hidx
@@ -394,7 +471,7 @@ theorem denote_blastUdiv (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
     · intro idx hidx
       simp
   next hdiscr =>
-    rw [blastUdiv.go_denote_mem_prefix] at hdiscr
+    rw [blastUdiv.go_denote_mem_prefix (hstart := Ref.hgate _)] at hdiscr
     rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr
     · have hzero : 0#w < rhs := by
         rw [Normalize.BitVec.zero_lt_iff_zero_neq]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
index e72f91dcef..c7e60a8a00 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Ult.lean
@@ -39,7 +39,8 @@ theorem mkUlt_denote_eq (aig : AIG α) (lhs rhs : BitVec w) (input : BinaryRefVe
   · simp
   · dsimp only
     intro idx hidx
-    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast.blastNot)]
+    rw [AIG.LawfulVecOperator.denote_mem_prefix (f := BVExpr.bitblast.blastNot) (h := ?h)]
+    case h => simp [Ref.hgate]
     apply hleft
   · dsimp only
     intro idx hidx
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
index 221539fa63..4e3fa65367 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Umod.lean
@@ -147,11 +147,14 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
     RefVec.get_cast]
   split
   next hdiscr =>
-    rw [blastUdiv.go_denote_mem_prefix] at hdiscr
+    rw [blastUdiv.go_denote_mem_prefix (hstart := Ref.hgate _)] at hdiscr
     rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr
     · simp only [beq_iff_eq] at hdiscr
       rw [hdiscr]
-      rw [blastUdiv.go_denote_mem_prefix]
+      rw [blastUdiv.go_denote_mem_prefix (hstart := ?h)]
+      case h =>
+        apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := BVPred.mkEq)
+        exact Ref.hgate _
       rw [AIG.LawfulOperator.denote_mem_prefix (f := BVPred.mkEq)]
       · simp [hleft]
       · simp [Ref.hgate]
@@ -162,7 +165,7 @@ theorem denote_blastUmod (aig : AIG α) (lhs rhs : BitVec w) (assign : α → Bo
       rw [denote_blastConst]
       simp
   next hdiscr =>
-    rw [blastUdiv.go_denote_mem_prefix] at hdiscr
+    rw [blastUdiv.go_denote_mem_prefix (hstart := Ref.hgate _)] at hdiscr
     rw [BVPred.mkEq_denote_eq (lhs := rhs) (rhs := 0#w)] at hdiscr
     · have hzero : 0#w < rhs := by
         rw [Normalize.BitVec.zero_lt_iff_zero_neq]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
index b4b2f61a93..2b720eef66 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
@@ -40,12 +40,12 @@ theorem go_get_aux (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWidth
   · dsimp only at hgo
     split at hgo
     · rw [← hgo]
-      intros
-      rw [go_get_aux]
+      intro hfoo
+      rw [go_get_aux (hfoo := hfoo)]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_lt]
     · rw [← hgo]
-      intros
-      rw [go_get_aux]
+      intro hfoo
+      rw [go_get_aux (hfoo := hfoo)]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_lt]
   · dsimp only at hgo
     rw [← hgo]
@@ -108,7 +108,7 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid
         rw [heq] at hsplit
         simp only [hsplit, ↓reduceDIte]
         rw [← hgo]
-        rw [go_get]
+        rw [go_get]; case hidx => omega
         rw [AIG.RefVec.get_push_ref_eq']
         · rw [go_denote_mem_prefix]
           · simp [heq]
@@ -118,7 +118,7 @@ theorem go_denote_eq (aig : AIG α) (w : Nat) (input : AIG.RefVec aig w) (newWid
         rw [heq] at hsplit
         simp only [hsplit, ↓reduceDIte]
         rw [← hgo]
-        rw [go_get]
+        rw [go_get]; case hidx => omega
         rw [AIG.RefVec.get_push_ref_eq']
         · rw [go_denote_mem_prefix]
           · simp only [Ref.cast_eq]
diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
index a24a5e5a27..42e62b9406 100644
--- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
+++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Var.lean
@@ -39,12 +39,11 @@ theorem go_get_aux (aig : AIG BVBit) (a : Nat) (curr : Nat) (hcurr : curr ≤ w)
   · dsimp only at hgo
     rw [← hgo]
     intro hfoo
-    rw [go_get_aux]
-    rw [AIG.RefVec.get_push_ref_lt]
+    rw [go_get_aux (hidx := Nat.lt_succ_of_lt hidx)]
+    rw [AIG.RefVec.get_push_ref_lt (hidx := hidx)]
     · simp only [Ref.cast, Ref.mk.injEq]
       rw [AIG.RefVec.get_cast]
-      · simp
-      · assumption
+      simp
     · apply go_le_size
   · dsimp only at hgo
     rw [← hgo]
@@ -99,7 +98,7 @@ theorem go_denote_eq (aig : AIG BVBit) (a : Nat) (assign : Assignment) (curr : N
     cases Nat.eq_or_lt_of_le hidx2 with
     | inl heq =>
       rw [← hgo]
-      rw [go_get]
+      rw [go_get]; case hidx => omega
       rw [AIG.RefVec.get_push_ref_eq']
       · rw [← heq]
         rw [go_denote_mem_prefix]
diff --git a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
index aa473f7cc7..400609f9b1 100644
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -175,7 +175,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩
           simp only [insertUnit, h5, ite_false, reduceCtorEq]
           constructor
-          · rw [Array.getElem_push_lt, h1]
+          · rw [Array.getElem_push_lt j.2, h1]
           · constructor
             · simp +zetaDelta [i_eq_l, ← hl]
               rfl
@@ -215,7 +215,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
           · simp +zetaDelta [i_eq_l, ← hl]
             rfl
           · constructor
-            · rw [Array.getElem_push_lt, h1]
+            · rw [Array.getElem_push_lt j.2, h1]
             · constructor
               · simp only [i_eq_l]
                 rw [Array.getElem_modify_self]
@@ -258,7 +258,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
         refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
         simp only [insertUnit, h5, ite_false, reduceCtorEq]
         constructor
-        · rw [Array.getElem_push_lt, h1]
+        · rw [Array.getElem_push_lt j.2, h1]
         · constructor
           · grind
           · constructor
diff --git a/tests/lean/run/10172.lean b/tests/lean/run/10172.lean
new file mode 100644
index 0000000000..d05c5da9fc
--- /dev/null
+++ b/tests/lean/run/10172.lean
@@ -0,0 +1,33 @@
+/-!
+# Rewrite tactic "steals" goals
+-/
+
+
+/-!
+https://github.com/leanprover/lean4/issues/10172
+
+There were two metaprogramming bugs:
+- `rw` didn't filter old vs new metavariables when coming up with new goals.
+- it also didn't make the new metavariables be synthetic opaque, so the old one was
+  being assigned, even with old vs new filtering.
+-/
+example (l m : List Nat) (i : Nat) (hi' : i < (l ++ m).length)
+    (hh : ∀ hi, l[i]'hi = 5) : (l ++ m)[i] = 5 := by
+  rw [List.getElem_append_left]
+  · rw [hh] -- used to be Error: unsolved goal `i < l.length`
+  · sorry -- used to be Error: No goals to be solved
+
+/-!
+While we're here, we could address a missing occurs check.
+
+https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/rewrite.20with.20the.20goal/near/538108360
+-/
+/--
+error: Occurs check failed: Expression
+  ?k
+contains the goal ?k
+-/
+#guard_msgs in
+example : 1 = 2 := by
+  refine ?k
+  rw [?k]