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

Tactic:
apply AIG.LawfulOperator.le_size_of_le_aig_size (f := BVPred.mkUlt)

Result:
case 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 ≤
    (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.decls.size

Proof state:
case 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 ≤
    (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.decls.size

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

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