-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
    ⟦aig.mkGate input, assign⟧
      =
    ((⟦aig, input.lhs.ref, assign⟧ ^^ input.lhs.inv) && (⟦aig, input.rhs.ref, assign⟧ ^^ input.rhs.inv))

Proof state:
α : Type
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✝
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = 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 ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Tactic:
injection heq with heq1 heq2 heq3 heq4

Result:
α : Type
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✝
⊢ (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 ⋯ ⋯;
    (lval ^^ linv✝) && (rval ^^ rinv✝)) =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Proof state:
case e_x.e_a.hprefix
α : Type
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✝
⊢ IsPrefix aig.decls (aig.mkGate input).aig.decls

Tactic:
apply LawfulOperator.isPrefix_aig

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = Decl.const b✝
⊢ b✝ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Tactic:
contradiction

Result:
no goals

Proof state:
case h_1
α : Type
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✝ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

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

Result:
no goals

Proof state:
α : Type
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✝ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

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

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
b✝ : Bool
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = Decl.const b✝
⊢ b✝ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Proof state:
case e_y.e_a.hprefix
α : Type
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✝
⊢ IsPrefix aig.decls (aig.mkGate input).aig.decls

Tactic:
apply LawfulOperator.isPrefix_aig

Result:
no goals

Proof state:
case e_x.e_a
α : Type
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 ⋯ ⋯ =
    denote.go { aig := aig, ref := input.lhs.ref }.ref.gate { aig := aig, ref := input.lhs.ref }.aig.decls assign ⋯ ⋯

Tactic:
simp only [heq1]

Result:
case e_x.e_a
α : Type
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 ⋯ ⋯ = denote.go lidx✝ aig.decls assign ⋯ ⋯

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq : Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv = Decl.atom idx✝
⊢ assign idx✝ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Tactic:
contradiction

Result:
no goals

Proof state:
case e_y.e_a
α : Type
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 ⋯ ⋯ =
    denote.go { aig := aig, ref := input.rhs.ref }.ref.gate { aig := aig, ref := input.rhs.ref }.aig.decls assign ⋯ ⋯

Tactic:
simp only [heq2]

Result:
case e_y.e_a
α : Type
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 ⋯ ⋯ = denote.go ridx✝ aig.decls assign ⋯ ⋯