Theorem: AIG.denote_idx_atom (LeanSAT/AIG/Lemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
a : α
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.atom a
⊢ ⟦{ aig := aig, ref := { gate := start, hgate := hstart } }, assign⟧ = assign a
Tactic:
unfold denote denote.go
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
a : α
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.atom a
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.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 := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    assign a

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
a : α
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.atom a
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.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 := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      xor lval linv && xor rval rinv) =
    assign a
Tactic:
split <;> simp_all
State after:
no goals