-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ShiftLeft.lean
theorem denote_blastShiftLeft (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),
        ⟦
          (blastShiftLeft aig target).aig,
          (blastShiftLeft aig target).vec.get idx hidx,
          assign
        ⟧
          =
        (lhs <<< rhs).getLsbD idx

Proof state:
case mk.isFalse.hright
α : 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
hg :
  blastShiftLeft.go (blastShiftLeft.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).aig
      (distance.cast ⋯) 0 (blastShiftLeft.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).vec =
    res
⊢ ∀ (idx : Nat) (hidx : idx < n),
    ⟦assign,
        { aig := (blastShiftLeft.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).aig,
          ref := (distance.cast ⋯).get idx hidx }⟧ =
      rhs.getLsbD idx

Tactic:
intros

Result:
case mk.isFalse.hright
α : 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
hg :
  blastShiftLeft.go (blastShiftLeft.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).aig
      (distance.cast ⋯) 0 (blastShiftLeft.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).vec =
    res
idx✝ : Nat
hidx✝ : idx✝ < n
⊢ ⟦assign,
      { aig := (blastShiftLeft.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).aig,
        ref := (distance.cast ⋯).get idx✝ hidx✝ }⟧ =
    rhs.getLsbD idx✝

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

Tactic:
simp only [hleft, Nat.zero_sub, BitVec.shiftLeftRec_zero, BitVec.and_twoPow, Nat.le_refl,
  BitVec.getLsbD_ge, Bool.false_eq_true, ↓reduceIte, BitVec.reduceHShiftLeft',
  BitVec.getLsbD_shiftLeft, Nat.sub_zero, Bool.iff_and_self, Bool.and_eq_true, decide_eq_true_eq,
  Bool.not_eq_true', decide_eq_false_iff_not, Nat.not_lt, Nat.zero_le, and_true]

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

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
target : aig.ArbitraryShiftTarget w0
lhs : BitVec w0
rhs : BitVec target.n
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦assign, { aig := aig, ref := target.target.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < target.n), ⟦assign, { aig := aig, ref := target.distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w0
⊢ ⟦assign, { aig := (blastShiftLeft aig target).aig, ref := (blastShiftLeft aig target).vec.get idx hidx }⟧ =
    (lhs <<< rhs).getLsbD idx

Tactic:
rw [BitVec.shiftLeft_eq_shiftLeftRec]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w0 : Nat
aig : AIG α
target : aig.ArbitraryShiftTarget w0
lhs : BitVec w0
rhs : BitVec target.n
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w0), ⟦assign, { aig := aig, ref := target.target.get idx hidx }⟧ = lhs.getLsbD idx
hright :
  ∀ (idx : Nat) (hidx : idx < target.n), ⟦assign, { aig := aig, ref := target.distance.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w0
⊢ ⟦assign, { aig := (blastShiftLeft aig target).aig, ref := (blastShiftLeft aig target).vec.get idx hidx }⟧ =
    (lhs.shiftLeftRec rhs (target.n - 1)).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
hg :
  blastShiftLeft.go (blastShiftLeft.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).aig
      (distance.cast ⋯) 0 (blastShiftLeft.twoPowShift aig { n := n, lhs := target, rhs := distance, pow := 0 }).vec =
    res
⊢ 0 ≤ n - 1

Tactic:
omega

Result:
no goals