-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftRight.lean
theorem denote_blastArithShiftRight (aig : AIG α) (target : ArbitraryShiftTarget aig w0)
    (lhs : BitVec w0) (rhs : BitVec target.n) (assign : α → Bool)
    (hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦aig, target.target.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < target.n), ⟦aig, target.distance.get idx hidx, assign⟧ = rhs.getLsbD idx) :
    ∀ (idx : Nat) (hidx : idx < w0),
        ⟦
          (blastArithShiftRight aig target).aig,
          (blastArithShiftRight aig target).vec.get idx hidx,
          assign
        ⟧
          =
        (BitVec.sshiftRight' lhs rhs).getLsbD idx

Proof state:
case mk.isFalse.hcurr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
lhs : BitVec w0
assign : α → Bool
idx : Nat
hidx : idx < w0
res : RefVecEntry α w0
n : Nat
target : aig.RefVec w0
distance : aig.RefVec n
rhs : BitVec { n := n, target := target, distance := distance }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w0),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.target.get idx hidx }⟧ =
      lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, target := target, distance := distance }.n),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.distance.get idx hidx }⟧ =
      rhs.getLsbD idx
h✝ : ¬n = 0
hres :
  blastArithShiftRight.go
      (blastArithShiftRight.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).aig (distance.cast ⋯)
      0 (blastArithShiftRight.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).vec =
    res
⊢ 0 ≤ n - 1

Tactic:
omega

Result:
no goals

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
lhs : BitVec w0
assign : α → Bool
idx : Nat
hidx : idx < w0
res : RefVecEntry α w0
n : Nat
target : aig.RefVec w0
distance : aig.RefVec n
rhs : BitVec { n := n, target := target, distance := distance }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w0),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.target.get idx hidx }⟧ =
      lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, target := target, distance := distance }.n),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.distance.get idx hidx }⟧ =
      rhs.getLsbD idx
hres :
  (match { n := n, target := target, distance := distance } with
    | { n := n, target := input, distance := distance } =>
      if n = 0 then { aig := aig, vec := input }
      else
        let res := blastArithShiftRight.twoPowShift aig { n := n, lhs := input, rhs := distance, pow := 0 };
        let aig_1 := res.aig;
        let acc := res.vec;
        let_fun this := ⋯;
        let distance := distance.cast this;
        blastArithShiftRight.go aig_1 distance 0 acc) =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (lhs.sshiftRightRec rhs ({ n := n, target := target, distance := distance }.n - 1)).getLsbD idx

Tactic:
dsimp only at hres

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
lhs : BitVec w0
assign : α → Bool
idx : Nat
hidx : idx < w0
res : RefVecEntry α w0
n : Nat
target : aig.RefVec w0
distance : aig.RefVec n
rhs : BitVec { n := n, target := target, distance := distance }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w0),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.target.get idx hidx }⟧ =
      lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, target := target, distance := distance }.n),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.distance.get idx hidx }⟧ =
      rhs.getLsbD idx
hres :
  (if n = 0 then { aig := aig, vec := target }
    else
      blastArithShiftRight.go
        (blastArithShiftRight.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).aig
        (distance.cast ⋯) 0
        (blastArithShiftRight.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).vec) =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (lhs.sshiftRightRec rhs ({ n := n, target := target, distance := distance }.n - 1)).getLsbD idx

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
lhs : BitVec w0
assign : α → Bool
idx : Nat
hidx : idx < w0
res : RefVecEntry α w0
n : Nat
target : aig.RefVec w0
distance : aig.RefVec n
rhs : BitVec { n := n, target := target, distance := distance }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w0),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.target.get idx hidx }⟧ =
      lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, target := target, distance := distance }.n),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.distance.get idx hidx }⟧ =
      rhs.getLsbD idx
hres :
  (if n = 0 then { aig := aig, vec := target }
    else
      blastArithShiftRight.go
        (blastArithShiftRight.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).aig
        (distance.cast ⋯) 0
        (blastArithShiftRight.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).vec) =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (lhs.sshiftRightRec rhs ({ n := n, target := target, distance := distance }.n - 1)).getLsbD idx

Tactic:
split at hres

Result:
case mk.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
lhs : BitVec w0
assign : α → Bool
idx : Nat
hidx : idx < w0
res : RefVecEntry α w0
n : Nat
target : aig.RefVec w0
distance : aig.RefVec n
rhs : BitVec { n := n, target := target, distance := distance }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w0),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.target.get idx hidx }⟧ =
      lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, target := target, distance := distance }.n),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.distance.get idx hidx }⟧ =
      rhs.getLsbD idx
h✝ : n = 0
hres : { aig := aig, vec := target } = res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (lhs.sshiftRightRec rhs ({ n := n, target := target, distance := distance }.n - 1)).getLsbD idx

case mk.isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
lhs : BitVec w0
assign : α → Bool
idx : Nat
hidx : idx < w0
res : RefVecEntry α w0
n : Nat
target : aig.RefVec w0
distance : aig.RefVec n
rhs : BitVec { n := n, target := target, distance := distance }.n
hleft :
  ∀ (idx : Nat) (hidx : idx < w0),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.target.get idx hidx }⟧ =
      lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < { n := n, target := target, distance := distance }.n),
    ⟦assign, { aig := aig, ref := { n := n, target := target, distance := distance }.distance.get idx hidx }⟧ =
      rhs.getLsbD idx
h✝ : ¬n = 0
hres :
  blastArithShiftRight.go
      (blastArithShiftRight.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).aig (distance.cast ⋯)
      0 (blastArithShiftRight.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).vec =
    res
⊢ ⟦assign, { aig := res.aig, ref := res.vec.get idx hidx }⟧ =
    (lhs.sshiftRightRec rhs ({ n := n, target := target, distance := distance }.n - 1)).getLsbD idx