Theorem: AIG.denote.go_eq_of_aig_eq
Proof state before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
b✝ : Bool
heq✝ : decls2[start] = Decl.const b✝
⊢ b✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq✝ : decls2[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls2[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lidx✝ decls2 assign ⋯ hdag2;
    let rval := go ridx✝ decls2 assign ⋯ hdag2;
    xor lval linv✝ && xor rval rinv✝) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv
Tactic:
. next heq =>
  rw [hidx1] at heq
  split <;> simp_all
Proof state after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
idx✝ : α
heq✝ : decls2[start] = Decl.atom idx✝
⊢ assign idx✝ =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv

case h_3
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
decls1 decls2 : Array (Decl α)
start : Nat
hdag1 : IsDag α decls1
hdag2 : IsDag α decls2
hbounds1 : start < decls1.size
hbounds2 : start < decls2.size
hprefix : IsPrefix decls1 decls2
hidx1 : decls2[start] = decls1[start]
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : decls2[start] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := go lidx✝ decls2 assign ⋯ hdag2;
    let rval := go ridx✝ decls2 assign ⋯ hdag2;
    xor lval linv✝ && xor rval rinv✝) =
    match elem : decls1[start] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := go lhs decls1 assign ⋯ hdag1;
      let rval := go rhs decls1 assign ⋯ hdag1;
      xor lval linv && xor rval rinv