-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/LawfulOperator.lean
theorem denote.eq_of_isPrefix (entry : Entrypoint α) (newAIG : AIG α)
      (hprefix : IsPrefix entry.aig.decls newAIG.decls) :
    ⟦newAIG, ⟨entry.ref.gate, (by have := entry.ref.hgate; have := hprefix.size_le; omega)⟩, assign⟧
      =
    ⟦entry, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ entry.ref.gate < newAIG.decls.size

Tactic:
have := entry.ref.hgate

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
this : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < newAIG.decls.size

Proof state:
case hprefix
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ IsPrefix entry.aig.decls { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls

Tactic:
assumption

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
this✝ : entry.ref.gate < entry.aig.decls.size
this : entry.aig.decls.size ≤ newAIG.decls.size
⊢ entry.ref.gate < newAIG.decls.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ ⟦assign, { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }⟧ = ⟦assign, entry⟧

Tactic:
unfold denote

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ go { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.ref.gate
      { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ =
    go entry.ref.gate entry.aig.decls assign ⋯ ⋯

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ go { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.ref.gate
      { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ =
    go entry.ref.gate entry.aig.decls assign ⋯ ⋯

Tactic:
apply denote.go_eq_of_isPrefix

Result:
case hprefix
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ IsPrefix entry.aig.decls { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
this : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < newAIG.decls.size

Tactic:
have := hprefix.size_le

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
this✝ : entry.ref.gate < entry.aig.decls.size
this : entry.aig.decls.size ≤ newAIG.decls.size
⊢ entry.ref.gate < newAIG.decls.size