-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/Udiv.lean
theorem blastDivSubtractShift_le_size (aig : AIG α) (falseRef trueRef : AIG.Ref aig)
     (n d : AIG.RefVec aig w) (wn wr : Nat) (q r : AIG.RefVec aig w) :
    aig.decls.size ≤ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size

Proof state:
case h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤
    (AIG.RefVec.ite
            (BVPred.mkUlt
                (blastSub
                    (blastShiftConcat
                        (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                            { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                        { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                    { lhs := ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                      rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                {
                  lhs :=
                    (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast ⋯,
                  rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig
            {
              discr :=
                (BVPred.mkUlt
                    (blastSub
                        (blastShiftConcat
                            (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                            { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                        {
                          lhs :=
                            ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                          rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
                    {
                      lhs :=
                        (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast
                          ⋯,
                      rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).ref,
              lhs :=
                (((blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).vec.cast
                          ⋯).cast
                      ⋯).cast
                  ⋯,
              rhs :=
                ((blastShiftConcat
                            (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                            { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).vec.cast
                      ⋯).cast
                  ⋯ }).aig.decls.size

Tactic:
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := AIG.RefVec.ite)

Result:
case h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤
    (BVPred.mkUlt
            (blastSub
                (blastShiftConcat
                    (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                        { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
                    { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig
                { lhs := ((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯,
                  rhs := ((d.cast ⋯).cast ⋯).cast ⋯ }).aig
            { lhs := (((blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).vec.cast ⋯).cast ⋯).cast ⋯,
              rhs := (((d.cast ⋯).cast ⋯).cast ⋯).cast ⋯ }).aig.decls.size

Proof state:
case h.h.h.h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤ (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig.decls.size

Tactic:
apply AIG.LawfulVecOperator.le_size (f := blastUdiv.blastShiftConcat)

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size

Tactic:
unfold blastDivSubtractShift

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤
    (let wn_1 := wn - 1;
          let wr := wr + 1;
          let res := blastShiftConcat aig { lhs := r, bit := n.getD wn_1 falseRef };
          let aig_1 := res.aig;
          let r' := res.vec;
          let_fun this := ⋯;
          let falseRef_1 := falseRef.cast this;
          let trueRef_1 := trueRef.cast this;
          let d_1 := d.cast this;
          let q_1 := q.cast this;
          let res_1 := blastShiftConcat aig_1 { lhs := q_1, bit := falseRef_1 };
          let aig_2 := res_1.aig;
          let posQ := res_1.vec;
          let_fun this_1 := ⋯;
          let trueRef_2 := trueRef_1.cast this_1;
          let d_2 := d_1.cast this_1;
          let q_2 := q_1.cast this_1;
          let r' := r'.cast this_1;
          let res := blastShiftConcat aig_2 { lhs := q_2, bit := trueRef_2 };
          let aig_3 := res.aig;
          let negQ := res.vec;
          let_fun this_2 := ⋯;
          let d_3 := d_2.cast this_2;
          let r' := r'.cast this_2;
          let posQ := posQ.cast this_2;
          let res_2 := blastSub aig_3 { lhs := r', rhs := d_3 };
          let aig_4 := res_2.aig;
          let negR := res_2.vec;
          let_fun this_3 := ⋯;
          let d_4 := d_3.cast this_3;
          let r'_1 := r'.cast this_3;
          let posQ := posQ.cast this_3;
          let negQ := negQ.cast this_3;
          let posR := r'_1;
          let res := BVPred.mkUlt aig_4 { lhs := r'_1, rhs := d_4 };
          let aig_5 := res.aig;
          let discr := res.ref;
          let_fun this_4 := ⋯;
          let posQ := posQ.cast this_4;
          let negQ := negQ.cast this_4;
          let posR := posR.cast this_4;
          let negR := negR.cast this_4;
          let res_3 := AIG.RefVec.ite aig_5 { discr := discr, lhs := posQ, rhs := negQ };
          let aig_6 := res_3.aig;
          let nextQ := res_3.vec;
          let_fun this_5 := ⋯;
          let posR := ⋯;
          ⋯).aig.decls.size

Proof state:
case h.h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤
    (blastShiftConcat
            (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
                { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig
            { lhs := (q.cast ⋯).cast ⋯, bit := (trueRef.cast ⋯).cast ⋯ }).aig.decls.size

Tactic:
apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := blastUdiv.blastShiftConcat)

Result:
case h.h.h.h.h
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤
    (blastShiftConcat (blastShiftConcat aig { lhs := r, bit := n.getD (wn - 1) falseRef }).aig
            { lhs := q.cast ⋯, bit := falseRef.cast ⋯ }).aig.decls.size