Theorem: BVExpr.bitblast.blastAdd.go_decl_eq (LeanSAT/Reflect/BVExpr/BitBlast/Impl/Add.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig curr hcurr cin s lhs rhs).aig.decls.size),
    (go aig curr hcurr cin s lhs rhs).aig.decls[idx] = aig.decls[idx]
Tactic:
generalize hgo : go aig curr hcurr cin s lhs rhs = res
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo : go aig curr hcurr cin s lhs rhs = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo : go aig curr hcurr cin s lhs rhs = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
unfold go at hgo
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      let lin := lhs.getRef curr hidx;
      let rin := rhs.getRef curr hidx;
      let res := mkFullAdder aig { lhs := lin, rhs := rin, cin := cin };
      let aig_1 := res.aig;
      let outRef := res.out;
      let carryRef := res.cout;
      let s := s.cast ⋯;
      let lhs := lhs.cast ⋯;
      let rhs := rhs.cast ⋯;
      let s := s.pushRef outRef;
      go aig_1 (curr + 1) ⋯ carryRef s lhs rhs
    else
      let_fun hcurr := ⋯;
      { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      let lin := lhs.getRef curr hidx;
      let rin := rhs.getRef curr hidx;
      let res := mkFullAdder aig { lhs := lin, rhs := rin, cin := cin };
      let aig_1 := res.aig;
      let outRef := res.out;
      let carryRef := res.cout;
      let s := s.cast ⋯;
      let lhs := lhs.cast ⋯;
      let rhs := rhs.cast ⋯;
      let s := s.pushRef outRef;
      go aig_1 (curr + 1) ⋯ carryRef s lhs rhs
    else
      let_fun hcurr := ⋯;
      { aig := aig, stream := hcurr ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
dsimp at hgo
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      go (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig (curr + 1) ⋯
        (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).cout
        ((s.cast ⋯).pushRef
          (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).out)
        (lhs.cast ⋯) (rhs.cast ⋯)
    else { aig := aig, stream := ⋯ ▸ s }) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      go (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).aig (curr + 1) ⋯
        (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).cout
        ((s.cast ⋯).pushRef
          (mkFullAdder aig { lhs := lhs.getRef curr hidx, rhs := rhs.getRef curr hidx, cin := cin }).out)
        (lhs.cast ⋯) (rhs.cast ⋯)
    else { aig := aig, stream := ⋯ ▸ 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
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ 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]
  intros
  rw [go_decl_eq]
  unfold mkFullAdder
  rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry)]
  rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderOut)]
  . apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
    assumption
  . apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry)
    apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
    assumption
State after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
. simp [← hgo]
State after:
no goals

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
rw [← hgo]
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
                (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
                ((s.cast ⋯).pushRef
                  (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
                (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size),
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
              ((s.cast ⋯).pushRef
                (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
              (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls[idx] =
      aig.decls[idx]

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size)
    (h2 :
      idx <
        (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
                (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
                ((s.cast ⋯).pushRef
                  (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
                (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size),
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
              ((s.cast ⋯).pushRef
                (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
              (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls[idx] =
      aig.decls[idx]
Tactic:
intros
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls[idx✝] =
    aig.decls[idx✝]

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls[idx✝] =
    aig.decls[idx✝]
Tactic:
rw [go_decl_eq]
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls[idx✝] =
    aig.decls[idx✝]

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls[idx✝] =
    aig.decls[idx✝]

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
unfold mkFullAdder
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ (let res := mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin };
          let aig_1 := res.aig;
          let outRef := res.ref;
          let_fun haig1 := ⋯;
          let input := { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast haig1;
          let res_1 := mkFullAdderCarry aig_1 input;
          let aig_2 := res_1.aig;
          let carryRef := res_1.ref;
          let_fun haig2 := ⋯;
          let outRef := outRef.cast haig2;
          let_fun hle := ⋯;
          { aig := aig_2, out := outRef, cout := carryRef, hle := hle }).aig.decls[idx✝] =
    aig.decls[idx✝]

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ (let res := mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin };
          let aig_1 := res.aig;
          let outRef := res.ref;
          let_fun haig1 := ⋯;
          let input := { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast haig1;
          let res_1 := mkFullAdderCarry aig_1 input;
          let aig_2 := res_1.aig;
          let carryRef := res_1.ref;
          let_fun haig2 := ⋯;
          let outRef := outRef.cast haig2;
          let_fun hle := ⋯;
          { aig := aig_2, out := outRef, cout := carryRef, hle := hle }).aig.decls[idx✝] =
    aig.decls[idx✝]

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderCarry)]
State after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls[idx✝] =
    aig.decls[idx✝]

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size

case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ <
    (mkFullAdderCarry (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig
            ({ lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast ⋯)).aig.decls.size

State before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls[idx✝] =
    aig.decls[idx✝]

case isTrue.h1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size

case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ <
    (mkFullAdderCarry (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig
            ({ lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast ⋯)).aig.decls.size
Tactic:
rw [AIG.LawfulOperator.decl_eq (f := mkFullAdderOut)]
State after:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size

case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ <
    (mkFullAdderCarry (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig
            ({ lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast ⋯)).aig.decls.size

State before:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size

case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ <
    (mkFullAdderCarry (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig
            ({ lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast ⋯)).aig.decls.size
Tactic:
. apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
  assumption
State after:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ <
    (mkFullAdderCarry (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig
            ({ lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast ⋯)).aig.decls.size

State before:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ <
    (mkFullAdderCarry (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig
            ({ lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast ⋯)).aig.decls.size
Tactic:
. apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry)
  apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
  assumption
State after:
no goals

State before:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
State after:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size

State before:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size
Tactic:
assumption
State after:
no goals

State before:
case isTrue.h2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ <
    (mkFullAdderCarry (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig
            ({ lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }.cast ⋯)).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderCarry)
State after:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size

State before:
case isTrue.h2.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < (mkFullAdderOut aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig.decls.size
Tactic:
apply AIG.LawfulOperator.lt_size_of_lt_aig_size (f := mkFullAdderOut)
State after:
case isTrue.h2.h.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size

State before:
case isTrue.h2.h.h
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : curr < w
hgo :
  go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
      (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
      ((s.cast ⋯).pushRef (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
      (lhs.cast ⋯) (rhs.cast ⋯) =
    res
idx✝ : Nat
h1✝ : idx✝ < aig.decls.size
h2✝ :
  idx✝ <
    (go (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).aig (curr + 1) ⋯
            (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).cout
            ((s.cast ⋯).pushRef
              (mkFullAdder aig { lhs := lhs.getRef curr h✝, rhs := rhs.getRef curr h✝, cin := cin }).out)
            (lhs.cast ⋯) (rhs.cast ⋯)).aig.decls.size
⊢ idx✝ < aig.decls.size
Tactic:
assumption
State after:
no goals

State before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
hcurr : curr ≤ w
cin : aig.Ref
s : aig.RefStream curr
lhs rhs : aig.RefStream w
res : AIG.RefStreamEntry α w
h✝ : ¬curr < w
hgo : { aig := aig, stream := ⋯ ▸ s } = res
⊢ ∀ (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < res.aig.decls.size), res.aig.decls[idx] = aig.decls[idx]
Tactic:
simp [← hgo]
State after:
no goals