-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BoolExpr/Circuit.lean
theorem go_denote_mem_prefix :
    ⟦
      (go aig expr atomHandler).val.aig,
      ⟨start, by apply Nat.lt_of_lt_of_le; exact hstart; apply go_le_size⟩,
      assign
    ⟧
      =
    ⟦aig, ⟨start, hstart⟩, assign⟧

Proof state:
case a
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig expr atomHandler).val.aig.decls.size

case m
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ Nat

Tactic:
exact hstart

Result:
case a
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig expr atomHandler).val.aig.decls.size

Proof state:
case a
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ aig.decls.size ≤ (go aig expr atomHandler).val.aig.decls.size

Tactic:
apply go_le_size

Result:
no goals

Proof state:
case hprefix
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ IsPrefix { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls (go aig expr atomHandler).val.aig.decls

Tactic:
apply go_isPrefix_aig

Result:
no goals

Proof state:
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ ⟦assign, { aig := (go aig expr atomHandler).val.aig, ref := { gate := start, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, hgate := hstart } }⟧

Tactic:
apply denote.eq_of_isPrefix (entry := ⟨aig, start,hstart⟩)

Result:
case hprefix
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ IsPrefix { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls (go aig expr atomHandler).val.aig.decls

Proof state:
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ start < (go aig expr atomHandler).val.aig.decls.size

Tactic:
apply Nat.lt_of_lt_of_le

Result:
case a
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ start < ?m

case a
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ ?m ≤ (go aig expr atomHandler).val.aig.decls.size

case m
α β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
atomHandler : AIG β → α → Entrypoint β
inst✝ : LawfulOperator β (fun x => α) atomHandler
assign : β → Bool
aig : AIG β
expr : BoolExpr α
start : Nat
hstart : start < aig.decls.size
⊢ Nat