-- 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
⊢ ⟦assign, aig.mkGate input⟧ =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Tactic:
conv =>
  lhs
  unfold denote denote.go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
⊢ (match elem : (aig.mkGate input).aig.decls[(aig.mkGate input).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.mkGate input).aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs (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:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
input : aig.GateInput
idx✝ : α
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = 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:
rw [mkGate, Array.getElem_push_eq] at heq

Result:
α : 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))

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 ridx✝ aig.decls assign ⋯ ⋯

Tactic:
apply denote.go_eq_of_isPrefix

Result:
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

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✝
⊢ rinv✝ = input.rhs.inv

Tactic:
simp [heq4]

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 lidx✝ aig.decls assign ⋯ ⋯

Tactic:
apply denote.go_eq_of_isPrefix

Result:
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

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 ⋯ ⋯ = ⟦assign, { aig := aig, ref := input.rhs.ref }⟧

Tactic:
unfold denote

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 { aig := aig, ref := input.rhs.ref }.ref.gate { aig := aig, ref := input.rhs.ref }.aig.decls assign ⋯ ⋯