-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/ZeroExtend.lean
theorem denote_blastZeroExtend (aig : AIG α) (target : ExtendTarget aig newWidth)
    (assign : α → Bool) :
    ∀ (idx : Nat) (hidx : idx < newWidth),
        ⟦(blastZeroExtend aig target).aig, (blastZeroExtend aig target).vec.get idx hidx, assign⟧
          =
        if hidx : idx < target.w then
           ⟦aig, target.vec.get idx hidx, assign⟧
        else
           false

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < newWidth),
    ⟦assign, { aig := (blastZeroExtend aig target).aig, ref := (blastZeroExtend aig target).vec.get idx hidx }⟧ =
      if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧ else false

Tactic:
intro idx hidx

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦assign, { aig := (blastZeroExtend aig target).aig, ref := (blastZeroExtend aig target).vec.get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧ else false

Proof state:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ 0 ≤ idx

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦assign,
      {
        aig :=
          (match target with
            | { w := width, vec := input } => blastZeroExtend.go aig width input newWidth 0 ⋯ RefVec.empty).aig,
        ref :=
          (match target with
                | { w := width, vec := input } => blastZeroExtend.go aig width input newWidth 0 ⋯ RefVec.empty).vec.get
            idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧ else false

Tactic:
apply blastZeroExtend.go_denote_eq

Result:
case a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ 0 ≤ idx

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦assign, { aig := (blastZeroExtend aig target).aig, ref := (blastZeroExtend aig target).vec.get idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧ else false

Tactic:
unfold blastZeroExtend

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : aig.ExtendTarget newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
⊢ ⟦assign,
      {
        aig :=
          (match target with
            | { w := width, vec := input } => blastZeroExtend.go aig width input newWidth 0 ⋯ RefVec.empty).aig,
        ref :=
          (match target with
                | { w := width, vec := input } => blastZeroExtend.go aig width input newWidth 0 ⋯ RefVec.empty).vec.get
            idx hidx }⟧ =
    if hidx : idx < target.w then ⟦assign, { aig := aig, ref := target.vec.get idx hidx }⟧ else false