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

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

Tactic:
assumption

Result:
no goals

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

Tactic:
congr 1

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

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ (!⟦assign,
        BVExpr.bitblast.mkOverflowBit ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig
          { w := w, vec := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).vec.cast ⋯ },
            cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }⟧) =
    !BitVec.carry w lhs (~~~rhs) true

Tactic:
congr 1

Result:
case e_a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
⊢ ⟦assign,
      BVExpr.bitblast.mkOverflowBit ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig
        { w := w, vec := { lhs := input.lhs.cast ⋯, rhs := (BVExpr.bitblast.blastNot aig input.rhs).vec.cast ⋯ },
          cin := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).ref }⟧ =
    BitVec.carry w lhs (~~~rhs) true

Proof state:
case e_a.hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := ((BVExpr.bitblast.blastNot aig input.rhs).aig.mkConstCached true).aig,
        ref := (input.lhs.cast ⋯).get idx hidx }⟧ =
    lhs.getLsbD idx

Tactic:
rw [AIG.LawfulOperator.denote_mem_prefix (f := AIG.mkConstCached)]

Result:
case e_a.hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref := { gate := ((input.lhs.cast ⋯).get idx hidx).gate, hgate := ?e_a.hleft✝ } }⟧ =
    lhs.getLsbD idx

case e_a.hleft
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ((input.lhs.cast ⋯).get idx hidx).gate < (BVExpr.bitblast.blastNot aig input.rhs).aig.decls.size

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

Tactic:
rw [BitVec.ult_eq_not_carry]

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

Proof state:
case e_a.hright
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
lhs rhs : BitVec w
input : aig.BinaryRefVec w
assign : α → Bool
hleft : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.lhs.get idx hidx }⟧ = lhs.getLsbD idx
hright : ∀ (idx : Nat) (hidx : idx < w), ⟦assign, { aig := aig, ref := input.rhs.get idx hidx }⟧ = rhs.getLsbD idx
idx : Nat
hidx : idx < w
⊢ ⟦assign,
      { aig := (BVExpr.bitblast.blastNot aig input.rhs).aig,
        ref := { gate := ((BVExpr.bitblast.blastNot aig input.rhs).vec.get idx hidx).gate, hgate := ⋯ } }⟧ =
    !rhs.getLsbD idx

Tactic:
rw [BVExpr.bitblast.denote_blastNot]

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