-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean
theorem mkEq_denote_eq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) (assign : α → Bool)
    (lhs rhs : BitVec w)
    (hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.lhs.get idx hidx, assign⟧ = lhs.getLsbD idx)
    (hright : ∀ (idx : Nat) (hidx : idx < w), ⟦aig, pair.rhs.get idx hidx, assign⟧ = rhs.getLsbD idx) :
    ⟦mkEq aig pair, assign⟧ = (lhs == rhs)

Proof state:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧
⊢ lhs = rhs

Tactic:
ext i h'

Result:
case mp.pred
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧
i : Nat
h' : i < w
⊢ lhs.getLsbD i = rhs.getLsbD i

Proof state:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧) →
    lhs = rhs

Tactic:
intro h

Result:
case mp
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧
⊢ lhs = rhs

Proof state:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧

Tactic:
rw [hleft, hright]

Result:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ lhs.getLsbD idx = rhs.getLsbD idx

Proof state:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ lhs.getLsbD idx = rhs.getLsbD idx

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign,
        let res := RefVec.zip aig (RefVec.ZipTarget.mk pair mkBEqCached);
        let aig := res.aig;
        let bits := res.vec;
        RefVec.fold aig (RefVec.FoldTarget.mkAnd bits)⟧ =
      true ↔
    (lhs == rhs) = true

Tactic:
simp only [RefVec.denote_fold_and, RefVec.denote_zip, denote_mkBEqCached, beq_iff_eq]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧) ↔
    lhs = rhs

Proof state:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧

Tactic:
intro h idx hidx

Result:
case mpr
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign, mkEq aig pair⟧ = (lhs == rhs)

Tactic:
unfold mkEq

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefVec w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := pair.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign,
      let res := RefVec.zip aig (RefVec.ZipTarget.mk pair mkBEqCached);
      let aig := res.aig;
      let bits := res.vec;
      RefVec.fold aig (RefVec.FoldTarget.mkAnd bits)⟧ =
    (lhs == rhs)