Theorem: AIG.denote_mkGate
Proof state before:
case e_x.e_a
α : 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✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.lhs.ref }, assign⟧

case e_x.e_a
α : 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✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ linv✝ = input.lhs.inv

case e_y.e_a
α : 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✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧

case e_y.e_a
α : 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✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv
Tactic:
. unfold denote
  simp only [heq1]
  apply denote.go_eq_of_aig_eq
  apply LawfulOperator.IsPrefix_aig
Proof state after:
case e_x.e_a
α : 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✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ linv✝ = input.lhs.inv

case e_y.e_a
α : 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✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ = ⟦{ aig := aig, ref := input.rhs.ref }, assign⟧

case e_y.e_a
α : 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✝
heq1 : input.lhs.ref.gate = lidx✝
heq2 : input.rhs.ref.gate = ridx✝
heq3 : input.lhs.inv = linv✝
heq4 : input.rhs.inv = rinv✝
⊢ rinv✝ = input.rhs.inv