-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_congr (assign1 assign2 : α → Bool) (aig : AIG α) (idx : Nat)
    (hidx : idx < aig.decls.size) (h : ∀ a, a ∈ aig → assign1 a = assign2 a) :
    ⟦aig, ⟨idx, hidx⟩, assign1⟧ = ⟦aig, ⟨idx, hidx⟩, assign2⟧

Proof state:
case hatom.a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ a ∈ aig

Tactic:
rw [mem_def, ← heq, Array.mem_def]

Result:
case hatom.a
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ aig.decls[idx] ∈ aig.decls.toList

Proof state:
case hconst
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ∀ (b : Bool),
    aig.decls[idx] = Decl.const b →
      ⟦assign1, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ =
        ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

Tactic:
intro b heq

Result:
case hconst
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
b : Bool
heq : aig.decls[idx] = Decl.const b
⊢ ⟦assign1, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ =
    ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

Proof state:
case hgate
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ ⟦assign1, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ =
    ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

Tactic:
simp only [denote_idx_gate heq]

Result:
case hgate
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ ((⟦assign1, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign1, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv)) =
    ((⟦assign2, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign2, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv))

Proof state:
case hgate
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
⊢ ((⟦assign1, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign1, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv)) =
    ((⟦assign2, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign2, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv))

Tactic:
have := aig.invariant hidx heq

Result:
case hgate
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
lhs rhs : Nat
linv rinv : Bool
heq : aig.decls[idx] = Decl.gate lhs rhs linv rinv
this : lhs < idx ∧ rhs < idx
⊢ ((⟦assign1, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign1, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv)) =
    ((⟦assign2, { aig := aig, ref := { gate := lhs, hgate := ⋯ } }⟧ ^^ linv) &&
      (⟦assign2, { aig := aig, ref := { gate := rhs, hgate := ⋯ } }⟧ ^^ rinv))

Proof state:
case hatom
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ ⟦assign1, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ =
    ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

Tactic:
simp only [denote_idx_atom heq]

Result:
case hatom
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
a : α
heq : aig.decls[idx] = Decl.atom a
⊢ assign1 a = assign2 a