internlm/Lean-Github huggingface dataset:
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧
Tactic:
rw [RefStream.getRef_in_bound]
Proof state after:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx }, assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝

case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝
Tactic:
. assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ ⟦{ aig := aig,
        ref := { gate := ((input.cast ⋯).getRef (lo + idx) ?mk.isTrue.isTrue.hidx).gate, hgate := ?mk.isTrue.isTrue } },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + idx) h✝ }, assign⟧
Tactic:
congr 1
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isTrue.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : lo + idx < w✝
⊢ lo + idx < w✝
Tactic:
assumption
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (input.cast ⋯).getRefD (lo + idx) (aig.mkConstCached false).ref },
      assign⟧ =
    false
Tactic:
rw [RefStream.getRef_out_bound]
Proof state after:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ = false

case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ = false

case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Tactic:
. simp
Proof state after:
case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Tactic:
. omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ ⟦{ aig := (aig.mkConstCached false).aig, ref := (aig.mkConstCached false).ref }, assign⟧ = false
Tactic:
simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.isFalse.hidx
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝¹ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
h✝ : ¬lo + idx < w✝
⊢ w✝ ≤ lo + idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isTrue.a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := blastExtract.go (input.cast ⋯) lo 0 ⋯ (aig.mkConstCached false).ref RefStream.empty } =
    res
⊢ 0 ≤ idx
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
have : idx = 0 := by omega
Proof state after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this : idx = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this : idx = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef idx hidx }, assign⟧ =
    if h : lo + idx < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + idx) h }, assign⟧ else false
Tactic:
simp only [this]
Proof state after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this : idx = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this : idx = 0
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Tactic:
have : 1 = newWidth := by omega
Proof state after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this✝ : idx = 0
this : 1 = newWidth
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
newWidth : Nat
aig : AIG α
assign : α → Bool
idx : Nat
hidx : idx < newWidth
res : RefStreamEntry α newWidth
w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
hnew : newWidth = hi - lo + 1
h✝ : ¬lo ≤ hi
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
this✝ : idx = 0
this : 1 = newWidth
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Tactic:
subst this
Proof state after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{ aig := res.aig, ref := res.stream.getRef 0 ⋯ }, assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Tactic:
rw [← hextract]
Proof state after:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    if h : lo + 0 < w✝ then ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧ else false
Tactic:
split
Proof state after:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧

case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false
Theorem: BVExpr.bitblast.blastExtract_eq_eval_getLsb
Proof state before:
case mk.isFalse.isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    ⟦{ aig := aig, ref := input.getRef (lo + 0) ⋯ }, assign⟧

case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false
Tactic:
. rw [RefStream.getRef_in_bound]
  dsimp
  rw [LawfulOperator.denote_mem_prefix (f := mkConstCached)]
  . congr 2
  . omega
Proof state after:
case mk.isFalse.isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
assign : α → Bool
idx w✝ : Nat
input : aig.RefStream w✝
hi lo : Nat
h✝¹ : ¬lo ≤ hi
this : idx = 0
hidx : idx < 1
res : RefStreamEntry α 1
hnew : 1 = hi - lo + 1
hextract :
  { aig := (aig.mkConstCached false).aig,
      stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) } =
    res
h✝ : ¬lo + 0 < w✝
⊢ ⟦{
        aig :=
          { aig := (aig.mkConstCached false).aig,
              stream := ⋯ ▸ RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.aig,
        ref :=
          { aig := (aig.mkConstCached false).aig,
                  stream :=
                    ⋯ ▸
                      RefStream.empty.pushRef ((input.cast ⋯).getRefD lo (aig.mkConstCached false).ref) }.stream.getRef
            0 ⋯ },
      assign⟧ =
    false