Theorem: AIG.denote_congr (LeanSAT/AIG/Lemmas.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign1 assign2 : α → Bool
aig : AIG α
idx : Nat
hidx : idx < aig.decls.size
h : ∀ (a : α), a ∈ aig → assign1 a = assign2 a
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
apply denote_idx_trichotomy
State after:
case hconst
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hatom
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hgate
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

State before:
case hconst
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hatom
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hgate
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
. intro b heq
  simp [denote_idx_const heq]
State after:
case hatom
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hgate
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

State before:
case hatom
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

case hgate
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
. intro a heq
  simp only [denote_idx_atom heq]
  apply h
  rw [mem_def]
  rw [← heq]
  rw [Array.mem_def]
  apply Array.getElem_mem_data
State after:
case hgate
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

State before:
case hgate
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
. intro lhs rhs linv rinv heq
  simp [denote_idx_gate heq]
  have := aig.inv idx lhs rhs linv rinv hidx heq
  rw [denote_congr assign1 assign2 aig lhs (by omega) h]
  rw [denote_congr assign1 assign2 aig rhs (by omega) h]
State after:
no goals

State before:
case hconst
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
intro b heq
State after:
case hconst
α : Type
inst✝² : BEq α
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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

State before:
case hconst
α : Type
inst✝² : BEq α
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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
simp [denote_idx_const heq]
State after:
no goals

State before:
case hatom
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
intro a heq
State after:
case hatom
α : Type
inst✝² : BEq α
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 := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

State before:
case hatom
α : Type
inst✝² : BEq α
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 := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
simp only [denote_idx_atom heq]
State after:
case hatom
α : Type
inst✝² : BEq α
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

State before:
case hatom
α : Type
inst✝² : BEq α
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
State after:
case hatom.a
α : Type
inst✝² : BEq α
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

State before:
case hatom.a
α : Type
inst✝² : BEq α
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]
State after:
case hatom.a
α : Type
inst✝² : BEq α
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
⊢ Decl.atom a ∈ aig.decls

State before:
case hatom.a
α : Type
inst✝² : BEq α
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
⊢ Decl.atom a ∈ aig.decls
Tactic:
rw [← heq]
State after:
case hatom.a
α : Type
inst✝² : BEq α
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

State before:
case hatom.a
α : Type
inst✝² : BEq α
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
Tactic:
rw [Array.mem_def]
State after:
case hatom.a
α : Type
inst✝² : BEq α
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.data

State before:
case hatom.a
α : Type
inst✝² : BEq α
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.data
Tactic:
apply Array.getElem_mem_data
State after:
no goals

State before:
case hgate
α : Type
inst✝² : BEq α
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 →
      ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
        ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
intro lhs rhs linv rinv heq
State after:
case hgate
α : Type
inst✝² : BEq α
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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧

State before:
case hgate
α : Type
inst✝² : BEq α
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
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign1⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := hidx } }, assign2⟧
Tactic:
simp [denote_idx_gate heq]
State after:
case hgate
α : Type
inst✝² : BEq α
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
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign1⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)

State before:
case hgate
α : Type
inst✝² : BEq α
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
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign1⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)
Tactic:
have := aig.inv idx lhs rhs linv rinv hidx heq
State after:
case hgate
α : Type
inst✝² : BEq α
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
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign1⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)

State before:
case hgate
α : Type
inst✝² : BEq α
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
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign1⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)
Tactic:
rw [denote_congr assign1 assign2 aig lhs (by omega) h]
State after:
case hgate
α : Type
inst✝² : BEq α
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
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)

State before:
case hgate
α : Type
inst✝² : BEq α
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
⊢ (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign1⟧ rinv) =
    (xor ⟦{ aig := aig, ref := { gate := lhs, hgate := ⋯ } }, assign2⟧ linv &&
      xor ⟦{ aig := aig, ref := { gate := rhs, hgate := ⋯ } }, assign2⟧ rinv)
Tactic:
rw [denote_congr assign1 assign2 aig rhs (by omega) h]
State after:
no goals

State before:
α : Type
inst✝² : BEq α
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
State after:
no goals

State before:
α : Type
inst✝² : BEq α
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
State after:
no goals