Theorem: BVExpr.bitblast.blastVar.go_getRef_aux
Proof state before:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref).getRef idx ?isTrue.hidx).cast ?isTrue.hfoo =
    (s.getRef idx hidx).cast hfoo

case isTrue.hidx
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ idx < curr + 1

case isTrue.hfoo
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
Tactic:
rw [AIG.RefStream.getRef_push_ref_lt]
Proof state after:
case isTrue
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ ((s.cast ⋯).getRef idx ?isTrue.hidx).cast ?isTrue.hfoo = (s.getRef idx hidx).cast hfoo

case isTrue.hidx
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ idx < curr

case isTrue.hfoo
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size

case isTrue.hfoo
w : Nat
aig : AIG BVBit
a curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry BVBit w
h✝ : curr < w
hgo :
  go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
      ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size
⊢ (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig.decls.size ≤
    (go w (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).aig (curr + 1)
            ((s.cast ⋯).pushRef (aig.mkAtomCached (BVBit.mk a ⟨curr, h✝⟩)).ref) a ⋯).aig.decls.size