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

Tactic:
split

Result:
case isTrue.isTrue
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
h✝¹ : curr < w
h✝ : aig.isConstant (rhs.get curr h✝¹) false = true
⊢ aig.decls.size ≤ (go aig lhs rhs (curr + 1) acc).aig.decls.size

case isTrue.isFalse
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
h✝¹ : curr < w
h✝ : ¬aig.isConstant (rhs.get curr h✝¹) false = true
⊢ aig.decls.size ≤
    (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

Proof state:
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

Tactic:
simp

Result:
no goals

Proof state:
case isTrue.isFalse.h
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
h✝¹ : curr < w
h✝ : ¬aig.isConstant (rhs.get curr h✝¹) false = true
⊢ aig.decls.size ≤
    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
            { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig.decls.size

Tactic:
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastAdd)

Result:
case isTrue.isFalse.h.h
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
h✝¹ : curr < w
h✝ : ¬aig.isConstant (rhs.get curr h✝¹) false = true
⊢ aig.decls.size ≤ (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig.decls.size

Proof state:
case isTrue.isFalse.h.h
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
h✝¹ : curr < w
h✝ : ¬aig.isConstant (rhs.get curr h✝¹) false = true
⊢ aig.decls.size ≤ (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig.decls.size

Tactic:
apply AIG.LawfulVecOperator.le_size (f := blastShiftLeftConst)

Result:
no goals

Proof state:
case isTrue.isFalse
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
h✝¹ : curr < w
h✝ : ¬aig.isConstant (rhs.get curr h✝¹) false = true
⊢ aig.decls.size ≤
    (go
            (AIG.RefVec.ite
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                    { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                  lhs :=
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                  rhs := (acc.cast ⋯).cast ⋯ }).aig
            (((lhs.cast ⋯).cast ⋯).cast ⋯) (((rhs.cast ⋯).cast ⋯).cast ⋯) (curr + 1)
            (AIG.RefVec.ite
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                    { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
                { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
                  lhs :=
                    (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                        { lhs := acc.cast ⋯,
                          rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
                  rhs := (acc.cast ⋯).cast ⋯ }).vec).aig.decls.size

Tactic:
refine Nat.le_trans ?_ (by apply go_le_size)

Result:
case isTrue.isFalse
w : Nat
aig : AIG BVBit
curr : Nat
acc lhs rhs : aig.RefVec w
h✝¹ : curr < w
h✝ : ¬aig.isConstant (rhs.get curr h✝¹) false = true
⊢ aig.decls.size ≤
    (AIG.RefVec.ite
            (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).aig
            { discr := ((rhs.cast ⋯).cast ⋯).get curr h✝¹,
              lhs :=
                (blastAdd (blastShiftLeftConst aig { vec := lhs, distance := curr }).aig
                    { lhs := acc.cast ⋯, rhs := (blastShiftLeftConst aig { vec := lhs, distance := curr }).vec }).vec,
              rhs := (acc.cast ⋯).cast ⋯ }).aig.decls.size