-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_mkAtom {aig : AIG α} :
    ⟦(aig.mkAtom var), assign⟧ = assign var

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    assign var

Tactic:
rw [mkAtom, Array.getElem_push_eq] at heq

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.atom var = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    assign var

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
b✝ : Bool
heq : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.const b✝
⊢ b✝ = assign var

Tactic:
rw [mkAtom, Array.getElem_push_eq] at heq

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
b✝ : Bool
heq : Decl.atom var = Decl.const b✝
⊢ b✝ = assign var

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
idx✝ : α
heq : var = idx✝
⊢ assign idx✝ = assign var

Tactic:
rw [heq]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
b✝ : Bool
heq : Decl.atom var = Decl.const b✝
⊢ b✝ = assign var

Tactic:
contradiction

Result:
no goals

Proof state:
case h_3
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    assign var

Tactic:
next heq =>
rw [mkAtom, Array.getElem_push_eq] at heq
contradiction

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
idx✝ : α
heq : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = assign var

Tactic:
rw [mkAtom, Array.getElem_push_eq] at heq

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
idx✝ : α
heq : Decl.atom var = Decl.atom idx✝
⊢ assign idx✝ = assign var

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
heq : Decl.atom var = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    assign var

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
⊢ ⟦assign, aig.mkAtom var⟧ = assign var

Tactic:
unfold denote denote.go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
⊢ (match elem : (aig.mkAtom var).aig.decls[(aig.mkAtom var).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.mkAtom var).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkAtom var).aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    assign var

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
idx✝ : α
heq : Decl.atom var = Decl.atom idx✝
⊢ assign idx✝ = assign var

Tactic:
injection heq with heq

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
idx✝ : α
heq : var = idx✝
⊢ assign idx✝ = assign var

Proof state:
case h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
b✝ : Bool
heq✝ : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.const b✝
⊢ b✝ = assign var

Tactic:
next heq =>
rw [mkAtom, Array.getElem_push_eq] at heq
contradiction

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
⊢ (match elem : (aig.mkAtom var).aig.decls[(aig.mkAtom var).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.mkAtom var).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (aig.mkAtom var).aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    assign var

Tactic:
split

Result:
case h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
b✝ : Bool
heq✝ : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.const b✝
⊢ b✝ = assign var

case h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
idx✝ : α
heq✝ : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = assign var

case h_3
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq✝ : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.gate lidx✝ ridx✝ linv✝ rinv✝
⊢ (let_fun this := ⋯;
    let lval := denote.go lidx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    let rval := denote.go ridx✝ (aig.mkAtom var).aig.decls assign ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    assign var

Proof state:
case h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
var : α
aig : AIG α
idx✝ : α
heq✝ : (aig.mkAtom var).aig.decls[(aig.mkAtom var).ref.gate] = Decl.atom idx✝
⊢ assign idx✝ = assign var

Tactic:
next heq =>
rw [mkAtom, Array.getElem_push_eq] at heq
injection heq with heq
rw [heq]

Result:
no goals