-- 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✝
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 ⋯ ⋯ ^^ linv✝) &&
      (denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ ^^ rinv✝)) =
    ((⟦assign, { aig := aig, ref := input.lhs.ref }⟧ ^^ input.lhs.inv) &&
      (⟦assign, { aig := aig, ref := input.rhs.ref }⟧ ^^ input.rhs.inv))

Tactic:
congr 2

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

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✝
⊢ linv✝ = input.lhs.inv

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 }⟧

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

Proof state:
case h_2
α : 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:
next heq =>
rw [mkGate, Array.getElem_push_eq] at heq
contradiction

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

Tactic:
unfold denote

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

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✝
⊢ linv✝ = input.lhs.inv

Tactic:
simp [heq3]

Result:
no goals

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✝
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))

Tactic:
dsimp only

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✝
⊢ ((denote.go lidx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ ^^ linv✝) &&
      (denote.go ridx✝ (aig.mkGate input).aig.decls assign ⋯ ⋯ ^^ 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
lidx✝ ridx✝ : Nat
linv✝ rinv✝ : Bool
heq : (aig.mkGate input).aig.decls[(aig.mkGate input).ref.gate] = 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:
rw [mkGate, Array.getElem_push_eq] at heq

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✝
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))