Theorem: BVPred.mkEq_denote_eq_eval_beq (LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Eq.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦mkEq aig pair, assign⟧ = (lhs == rhs)
Tactic:
unfold mkEq
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
      let aig := res.aig;
      let bits := res.stream;
      RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
      assign⟧ =
    (lhs == rhs)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
      let aig := res.aig;
      let bits := res.stream;
      RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
      assign⟧ =
    (lhs == rhs)
Tactic:
rw [Bool.eq_iff_iff]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
        let aig := res.aig;
        let bits := res.stream;
        RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
        assign⟧ =
      true ↔
    (lhs == rhs) = true

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ ⟦let res := RefStream.zip aig (RefStream.ZipTarget.mk pair mkBEqCached);
        let aig := res.aig;
        let bits := res.stream;
        RefStream.fold aig (RefStream.FoldTarget.mkAnd bits),
        assign⟧ =
      true ↔
    (lhs == rhs) = true
Tactic:
simp
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) ↔
    lhs = rhs

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) ↔
    lhs = rhs
Tactic:
constructor
State after:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) →
    lhs = rhs

case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧

State before:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) →
    lhs = rhs

case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Tactic:
. intro h
  ext
  rw [← hleft, ← hright]
  . simp [h]
  . omega
  . omega
State after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧

State before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Tactic:
. intro h idx hidx
  rw [hleft, hright]
  simp [h]
State after:
no goals

State before:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ (∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧) →
    lhs = rhs
Tactic:
intro h
State after:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
⊢ lhs = rhs

State before:
case mp
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
⊢ lhs = rhs
Tactic:
ext
State after:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ lhs.getLsb ↑i✝ = rhs.getLsb ↑i✝

State before:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ lhs.getLsb ↑i✝ = rhs.getLsb ↑i✝
Tactic:
rw [← hleft, ← hright]
State after:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := pair.rhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

State before:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := pair.rhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Tactic:
. simp [h]
State after:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

State before:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Tactic:
. omega
State after:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

State before:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w

case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Tactic:
. omega
State after:
no goals

State before:
case mp.pred
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := pair.rhs.getRef ↑i✝ ?mp.pred.hidx }, assign⟧
Tactic:
simp [h]
State after:
no goals

State before:
case mp.pred.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h :
  ∀ (idx : Nat) (hidx : idx < w),
    ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
      ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
i✝ : Fin w
⊢ ↑i✝ < w
Tactic:
omega
State after:
no goals

State before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
⊢ lhs = rhs →
    ∀ (idx : Nat) (hidx : idx < w),
      ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ =
        ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Tactic:
intro h idx hidx
State after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧

State before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧
Tactic:
rw [hleft, hright]
State after:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ lhs.getLsb idx = rhs.getLsb idx

State before:
case mpr
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
pair : aig.BinaryRefStream w
assign : α → Bool
lhs rhs : BitVec w
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.lhs.getRef idx hidx }, assign⟧ = lhs.getLsb idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦{ aig := aig, ref := pair.rhs.getRef idx hidx }, assign⟧ = rhs.getLsb idx
h : lhs = rhs
idx : Nat
hidx : idx < w
⊢ lhs.getLsb idx = rhs.getLsb idx
Tactic:
simp [h]
State after:
no goals