Theorem: AIG.LawfulOperator.denote_mem_prefix (LeanSAT/AIG/LawfulOperator.lean)

State before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
start : Nat
assign : α → Bool
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ start < (f aig input).aig.decls.size
Tactic:
apply lt_size_of_lt_aig_size
State after:
case h
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
start : Nat
assign : α → Bool
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ start < aig.decls.size

State before:
case h
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
start : Nat
assign : α → Bool
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ start < aig.decls.size
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
start : Nat
assign : α → Bool
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ ⟦{ aig := (f aig input).aig, ref := { gate := start, hgate := ⋯ } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := h } }, assign⟧
Tactic:
rw [denote_input_entry ⟨aig, start, h⟩]
State after:
no goals