-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Append.lean
theorem denote_blastAppend (aig : AIG α) (target : AppendTarget aig newWidth)
  (assign : α → Bool) :
  ∀ (idx : Nat) (hidx : idx < newWidth),
      ⟦
        (blastAppend aig target).aig,
        (blastAppend aig target).vec.get idx hidx,
        assign
      ⟧
        =
      if hr : idx < target.rw then
         ⟦aig, target.rhs.get idx hr, assign⟧
      else
         have := target.h
         ⟦aig, target.lhs.get (idx - target.rw) (by omega), assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx : Nat
hidx : idx < newWidth
hr : ¬idx < target.rw
this : newWidth = target.rw + target.lw
⊢ idx - target.rw < target.lw

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦assign,
      {
        aig :=
          (match target with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, vec := ⋯ ▸ combined }).aig,
        ref :=
          (match target with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, vec := ⋯ ▸ combined }).vec.get
            idx✝ hidx✝ }⟧ =
    if hr : idx✝ < target.rw then ⟦assign, { aig := aig, ref := target.rhs.get idx✝ hr }⟧
    else
      let_fun this := ⋯;
      ⟦assign, { aig := aig, ref := target.lhs.get (idx✝ - target.rw) ⋯ }⟧

Tactic:
rcases target with ⟨lw, rw, lhs, rhs, ht⟩

Result:
case mk.refl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefVec lw✝
rw : aig.RefVec rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦assign,
      {
        aig :=
          (match AppendTarget.mk lw rw ⋯ with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, vec := ⋯ ▸ combined }).aig,
        ref :=
          (match AppendTarget.mk lw rw ⋯ with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, vec := ⋯ ▸ combined }).vec.get
            idx✝ hidx✝ }⟧ =
    if hr : idx✝ < (AppendTarget.mk lw rw ⋯).rw then
      ⟦assign, { aig := aig, ref := (AppendTarget.mk lw rw ⋯).rhs.get idx✝ hr }⟧
    else
      let_fun this := ⋯;
      ⟦assign, { aig := aig, ref := (AppendTarget.mk lw rw ⋯).lhs.get (idx✝ - (AppendTarget.mk lw rw ⋯).rw) ⋯ }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
⊢ ∀ (idx : Nat) (hidx : idx < newWidth),
    ⟦assign, { aig := (blastAppend aig target).aig, ref := (blastAppend aig target).vec.get idx hidx }⟧ =
      if hr : idx < target.rw then ⟦assign, { aig := aig, ref := target.rhs.get idx hr }⟧
      else
        let_fun this := ⋯;
        ⟦assign, { aig := aig, ref := target.lhs.get (idx - target.rw) ⋯ }⟧

Tactic:
intros

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦assign, { aig := (blastAppend aig target).aig, ref := (blastAppend aig target).vec.get idx✝ hidx✝ }⟧ =
    if hr : idx✝ < target.rw then ⟦assign, { aig := aig, ref := target.rhs.get idx✝ hr }⟧
    else
      let_fun this := ⋯;
      ⟦assign, { aig := aig, ref := target.lhs.get (idx✝ - target.rw) ⋯ }⟧

Proof state:
case mk.refl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefVec lw✝
rw : aig.RefVec rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦assign, { aig := aig, ref := (rw.append lw).get idx✝ hidx✝ }⟧ =
    if hr : idx✝ < rw✝ then ⟦assign, { aig := aig, ref := rw.get idx✝ hr }⟧
    else ⟦assign, { aig := aig, ref := lw.get (idx✝ - rw✝) ⋯ }⟧

Tactic:
rw [AIG.RefVec.get_append]

Result:
case mk.refl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefVec lw✝
rw : aig.RefVec rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦assign, { aig := aig, ref := if h : idx✝ < rw✝ then rw.get idx✝ h else lw.get (idx✝ - rw✝) ⋯ }⟧ =
    if hr : idx✝ < rw✝ then ⟦assign, { aig := aig, ref := rw.get idx✝ hr }⟧
    else ⟦assign, { aig := aig, ref := lw.get (idx✝ - rw✝) ⋯ }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦assign, { aig := (blastAppend aig target).aig, ref := (blastAppend aig target).vec.get idx✝ hidx✝ }⟧ =
    if hr : idx✝ < target.rw then ⟦assign, { aig := aig, ref := target.rhs.get idx✝ hr }⟧
    else
      let_fun this := ⋯;
      ⟦assign, { aig := aig, ref := target.lhs.get (idx✝ - target.rw) ⋯ }⟧

Tactic:
unfold blastAppend

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
target : AppendTarget aig newWidth
assign : α → Bool
idx✝ : Nat
hidx✝ : idx✝ < newWidth
⊢ ⟦assign,
      {
        aig :=
          (match target with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, vec := ⋯ ▸ combined }).aig,
        ref :=
          (match target with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, vec := ⋯ ▸ combined }).vec.get
            idx✝ hidx✝ }⟧ =
    if hr : idx✝ < target.rw then ⟦assign, { aig := aig, ref := target.rhs.get idx✝ hr }⟧
    else
      let_fun this := ⋯;
      ⟦assign, { aig := aig, ref := target.lhs.get (idx✝ - target.rw) ⋯ }⟧

Proof state:
case mk.refl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefVec lw✝
rw : aig.RefVec rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦assign,
      {
        aig :=
          (match AppendTarget.mk lw rw ⋯ with
            | AppendTarget.mk lhs rhs h =>
              let combined := rhs.append lhs;
              { aig := aig, vec := ⋯ ▸ combined }).aig,
        ref :=
          (match AppendTarget.mk lw rw ⋯ with
                | AppendTarget.mk lhs rhs h =>
                  let combined := rhs.append lhs;
                  { aig := aig, vec := ⋯ ▸ combined }).vec.get
            idx✝ hidx✝ }⟧ =
    if hr : idx✝ < (AppendTarget.mk lw rw ⋯).rw then
      ⟦assign, { aig := aig, ref := (AppendTarget.mk lw rw ⋯).rhs.get idx✝ hr }⟧
    else
      let_fun this := ⋯;
      ⟦assign, { aig := aig, ref := (AppendTarget.mk lw rw ⋯).lhs.get (idx✝ - (AppendTarget.mk lw rw ⋯).rw) ⋯ }⟧

Tactic:
dsimp only

Result:
case mk.refl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefVec lw✝
rw : aig.RefVec rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦assign, { aig := aig, ref := (rw.append lw).get idx✝ hidx✝ }⟧ =
    if hr : idx✝ < rw✝ then ⟦assign, { aig := aig, ref := rw.get idx✝ hr }⟧
    else ⟦assign, { aig := aig, ref := lw.get (idx✝ - rw✝) ⋯ }⟧

Proof state:
case mk.refl
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx✝ lw✝ rw✝ : Nat
lw : aig.RefVec lw✝
rw : aig.RefVec rw✝
hidx✝ : idx✝ < rw✝ + lw✝
⊢ ⟦assign, { aig := aig, ref := if h : idx✝ < rw✝ then rw.get idx✝ h else lw.get (idx✝ - rw✝) ⋯ }⟧ =
    if hr : idx✝ < rw✝ then ⟦assign, { aig := aig, ref := rw.get idx✝ hr }⟧
    else ⟦assign, { aig := aig, ref := lw.get (idx✝ - rw✝) ⋯ }⟧

Tactic:
split <;> rfl

Result:
no goals