-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/RotateRight.lean
theorem denote_blastRotateRight (aig : AIG α) (target : ShiftTarget aig w)
  (assign : α → Bool) :
  ∀ (idx : Nat) (hidx : idx < w),
      ⟦
        (blastRotateRight aig target).aig,
        (blastRotateRight aig target).vec.get idx hidx,
        assign
      ⟧
        =
      if hidx2 : idx < w - target.distance % w then
        ⟦aig, target.vec.get ((target.distance % w) + idx) (by omega), assign⟧
      else
        ⟦aig, target.vec.get (idx - (w - (target.distance % w))) (by omega), assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign,
      {
        aig :=
          (match target with
            | { vec := input, distance := distance } =>
              { aig := aig, vec := blastRotateRight.go input distance 0 ⋯ RefVec.empty }).aig,
        ref :=
          (match target with
                | { vec := input, distance := distance } =>
                  { aig := aig, vec := blastRotateRight.go input distance 0 ⋯ RefVec.empty }).vec.get
            idx✝ hidx✝ }⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx✝) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := aig, ref := (blastRotateRight.go target.vec target.distance 0 ⋯ RefVec.empty).get idx✝ hidx✝ }⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx✝) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧

Proof state:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx : Nat
hidx : idx < w
hidx2 : ¬idx < w - target.distance % w
⊢ idx - (w - target.distance % w) < w

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := aig, ref := (blastRotateRight.go target.vec target.distance 0 ⋯ RefVec.empty).get idx✝ hidx✝ }⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx✝) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧

Tactic:
rw [blastRotateRight.go_get]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign,
      { aig := aig,
        ref :=
          if hidx3 : idx✝ < w - target.distance % w then target.vec.get (target.distance % w + idx✝) ⋯
          else target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx✝) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧

case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ 0 ≤ idx✝

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign,
      { aig := aig,
        ref :=
          if hidx3 : idx✝ < w - target.distance % w then target.vec.get (target.distance % w + idx✝) ⋯
          else target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx✝) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧

Tactic:
split <;> simp

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx : Nat
hidx : idx < w
hidx2 : idx < w - target.distance % w
⊢ target.distance % w + idx < w

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := (blastRotateRight aig target).aig, ref := (blastRotateRight aig target).vec.get idx hidx }⟧ =
      if hidx2 : idx < w - target.distance % w then
        ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx) ⋯ }⟧
      else ⟦assign, { aig := aig, ref := target.vec.get (idx - (w - target.distance % w)) ⋯ }⟧

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := (blastRotateRight aig target).aig, ref := (blastRotateRight aig target).vec.get idx✝ hidx✝ }⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx✝) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign, { aig := (blastRotateRight aig target).aig, ref := (blastRotateRight aig target).vec.get idx✝ hidx✝ }⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx✝) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧

Tactic:
unfold blastRotateRight

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
target : aig.ShiftTarget w
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < w
⊢ ⟦assign,
      {
        aig :=
          (match target with
            | { vec := input, distance := distance } =>
              { aig := aig, vec := blastRotateRight.go input distance 0 ⋯ RefVec.empty }).aig,
        ref :=
          (match target with
                | { vec := input, distance := distance } =>
                  { aig := aig, vec := blastRotateRight.go input distance 0 ⋯ RefVec.empty }).vec.get
            idx✝ hidx✝ }⟧ =
    if hidx2 : idx✝ < w - target.distance % w then
      ⟦assign, { aig := aig, ref := target.vec.get (target.distance % w + idx✝) ⋯ }⟧
    else ⟦assign, { aig := aig, ref := target.vec.get (idx✝ - (w - target.distance % w)) ⋯ }⟧