-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
theorem twoPowShift_eq (aig : AIG α) (target : TwoPowShiftTarget aig w) (lhs : BitVec w)
    (rhs : BitVec target.n) (assign : α → Bool)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, target.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w),
        ⟦
          (twoPowShift aig target).aig,
          (twoPowShift aig target).vec.get idx hidx,
          assign
        ⟧
          =
        (BitVec.sshiftRight' lhs (rhs &&& BitVec.twoPow target.n target.pow)).getLsbD idx

Proof state:
case mk.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs : BitVec w
assign : α → Bool
idx : Nat
hidx : idx < w
res : RefVecEntry α w
n : Nat
lvec : aig.RefVec w
rvec : aig.RefVec n
pow : Nat
rhs : BitVec { n := n, lhs := lvec, rhs := rvec, pow := pow }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, lhs := lvec, rhs := rvec, pow := pow }.n),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h✝ : ¬pow < n
hg : { aig := aig, vec := lvec } = res
this : rhs.getLsbD pow = false
⊢ ⟦assign, { aig := { aig := aig, vec := lvec }.aig, ref := { aig := aig, vec := lvec }.vec.get idx hidx }⟧ =
    (lhs.sshiftRight' 0#n).getLsbD idx

Tactic:
rw [hleft]

Result:
case mk.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs : BitVec w
assign : α → Bool
idx : Nat
hidx : idx < w
res : RefVecEntry α w
n : Nat
lvec : aig.RefVec w
rvec : aig.RefVec n
pow : Nat
rhs : BitVec { n := n, lhs := lvec, rhs := rvec, pow := pow }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, lhs := lvec, rhs := rvec, pow := pow }.n),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h✝ : ¬pow < n
hg : { aig := aig, vec := lvec } = res
this : rhs.getLsbD pow = false
⊢ lhs.getLsbD idx = (lhs.sshiftRight' 0#n).getLsbD idx

Proof state:
case mk.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs : BitVec w
assign : α → Bool
idx : Nat
hidx : idx < w
res : RefVecEntry α w
n : Nat
lvec : aig.RefVec w
rvec : aig.RefVec n
pow : Nat
rhs : BitVec { n := n, lhs := lvec, rhs := rvec, pow := pow }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, lhs := lvec, rhs := rvec, pow := pow }.n),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h✝ : ¬pow < n
hg : { aig := aig, vec := lvec } = res
this : rhs.getLsbD pow = false
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ = (lhs.sshiftRight' 0#n).getLsbD idx

Tactic:
rw [← hg]

Result:
case mk.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs : BitVec w
assign : α → Bool
idx : Nat
hidx : idx < w
res : RefVecEntry α w
n : Nat
lvec : aig.RefVec w
rvec : aig.RefVec n
pow : Nat
rhs : BitVec { n := n, lhs := lvec, rhs := rvec, pow := pow }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, lhs := lvec, rhs := rvec, pow := pow }.n),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h✝ : ¬pow < n
hg : { aig := aig, vec := lvec } = res
this : rhs.getLsbD pow = false
⊢ ⟦assign, { aig := { aig := aig, vec := lvec }.aig, ref := { aig := aig, vec := lvec }.vec.get idx hidx }⟧ =
    (lhs.sshiftRight' 0#n).getLsbD idx

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs : BitVec w
assign : α → Bool
idx : Nat
hidx : idx < w
res : RefVecEntry α w
n : Nat
lvec : aig.RefVec w
rvec : aig.RefVec n
pow : Nat
rhs : BitVec { n := n, lhs := lvec, rhs := rvec, pow := pow }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, lhs := lvec, rhs := rvec, pow := pow }.n),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.rhs.get idx hidx }⟧ = rhs.getLsbD idx
hg :
  (match { n := n, lhs := lvec, rhs := rvec, pow := pow } with
    | { n := n, lhs := lhs, rhs := rhs, pow := pow } =>
      if h : pow < n then
        let res := blastArithShiftRightConst aig { vec := lhs, distance := 2 ^ pow };
        let aig_1 := res.aig;
        let shifted := res.vec;
        let_fun this := ⋯;
        let rhs := rhs.cast this;
        let lhs_1 := lhs.cast this;
        RefVec.ite aig_1 { discr := rhs.get pow h, lhs := shifted, rhs := lhs_1 }
      else { aig := aig, vec := lhs }) =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (lhs.sshiftRight' (if rhs.getLsbD pow = true then BitVec.twoPow n pow else 0#n)).getLsbD idx

Tactic:
dsimp only at hg

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs : BitVec w
assign : α → Bool
idx : Nat
hidx : idx < w
res : RefVecEntry α w
n : Nat
lvec : aig.RefVec w
rvec : aig.RefVec n
pow : Nat
rhs : BitVec { n := n, lhs := lvec, rhs := rvec, pow := pow }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, lhs := lvec, rhs := rvec, pow := pow }.n),
    ⟦assign, { aig := aig, ref := { n := n, lhs := lvec, rhs := rvec, pow := pow }.rhs.get idx hidx }⟧ = rhs.getLsbD idx
hg :
  (if h : pow < n then
      RefVec.ite (blastArithShiftRightConst aig { vec := lvec, distance := 2 ^ pow }).aig
        { discr := (rvec.cast ⋯).get pow h,
          lhs := (blastArithShiftRightConst aig { vec := lvec, distance := 2 ^ pow }).vec, rhs := lvec.cast ⋯ }
    else { aig := aig, vec := lvec }) =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (lhs.sshiftRight' (if rhs.getLsbD pow = true then BitVec.twoPow n pow else 0#n)).getLsbD idx