-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Operations/ShiftRight.lean
theorem blastArithShiftRight.go_le_size (aig : AIG α) (distance : AIG.RefVec aig n) (curr : Nat)
    (acc : AIG.RefVec aig w) :
    aig.decls.size ≤ (go aig distance curr acc).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
h✝ : curr < n - 1
⊢ ?m.83801 ≤
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size

Tactic:
apply go_le_size

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
⊢ aig.decls.size ≤
    (if curr < n - 1 then
            go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯)
              (curr + 1) (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec
          else { aig := aig, vec := acc }).aig.decls.size

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
h✝ : curr < n - 1
⊢ aig.decls.size ≤
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
h✝ : ¬curr < n - 1
⊢ aig.decls.size ≤ { aig := aig, vec := acc }.aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
⊢ aig.decls.size ≤
    (if curr < n - 1 then
            let res := twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 };
            let aig_1 := res.aig;
            let acc_1 := res.vec;
            let_fun this := ⋯;
            let distance := distance.cast this;
            go aig_1 distance (curr + 1) acc_1
          else { aig := aig, vec := acc }).aig.decls.size

Tactic:
dsimp only

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
⊢ aig.decls.size ≤
    (if curr < n - 1 then
            go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯)
              (curr + 1) (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec
          else { aig := aig, vec := acc }).aig.decls.size

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
h✝ : curr < n - 1
⊢ aig.decls.size ≤
    (go (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig (distance.cast ⋯) (curr + 1)
            (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).vec).aig.decls.size

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

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
h✝ : curr < n - 1
⊢ aig.decls.size ≤ (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig.decls.size

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
⊢ aig.decls.size ≤ (go aig distance curr acc).aig.decls.size

Tactic:
unfold go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
⊢ aig.decls.size ≤
    (if curr < n - 1 then
            let res := twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 };
            let aig_1 := res.aig;
            let acc_1 := res.vec;
            let_fun this := ⋯;
            let distance := distance.cast this;
            go aig_1 distance (curr + 1) acc_1
          else { aig := aig, vec := acc }).aig.decls.size

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
h✝ : ¬curr < n - 1
⊢ aig.decls.size ≤ { aig := aig, vec := acc }.aig.decls.size

Tactic:
simp

Result:
no goals

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
n w : Nat
aig : AIG α
distance : aig.RefVec n
curr : Nat
acc : aig.RefVec w
h✝ : curr < n - 1
⊢ aig.decls.size ≤ (twoPowShift aig { n := n, lhs := acc, rhs := distance, pow := curr + 1 }).aig.decls.size

Tactic:
apply AIG.LawfulVecOperator.le_size (f := blastArithShiftRight.twoPowShift)

Result:
no goals