-- Std.Sat.AIG.CachedLemmas
Std.Sat.AIG.mkGateCached.go.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (decls : Array (Std.Sat.AIG.Decl α))
  (cache : Std.Sat.AIG.Cache α decls) (hdag : Std.Sat.AIG.IsDAG α decls) (hzero : 0 < decls.size)
  (hconst : decls[0] = Std.Sat.AIG.Decl.false)
  (input_2 : { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.BinaryInput),
  Std.Sat.AIG.mkGateCached.go { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }
      input_2 =
    match
      cache.get?
        (Std.Sat.AIG.Decl.gate (Std.Sat.AIG.Fanin.mk input_2.lhs.gate input_2.lhs.invert)
          (Std.Sat.AIG.Fanin.mk input_2.rhs.gate input_2.rhs.invert)) with
    | some hit =>
      { aig := { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst },
        ref := { gate := hit.idx, invert := false, hgate := ⋯ } }
    | none =>
      have lhsVal :=
        { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.getConstant input_2.lhs;
      have rhsVal :=
        { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.getConstant input_2.rhs;
      match lhsVal, rhsVal with
      | some false, x =>
        have ref :=
          { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.mkConstCached false;
        { aig := { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }, ref := ref }
      | x, some false =>
        have ref :=
          { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.mkConstCached false;
        { aig := { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }, ref := ref }
      | some true, x =>
        { aig := { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst },
          ref := { gate := input_2.rhs.gate, invert := input_2.rhs.invert, hgate := ⋯ } }
      | x, some true =>
        { aig := { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst },
          ref := { gate := input_2.lhs.gate, invert := input_2.lhs.invert, hgate := ⋯ } }
      | x, x_1 =>
        if (input_2.lhs.gate == input_2.rhs.gate) = true then
          if (input_2.lhs.invert == input_2.rhs.invert) = true then
            { aig := { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst },
              ref := { gate := input_2.lhs.gate, invert := input_2.lhs.invert, hgate := ⋯ } }
          else
            have ref :=
              { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }.mkConstCached false;
            { aig := { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }, ref := ref }
        else
          let g := decls.size;
          have cache_1 :=
            Std.Sat.AIG.Cache.insert decls cache
              (Std.Sat.AIG.Decl.gate (Std.Sat.AIG.Fanin.mk input_2.lhs.gate input_2.lhs.invert)
                (Std.Sat.AIG.Fanin.mk input_2.rhs.gate input_2.rhs.invert));
          let decls_1 :=
            decls.push
              (Std.Sat.AIG.Decl.gate (Std.Sat.AIG.Fanin.mk input_2.lhs.gate input_2.lhs.invert)
                (Std.Sat.AIG.Fanin.mk input_2.rhs.gate input_2.rhs.invert));
          have hdag_1 := ⋯;
          have hzero' := ⋯;
          have hconst_1 := ⋯;
          { aig := { decls := decls_1, cache := cache_1, hdag := hdag_1, hzero := hzero', hconst := hconst_1 },
            ref := { gate := g, invert := false, hgate := ⋯ } }