split
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ (match elem : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkGate input).aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.const b✝
⊢ b✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯;
    xor lval linv✝ && xor rval rinv✝) =
    (xor ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧ input.lhs.inv &&
      xor ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧ input.rhs.inv)