-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Mul.lean
theorem go_le_size {w : Nat} (aig : AIG BVBit) (curr : Nat) (acc : AIG.RefVec aig w)
    (lhs rhs : AIG.RefVec aig w) :
    aig.decls.size ≤ (go aig lhs rhs curr acc).aig.decls.size

Proof state:
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
⊢ aig.decls.size ≤
    (if h : curr < w then
            if aig.isConstant (rhs.get curr h) false = true then go aig lhs rhs (curr + 1) acc
            else
              let res := blastShiftLeftConst aig { vec := lhs, distance := curr };
              let aig_1 := res.aig;
              let shifted := res.vec;
              let_fun this := ⋯;
              let lhs_1 := lhs.cast this;
              let rhs_1 := rhs.cast this;
              let acc_1 := acc.cast this;
              let res := blastAdd aig_1 { lhs := acc_1, rhs := shifted };
              let aig_2 := res.aig;
              let added := res.vec;
              let_fun this_1 := ⋯;
              let lhs_2 := lhs_1.cast this_1;
              let rhs_2 := rhs_1.cast this_1;
              let acc_2 := acc_1.cast this_1;
              let res := AIG.RefVec.ite aig_2 { discr := rhs_2.get curr h, lhs := added, rhs := acc_2 };
              let aig_3 := res.aig;
              let acc_3 := res.vec;
              let_fun this := ⋯;
              let lhs := lhs_2.cast this;
              let rhs := rhs_2.cast this;
              go aig_3 lhs rhs (curr + 1) acc_3
          else { aig := aig, vec := acc }).aig.decls.size

Tactic:
split

Result:
case isTrue
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
h✝ : curr < w
⊢ aig.decls.size ≤
    (if aig.isConstant (rhs.get curr h✝) false = true then go aig lhs rhs (curr + 1) acc
          else
            let res := blastShiftLeftConst aig { vec := lhs, distance := curr };
            let aig_1 := res.aig;
            let shifted := res.vec;
            let_fun this := ⋯;
            let lhs_1 := lhs.cast this;
            let rhs_1 := rhs.cast this;
            let acc_1 := acc.cast this;
            let res := blastAdd aig_1 { lhs := acc_1, rhs := shifted };
            let aig_2 := res.aig;
            let added := res.vec;
            let_fun this_1 := ⋯;
            let lhs_2 := lhs_1.cast this_1;
            let rhs_2 := rhs_1.cast this_1;
            let acc_2 := acc_1.cast this_1;
            let res := AIG.RefVec.ite aig_2 { discr := rhs_2.get curr h✝, lhs := added, rhs := acc_2 };
            let aig_3 := res.aig;
            let acc_3 := res.vec;
            let_fun this := ⋯;
            let lhs := lhs_2.cast this;
            let rhs := rhs_2.cast this;
            go aig_3 lhs rhs (curr + 1) acc_3).aig.decls.size

case isFalse
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
h✝ : ¬curr < w
⊢ aig.decls.size ≤ { aig := aig, vec := acc }.aig.decls.size

Proof state:
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
⊢ aig.decls.size ≤ (go aig lhs rhs curr acc).aig.decls.size

Tactic:
unfold go

Result:
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
⊢ aig.decls.size ≤
    (if h : curr < w then
            if aig.isConstant (rhs.get curr h) false = true then go aig lhs rhs (curr + 1) acc
            else
              let res := blastShiftLeftConst aig { vec := lhs, distance := curr };
              let aig_1 := res.aig;
              let shifted := res.vec;
              let_fun this := ⋯;
              let lhs_1 := lhs.cast this;
              let rhs_1 := rhs.cast this;
              let acc_1 := acc.cast this;
              let res := blastAdd aig_1 { lhs := acc_1, rhs := shifted };
              let aig_2 := res.aig;
              let added := res.vec;
              let_fun this_1 := ⋯;
              let lhs_2 := lhs_1.cast this_1;
              let rhs_2 := rhs_1.cast this_1;
              let acc_2 := acc_1.cast this_1;
              let res := AIG.RefVec.ite aig_2 { discr := rhs_2.get curr h, lhs := added, rhs := acc_2 };
              let aig_3 := res.aig;
              let acc_3 := res.vec;
              let_fun this := ⋯;
              let lhs := lhs_2.cast this;
              let rhs := rhs_2.cast this;
              go aig_3 lhs rhs (curr + 1) acc_3
          else { aig := aig, vec := acc }).aig.decls.size