-- 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:
case inl.isFalse.hidx
α : 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✝ : ¬idx < w
⊢ idx = curr

Tactic:
rw [heq]

Result:
no goals

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 : 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) ⋯

Tactic:
split

Result:
case inl.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✝ : idx < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get idx ⋯))).get idx hidx1 = input.get idx ⋯

case inl.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✝ : ¬idx < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get (w - 1) ⋯))).get idx hidx1 = 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
hcurr : curr ≤ idx
this : curr < newWidth
⊢ (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:
cases Nat.eq_or_lt_of_le hcurr with
| inl heq =>
  simp only [heq]
  split
  all_goals
    rw [go_get_aux]
    rw [AIG.RefVec.get_push_ref_eq']
    rw [heq]
| inr heq =>
  split
  all_goals
    rw [go_get]
    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
hcurr : curr ≤ idx
this : curr < newWidth
⊢ (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) ⋯

Tactic:
simp only [this, ↓reduceDIte]

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
this : curr < newWidth
⊢ (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) ⋯

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
⊢ curr < newWidth

Tactic:
omega

Result:
no goals

Proof state:
case inl.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✝ : idx < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get idx ⋯))).get idx hidx1 = input.get idx ⋯

case inl.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✝ : ¬idx < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get (w - 1) ⋯))).get idx hidx1 = input.get (w - 1) ⋯

Tactic:
all_goals
  rw [go_get_aux]
  rw [AIG.RefVec.get_push_ref_eq']
  rw [heq]

Result:
no goals

Proof state:
case inl.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✝ : ¬idx < w
⊢ (go w hw input newWidth (curr + 1) ⋯ (s.push (input.get (w - 1) ⋯))).get idx hidx1 = input.get (w - 1) ⋯

Tactic:
rw [go_get_aux]

Result:
case inl.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✝ : ¬idx < w
⊢ (s.push (input.get (w - 1) ⋯)).get idx ?inl.isFalse.hidx1 = input.get (w - 1) ⋯

case inl.isFalse.hidx1
α : 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✝ : ¬idx < w
⊢ idx < curr + 1

Proof state:
case inl.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✝ : ¬idx < w
⊢ (s.push (input.get (w - 1) ⋯)).get idx ?inl.isFalse.hidx1 = input.get (w - 1) ⋯

case inl.isFalse.hidx1
α : 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✝ : ¬idx < w
⊢ idx < curr + 1

Tactic:
rw [AIG.RefVec.get_push_ref_eq']

Result:
case inl.isFalse.hidx
α : 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✝ : ¬idx < w
⊢ idx = curr

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
⊢ idx < w

Tactic:
omega

Result:
no goals