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

Tactic:
simp [denote_idx_const heq]

Result:
no goals

Proof state:
α : 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
⊢ lhs < aig.decls.size

Tactic:
omega

Result:
no goals

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 : α),
    aig.decls[idx] = Decl.atom a →
      ⟦assign1, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ =
        ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

Tactic:
intro a 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, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ =
    ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

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 a = assign2 a

Tactic:
apply h

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
⊢ a ∈ aig

Proof state:
α : 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
⊢ ⟦assign1, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ =
    ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

Tactic:
apply denote_idx_trichotomy

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),
    aig.decls[idx] = Decl.const b →
      ⟦assign1, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ =
        ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

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 : α),
    aig.decls[idx] = Decl.atom a →
      ⟦assign1, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧ =
        ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

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

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),
    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:
intro lhs rhs linv rinv 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 := idx, hgate := hidx } }⟧ =
    ⟦assign2, { aig := aig, ref := { gate := idx, hgate := hidx } }⟧

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
⊢ aig.decls[idx] ∈ aig.decls.toList

Tactic:
apply Array.getElem_mem_toList

Result:
no goals

Proof state:
α : 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
⊢ rhs < aig.decls.size

Tactic:
omega

Result:
no goals

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

Tactic:
rw [denote_congr assign1 assign2 aig lhs (by omega) h]

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
⊢ ((⟦assign2, { 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
this : lhs < idx ∧ rhs < idx
⊢ ((⟦assign2, { 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:
rw [denote_congr assign1 assign2 aig rhs (by omega) h]

Result:
no goals