-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/SignExtend.lean
theorem go_get (aig : AIG α) (w : Nat) (hw : 0 < w) (input : RefVec aig w) (newWidth : Nat)
    (curr : Nat) (hcurr : curr ≤ newWidth) (s : RefVec aig curr) :
    ∀ (idx : Nat) (hidx1 : idx < newWidth),
        curr ≤ idx
          →
        (go w hw input newWidth curr hcurr s).get idx hidx1
          =
        if hidx2 : idx < w then
          input.get idx (by omega)
        else
          input.get (w - 1) (by omega)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (go w hw input newWidth curr hcurr✝ s).get idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Tactic:
unfold go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (if hcurr1 : curr < newWidth then
          if hcurr2 : curr < w then
            let s := s.push (input.get curr hcurr2);
            go w hw input newWidth (curr + 1) ⋯ s
          else
            let s := s.push (input.get (w - 1) ⋯);
            go w hw input newWidth (curr + 1) ⋯ s
        else
          let_fun hcurr := ⋯;
          hcurr ▸ s).get
      idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Proof state:
case inr.isFalse.a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr < idx
h✝ : ¬curr < w
⊢ curr + 1 ≤ idx

Tactic:
omega

Result:
no goals

Proof state:
case inr.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr < idx
h✝ : ¬curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get (w - 1) ⋯))).get idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Tactic:
rw [go_get]

Result:
case inr.isFalse.a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr < idx
h✝ : ¬curr < w
⊢ curr + 1 ≤ idx

Proof state:
case inl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr = idx
⊢ (if h : curr < w then go w hw input newWidth (curr + 1) ⋯ (s.push (input.get curr ⋯))
        else go w hw input newWidth (curr + 1) ⋯ (s.push (input.get (w - 1) ⋯))).get
      idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Tactic:
simp only [heq]

Result:
case inl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr = idx
⊢ (if h : idx < w then go w hw input newWidth (curr + 1) ⋯ (s.push (input.get idx ⋯))
        else go w hw input newWidth (curr + 1) ⋯ (s.push (input.get (w - 1) ⋯))).get
      idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Proof state:
case inr.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr < idx
h✝ : curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get curr ⋯))).get idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

case inr.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr < idx
h✝ : ¬curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get (w - 1) ⋯))).get idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Tactic:
all_goals
  rw [go_get]
  omega

Result:
no goals

Proof state:
case inr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr < idx
⊢ (if h : curr < w then go w hw input newWidth (curr + 1) ⋯ (s.push (input.get curr ⋯))
        else go w hw input newWidth (curr + 1) ⋯ (s.push (input.get (w - 1) ⋯))).get
      idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Tactic:
split

Result:
case inr.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr < idx
h✝ : curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get curr ⋯))).get idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

case inr.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
this : curr < newWidth
heq : curr < idx
h✝ : ¬curr < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get (w - 1) ⋯))).get idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hidx2 : ¬idx < w
⊢ w - 1 < w

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr : curr ≤ newWidth
s : aig.RefVec curr
⊢ ∀ (idx : Nat) (hidx1 : idx < newWidth),
    curr ≤ idx →
      (go w hw input newWidth curr hcurr s).get idx hidx1 =
        if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯

Tactic:
intro idx hidx1 hcurr

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
w : Nat
hw : 0 < w
input : aig.RefVec w
newWidth curr : Nat
hcurr✝ : curr ≤ newWidth
s : aig.RefVec curr
idx : Nat
hidx1 : idx < newWidth
hcurr : curr ≤ idx
⊢ (go w hw input newWidth curr hcurr✝ s).get idx hidx1 =
    if hidx2 : idx < w then input.get idx ⋯ else input.get (w - 1) ⋯