-- 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:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
x✝¹⁰ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝⁹ x✝⁸ : Decl α
linv✝ rinv✝ : Bool
x✝⁷ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = true → False
x✝⁶ : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = false → False
x✝⁵ : aig.decls[input.rhs.ref.gate] = Decl.const true → input.rhs.inv = true → False
x✝⁴ : aig.decls[input.rhs.ref.gate] = Decl.const false → input.rhs.inv = false → False
x✝³ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = false → input.rhs.inv = false → False
x✝² : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = true → input.rhs.inv = false → False
x✝¹ : aig.decls[input.rhs.ref.gate] = Decl.const true → input.lhs.inv = false → input.rhs.inv = false → False
x✝ : aig.decls[input.rhs.ref.gate] = Decl.const false → input.lhs.inv = false → input.rhs.inv = true → False
h✝ : ¬(input.lhs.ref.gate == input.rhs.ref.gate && input.lhs.inv == false && input.rhs.inv == false) = true
hifeq : input.lhs.ref.gate = input.rhs.ref.gate
hinv : input.lhs.inv = !input.rhs.inv
⊢ input.lhs.ref = input.rhs.ref

Tactic:
rcases input with ⟨⟨⟨_, _⟩, _⟩, ⟨⟨_, _⟩, _⟩⟩

Result:
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