-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
theorem go_denote_eq (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
      (hcurr : curr ≤ n - 1) (acc : AIG.RefVec aig w)
    (lhs : BitVec w) (rhs : BitVec n) (assign : α → Bool)
    (hacc : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, acc.get idx hidx, assign⟧ = (BitVec.ushiftRightRec lhs rhs curr).getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < n), ⟦aig, distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (go aig distance curr acc).aig,
          (go aig distance curr acc).vec.get idx hidx,
          assign
        ⟧
          =
        (BitVec.ushiftRightRec lhs rhs (n - 1)).getLsbD idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
hcurr : curr ≤ n - 1
acc : aig.RefVec w
lhs : BitVec w
rhs : BitVec n
assign : α → Bool
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.ushiftRightRec rhs curr).getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := (go aig distance curr acc).aig, ref := (go aig distance curr acc).vec.get idx hidx }⟧ =
    (lhs.ushiftRightRec rhs (n - 1)).getLsbD idx

Tactic:
generalize hgo : go aig distance curr acc = res

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
hcurr : curr ≤ n - 1
acc : aig.RefVec w
lhs : BitVec w
rhs : BitVec n
assign : α → Bool
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.ushiftRightRec rhs curr).getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry α w
hgo : go aig distance curr acc = res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs.ushiftRightRec rhs (n - 1)).getLsbD idx

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
hcurr : curr ≤ n - 1
acc : aig.RefVec w
lhs : BitVec w
rhs : BitVec n
assign : α → Bool
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.ushiftRightRec rhs curr).getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
⊢ ⟦assign,
      {
        aig :=
          (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯)
              (curr + 1) (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig,
        ref :=
          (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯)
                  (curr + 1) (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).vec.get
            idx hidx }⟧ =
    (lhs.ushiftRightRec rhs (n - 1)).getLsbD idx

Tactic:
rw [go_denote_eq]

Result:
case isTrue.hcurr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
hcurr : curr ≤ n - 1
acc : aig.RefVec w
lhs : BitVec w
rhs : BitVec n
assign : α → Bool
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.ushiftRightRec rhs curr).getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
⊢ curr + 1 ≤ n - 1

case isTrue.hacc
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
hcurr : curr ≤ n - 1
acc : aig.RefVec w
lhs : BitVec w
rhs : BitVec n
assign : α → Bool
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.ushiftRightRec rhs curr).getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign,
        { aig := (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig,
          ref := (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec.get idx hidx }⟧ =
      (lhs.ushiftRightRec rhs (curr + 1)).getLsbD idx

case isTrue.hright
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
hcurr : curr ≤ n - 1
acc : aig.RefVec w
lhs : BitVec w
rhs : BitVec n
assign : α → Bool
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.ushiftRightRec rhs curr).getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry α w
h✝ : curr < n - 1
hgo :
  go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
      (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec =
    res
⊢ ∀ (idx : Nat) (hidx : idx < n),
    ⟦assign,
        { aig := (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig,
          ref := (distance.cast ⋯).get idx hidx }⟧ =
      rhs.getLsbD idx

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
hcurr : curr ≤ n - 1
acc : aig.RefVec w
lhs : BitVec w
rhs : BitVec n
assign : α → Bool
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.ushiftRightRec rhs curr).getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry α w
h✝ : ¬curr < n - 1
hgo : { aig := aig, vec := acc } = res
this : curr = n - 1
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs.ushiftRightRec rhs (n - 1)).getLsbD idx

Tactic:
rw [← hgo]

Result:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
hcurr : curr ≤ n - 1
acc : aig.RefVec w
lhs : BitVec w
rhs : BitVec n
assign : α → Bool
hacc :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := acc.get idx hidx }⟧ = (lhs.ushiftRightRec rhs curr).getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < n), ⟦assign, { aig := aig, ref := distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
res : RefVecEntry α w
h✝ : ¬curr < n - 1
hgo : { aig := aig, vec := acc } = res
this : curr = n - 1
⊢ ⟦assign, { aig := { aig := aig, vec := acc }.aig, ref := { aig := aig, vec := acc }.vec.get idx hidx }⟧ =
    (lhs.ushiftRightRec rhs (n - 1)).getLsbD idx