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

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
curr : Nat
falseRef trueRef : aig.Ref
n d : aig.RefVec w
wn wr : Nat
q r : aig.RefVec w
⊢ aig.decls.size ≤
    (match curr with
          | 0 => { aig := aig, q := q, r := r, hle := ⋯ }
          | curr.succ =>
            {
              aig :=
                (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr (falseRef.cast ⋯)
                    (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).aig,
              q :=
                (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr (falseRef.cast ⋯)
                    (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).q,
              r :=
                (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr (falseRef.cast ⋯)
                    (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                    (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).r,
              hle := ⋯ }).aig.decls.size

Tactic:
split

Result:
case h_1
α : 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
curr✝ : Nat
⊢ aig.decls.size ≤ { aig := aig, q := q, r := r, hle := ⋯ }.aig.decls.size

case h_2
α : 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
curr✝¹ curr✝ : Nat
⊢ aig.decls.size ≤
    {
            aig :=
              (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                  (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).aig,
            q :=
              (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                  (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).q,
            r :=
              (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                  (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).r,
            hle := ⋯ }.aig.decls.size

Proof state:
case h_2
α : 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
curr✝¹ curr✝ : Nat
⊢ aig.decls.size ≤ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size

Tactic:
apply blastUdiv.blastDivSubtractShift_le_size

Result:
no goals

Proof state:
case h_2
α : 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
curr✝¹ curr✝ : Nat
⊢ aig.decls.size ≤
    {
            aig :=
              (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                  (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).aig,
            q :=
              (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                  (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).q,
            r :=
              (go (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig curr✝ (falseRef.cast ⋯)
                  (trueRef.cast ⋯) (n.cast ⋯) (d.cast ⋯) (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wn
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).wr
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).q
                  (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).r).r,
            hle := ⋯ }.aig.decls.size

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

Result:
case h_2
α : 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
curr✝¹ curr✝ : Nat
⊢ aig.decls.size ≤ (blastDivSubtractShift aig falseRef trueRef n d wn wr q r).aig.decls.size