fix: make rw collect only new goals, occurs check (#10306)

This PR fixes a few bugs in the `rw` tactic: it could "steal" goals because they appear in the type of the rewrite, it did not do an occurs check, and new proof goals would not be synthetic opaque. This PR also lets the `rfl` tactic assign synthetic opaque metavariables so that it is equivalent to `exact rfl`. Implementation note: filtering old vs new is not sufficient. This PR partially addresses the bug where the rw tactic creates natural metavariables for each of the goals; now new proof goals are synthetic opaque. Metaprogramming API: Instead of `Lean.MVarId.rewrite` prefer `Lean.Elab.Tactic.elabRewrite` for elaborating rewrite theorems and applying rewrites to expressions. Closes #10172
2025-09-13 21:44:55 -07:00 · 2025-09-13 21:44:55 -07:00 · 409cbe1da9
commit 409cbe1da9
parent 3e4fa12c72
33 changed files with 339 additions and 186 deletions
--- 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]
--- 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
--- 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
--- 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))
--- 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
--- 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
--- 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)

--- 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 :=
--- 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
--- 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
--- 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
--- 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]
--- 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]
--- 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
--- 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

--- 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
--- 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
--- 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 =>
--- 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
--- 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]
--- 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]
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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]
--- 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
--- 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]
--- 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]
--- 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]
--- 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
--- a/tests/lean/run/10172.lean
+++ 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]