-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkGateCached.go_eval_eq_mkGate_eval {aig : AIG α} {input : GateInput aig} :
    ⟦go aig input, assign⟧ = ⟦aig.mkGate input, assign⟧

Proof state:
case mk.mk.mk.mk.mk
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
x✝¹⁰ x✝⁹ : Decl α
linv✝ rinv✝ inv✝¹ : Bool
gate✝¹ : Nat
hgate✝¹ : gate✝¹ < aig.decls.size
inv✝ : Bool
gate✝ : Nat
hgate✝ : gate✝ < aig.decls.size
x✝⁸ :
  Option
    (CacheHit aig.decls
      (Decl.gate
        { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.ref.gate
        { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.ref.gate
        { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv
        { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv))
heq✝ :
  aig.cache.get?
      (Decl.gate
        { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.ref.gate
        { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.ref.gate
        { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv
        { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv) =
    none
x✝⁷ :
  aig.decls[{ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.ref.gate] =
      Decl.const true →
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv =
        true →
      False
x✝⁶ :
  aig.decls[{ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.ref.gate] =
      Decl.const false →
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv =
        false →
      False
x✝⁵ :
  aig.decls[{ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.ref.gate] =
      Decl.const true →
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv =
        true →
      False
x✝⁴ :
  aig.decls[{ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.ref.gate] =
      Decl.const false →
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv =
        false →
      False
x✝³ :
  aig.decls[{ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.ref.gate] =
      Decl.const true →
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv =
        false →
      { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv =
          false →
        False
x✝² :
  aig.decls[{ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.ref.gate] =
      Decl.const false →
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv =
        true →
      { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv =
          false →
        False
x✝¹ :
  aig.decls[{ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.ref.gate] =
      Decl.const true →
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv =
        false →
      { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv =
          false →
        False
x✝ :
  aig.decls[{ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.ref.gate] =
      Decl.const false →
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
              rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv =
        false →
      { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv =
          true →
        False
h✝ :
  ¬({ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                    rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.ref.gate ==
            { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                    rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.ref.gate &&
          { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                  rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv ==
            false &&
        { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
                rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv ==
          false) =
      true
hifeq :
  { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
            rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.ref.gate =
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
            rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.ref.gate
hinv :
  { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
          rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.inv =
    !{ lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
            rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.inv
⊢ { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
          rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.lhs.ref =
    { lhs := { ref := { gate := gate✝¹, hgate := hgate✝¹ }, inv := inv✝¹ },
          rhs := { ref := { gate := gate✝, hgate := hgate✝ }, inv := inv✝ } }.rhs.ref

Tactic:
simpa using hifeq

Result:
no goals