Theorem: AIG.denote_mkImpCached (LeanSAT/AIG/CachedGatesLemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkImpCached input, assign⟧ =
    (!⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ ||
      ⟦{ aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }, assign⟧)
Tactic:
rw [← imp_as_aig]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkImpCached input, assign⟧ =
    !(⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ &&
        !⟦{ aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }, assign⟧)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.BinaryInput
⊢ ⟦aig.mkImpCached input, assign⟧ =
    !(⟦{ aig := aig, ref := { gate := input.lhs.gate, hgate := ⋯ } }, assign⟧ &&
        !⟦{ aig := aig, ref := { gate := input.rhs.gate, hgate := ⋯ } }, assign⟧)
Tactic:
simp [mkImpCached, LawfulOperator.denote_input_entry (f := mkConstCached)]
State after:
no goals