-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
theorem denote_blastReplicate (aig : AIG α) (target : ReplicateTarget aig newWidth)
    (assign : α → Bool) :
    ∀ (idx : Nat) (hidx : idx < newWidth),
        ⟦(blastReplicate aig target).aig, (blastReplicate aig target).vec.get idx hidx, assign⟧
          =
        ⟦aig, target.inner.get (idx % target.w) (blastReplicate.aux2 (target.h ▸ hidx)), assign⟧

Proof state:
case mk.a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ n : Nat
input : aig.RefVec w✝
hidx : idx < w✝ * n
⊢ w✝ * 0 ≤ idx

Tactic:
omega

Result:
no goals

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ n : Nat
input : aig.RefVec w✝
hidx : idx < w✝ * n
⊢ ⟦assign, { aig := aig, ref := (⋯ ▸ blastReplicate.go n input 0 ⋯ RefVec.empty).get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := input.get (idx % w✝) ⋯ }⟧

Tactic:
rw [blastReplicate.go_get]

Result:
case mk.a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ n : Nat
input : aig.RefVec w✝
hidx : idx < w✝ * n
⊢ w✝ * 0 ≤ idx

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
w✝ n : Nat
input : aig.RefVec w✝
h : newWidth = w✝ * n
⊢ ⟦assign,
      { aig := (blastReplicate aig (ReplicateTarget.mk n input h)).aig,
        ref := (blastReplicate aig (ReplicateTarget.mk n input h)).vec.get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := (ReplicateTarget.mk n input h).inner.get (idx % (ReplicateTarget.mk n input h).w) ⋯ }⟧

Tactic:
unfold blastReplicate

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
w✝ n : Nat
input : aig.RefVec w✝
h : newWidth = w✝ * n
⊢ ⟦assign,
      {
        aig :=
          (match ReplicateTarget.mk n input h with
            | ReplicateTarget.mk n inner h =>
              let ref := blastReplicate.go n inner 0 ⋯ RefVec.empty;
              { aig := aig, vec := ⋯ ▸ ref }).aig,
        ref :=
          (match ReplicateTarget.mk n input h with
                | ReplicateTarget.mk n inner h =>
                  let ref := blastReplicate.go n inner 0 ⋯ RefVec.empty;
                  { aig := aig, vec := ⋯ ▸ ref }).vec.get
            idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := (ReplicateTarget.mk n input h).inner.get (idx % (ReplicateTarget.mk n input h).w) ⋯ }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : ReplicateTarget aig newWidth
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < newWidth),
    ⟦assign, { aig := (blastReplicate aig target).aig, ref := (blastReplicate aig target).vec.get idx hidx }⟧ =
      ⟦assign, { aig := aig, ref := target.inner.get (idx % target.w) ⋯ }⟧

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : ReplicateTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦assign, { aig := (blastReplicate aig target).aig, ref := (blastReplicate aig target).vec.get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := target.inner.get (idx % target.w) ⋯ }⟧

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
w✝ n : Nat
input : aig.RefVec w✝
h : newWidth = w✝ * n
⊢ ⟦assign, { aig := aig, ref := (⋯ ▸ blastReplicate.go n input 0 ⋯ RefVec.empty).get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := input.get (idx % w✝) ⋯ }⟧

Tactic:
subst h

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ n : Nat
input : aig.RefVec w✝
hidx : idx < w✝ * n
⊢ ⟦assign, { aig := aig, ref := (⋯ ▸ blastReplicate.go n input 0 ⋯ RefVec.empty).get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := input.get (idx % w✝) ⋯ }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : ReplicateTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦assign, { aig := (blastReplicate aig target).aig, ref := (blastReplicate aig target).vec.get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := target.inner.get (idx % target.w) ⋯ }⟧

Tactic:
rcases target with ⟨n, input, h⟩

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
w✝ n : Nat
input : aig.RefVec w✝
h : newWidth = w✝ * n
⊢ ⟦assign,
      { aig := (blastReplicate aig (ReplicateTarget.mk n input h)).aig,
        ref := (blastReplicate aig (ReplicateTarget.mk n input h)).vec.get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := (ReplicateTarget.mk n input h).inner.get (idx % (ReplicateTarget.mk n input h).w) ⋯ }⟧

Proof state:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
w✝ n : Nat
input : aig.RefVec w✝
h : newWidth = w✝ * n
⊢ ⟦assign,
      {
        aig :=
          (match ReplicateTarget.mk n input h with
            | ReplicateTarget.mk n inner h =>
              let ref := blastReplicate.go n inner 0 ⋯ RefVec.empty;
              { aig := aig, vec := ⋯ ▸ ref }).aig,
        ref :=
          (match ReplicateTarget.mk n input h with
                | ReplicateTarget.mk n inner h =>
                  let ref := blastReplicate.go n inner 0 ⋯ RefVec.empty;
                  { aig := aig, vec := ⋯ ▸ ref }).vec.get
            idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := (ReplicateTarget.mk n input h).inner.get (idx % (ReplicateTarget.mk n input h).w) ⋯ }⟧

Tactic:
dsimp only

Result:
case mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
w✝ n : Nat
input : aig.RefVec w✝
h : newWidth = w✝ * n
⊢ ⟦assign, { aig := aig, ref := (⋯ ▸ blastReplicate.go n input 0 ⋯ RefVec.empty).get idx hidx }⟧ =
    ⟦assign, { aig := aig, ref := input.get (idx % w✝) ⋯ }⟧