Theorem: AIG.denote_projected_entry' (LeanSAT/AIG/Lemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
⊢ ⟦{ aig := entry.aig, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign⟧ = ⟦entry, assign⟧
Tactic:
cases entry
State after:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦{ aig := { aig := aig✝, ref := ref✝ }.aig, ref := { gate := { aig := aig✝, ref := ref✝ }.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig✝, ref := ref✝ }, assign⟧

State before:
case mk
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig✝ : AIG α
ref✝ : aig✝.Ref
⊢ ⟦{ aig := { aig := aig✝, ref := ref✝ }.aig, ref := { gate := { aig := aig✝, ref := ref✝ }.ref.gate, hgate := ⋯ } },
      assign⟧ =
    ⟦{ aig := aig✝, ref := ref✝ }, assign⟧
Tactic:
simp
State after:
no goals