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 := entry.ref }, 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 := { aig := aig✝, ref := ref✝ }.ref }, 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 := { aig := aig✝, ref := ref✝ }.ref }, assign⟧ =
    ⟦{ aig := aig✝, ref := ref✝ }, assign⟧
Tactic:
simp
State after:
no goals