-- 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:
α : 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)

Tactic:
rw [Bool.eq_iff_iff]

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)⟧ =
      true ↔
    (lhs == rhs) = true

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
⊢ (∀ (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:
constructor

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
⊢ (∀ (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

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 }⟧

Proof state:
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

Tactic:
rw [← hleft, ← hright]

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
⊢ ⟦assign, { aig := aig, ref := pair.lhs.get i ?mp.pred.hidx }⟧ =
    ⟦assign, { aig := aig, ref := pair.rhs.get i ?mp.pred.hidx }⟧

case mp.pred.hidx
α : 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
⊢ i < w

case mp.pred.hidx
α : 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
⊢ i < w

Proof state:
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
⊢ ⟦assign, { aig := aig, ref := pair.lhs.get i ?mp.pred.hidx }⟧ =
    ⟦assign, { aig := aig, ref := pair.rhs.get i ?mp.pred.hidx }⟧

Tactic:
simp [h, h']

Result:
no goals

Proof state:
case mp.pred.hidx
α : 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
⊢ i < w

Tactic:
omega

Result:
no goals