-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Var.lean
theorem blastVar.go_decl_eq {aig : AIG BVBit} (curr : Nat) (s : AIG.RefVec aig curr) (a : Nat)
    (hcurr : curr ≤ w) :
    ∀ (idx : Nat) (h1) (h2), (go aig w a curr s hcurr).aig.decls[idx]'h2 = aig.decls[idx]'h1

Proof state:
case isTrue
w : Nat
aig : AIG BVBit
curr✝ : Nat
s : aig.RefVec curr✝
a : Nat
hcurr : curr✝ ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : curr✝ < w
hgo :
  go (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig w a (curr✝ + 1)
      ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).ref) ⋯ =
    res
curr : Nat
h1 : curr < aig.decls.size
h2 :
  curr <
    (go (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig w a (curr✝ + 1)
            ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).ref) ⋯).aig.decls.size
⊢ (go (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig w a (curr✝ + 1)
            ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).ref) ⋯).aig.decls[curr] =
    aig.decls[curr]

Tactic:
rw [blastVar.go_decl_eq]

Result:
case isTrue
w : Nat
aig : AIG BVBit
curr✝ : Nat
s : aig.RefVec curr✝
a : Nat
hcurr : curr✝ ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : curr✝ < w
hgo :
  go (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig w a (curr✝ + 1)
      ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).ref) ⋯ =
    res
curr : Nat
h1 : curr < aig.decls.size
h2 :
  curr <
    (go (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig w a (curr✝ + 1)
            ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).ref) ⋯).aig.decls.size
⊢ (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig.decls[curr] = aig.decls[curr]

case isTrue.h1
w : Nat
aig : AIG BVBit
curr✝ : Nat
s : aig.RefVec curr✝
a : Nat
hcurr : curr✝ ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : curr✝ < w
hgo :
  go (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig w a (curr✝ + 1)
      ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).ref) ⋯ =
    res
curr : Nat
h1 : curr < aig.decls.size
h2 :
  curr <
    (go (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig w a (curr✝ + 1)
            ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).ref) ⋯).aig.decls.size
⊢ curr < (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig.decls.size

Proof state:
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig w a curr s hcurr).aig.decls.size),
    (go aig w a curr s hcurr).aig.decls[idx] = aig.decls[idx]

Tactic:
generalize hgo : go aig w a curr s hcurr = res

Result:
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
hgo : go aig w a curr s hcurr = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Proof state:
case isFalse
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : ¬curr < w
hgo : { aig := aig, vec := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < { aig := aig, vec := ⋯ ▸ s }.aig.decls.size),
    { aig := aig, vec := ⋯ ▸ s }.aig.decls[idx] = aig.decls[idx]

Tactic:
intros

Result:
case isFalse
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : ¬curr < w
hgo : { aig := aig, vec := ⋯ ▸ s } = res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ : idx✝ < { aig := aig, vec := ⋯ ▸ s }.aig.decls.size
⊢ { aig := aig, vec := ⋯ ▸ s }.aig.decls[idx✝] = aig.decls[idx✝]

Proof state:
case isTrue
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : curr < w
hgo :
  (let res := aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.push bitRef;
    go aig_1 w a (curr + 1) s ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
dsimp only at hgo

Result:
case isTrue
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : curr < w
hgo :
  go (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig w a (curr + 1)
      ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) ⋯ =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Proof state:
case isTrue.h2.h
w : Nat
aig : AIG BVBit
curr✝ : Nat
s : aig.RefVec curr✝
a : Nat
hcurr : curr✝ ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : curr✝ < w
hgo :
  go (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig w a (curr✝ + 1)
      ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).ref) ⋯ =
    res
curr : Nat
h1 : curr < aig.decls.size
h2 :
  curr <
    (go (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).aig w a (curr✝ + 1)
            ((s.cast ⋯).push (aig.mkAtomCached (BVBit.mk a ⟨curr✝, h✝⟩)).ref) ⋯).aig.decls.size
⊢ curr < aig.decls.size

Tactic:
assumption

Result:
no goals

Proof state:
case isFalse
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : ¬curr < w
hgo : { aig := aig, vec := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
rw [← hgo]

Result:
case isFalse
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : ¬curr < w
hgo : { aig := aig, vec := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < { aig := aig, vec := ⋯ ▸ s }.aig.decls.size),
    { aig := aig, vec := ⋯ ▸ s }.aig.decls[idx] = aig.decls[idx]

Proof state:
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
hgo :
  (if hcurr : curr < w then
      let res := aig.mkAtomCached (BVBit.mk a ⟨curr, hcurr⟩);
      let aig_1 := res.aig;
      let bitRef := res.ref;
      let s := s.cast ⋯;
      let s := s.push bitRef;
      go aig_1 w a (curr + 1) s ⋯
    else
      let_fun hcurr := ⋯;
      { aig := aig, vec := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

Tactic:
split at hgo

Result:
case isTrue
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : curr < w
hgo :
  (let res := aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.push bitRef;
    go aig_1 w a (curr + 1) s ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
w : Nat
aig : AIG BVBit
curr : Nat
s : aig.RefVec curr
a : Nat
hcurr : curr ≤ w
res : AIG.RefVecEntry BVBit w
h✝ : ¬curr < w
hgo :
  (let_fun hcurr := ⋯;
    { aig := aig, vec := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]