Theorem: AIG.relabelNat_unsat_iff (LeanSAT/AIG/RelabelNat.lean)

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ aig.relabelNat.unsatAt idx hidx1 ↔ aig.unsatAt idx hidx2
Tactic:
dsimp [relabelNat, relabelNat']
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ (relabel
          (fun x =>
            match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0)
          aig).unsatAt
      idx hidx1 ↔
    aig.unsatAt idx hidx2

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ (relabel
          (fun x =>
            match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0)
          aig).unsatAt
      idx hidx1 ↔
    aig.unsatAt idx hidx2
Tactic:
rw [relabel_unsat_iff]
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ ∀ (x y : α),
    x ∈ aig →
      y ∈ aig →
        ((match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0) =
            match (RelabelNat.State.ofAIG aig).find? y with
            | some var => var
            | none => 0) →
          x = y

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
⊢ ∀ (x y : α),
    x ∈ aig →
      y ∈ aig →
        ((match (RelabelNat.State.ofAIG aig).find? x with
            | some var => var
            | none => 0) =
            match (RelabelNat.State.ofAIG aig).find? y with
            | some var => var
            | none => 0) →
          x = y
Tactic:
intro x y hx hy heq
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
heq :
  (match (RelabelNat.State.ofAIG aig).find? x with
    | some var => var
    | none => 0) =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
heq :
  (match (RelabelNat.State.ofAIG aig).find? x with
    | some var => var
    | none => 0) =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
split at heq
State after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
. next hcase1 =>
  split at heq
  . next hcase2 =>
    apply RelabelNat.State.ofAIG_find_unique
    . assumption
    . rw [heq]
      assumption
  . next hcase2 =>
    exfalso
    rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
    simp[hcase2] at hn
State after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
. next hcase =>
  exfalso
  rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩
  simp[hcase] at hn
State after:
no goals

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
next hcase1 =>
split at heq
. next hcase2 =>
  apply RelabelNat.State.ofAIG_find_unique
  . assumption
  . rw [heq]
    assumption
. next hcase2 =>
  exfalso
  rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
  simp[hcase2] at hn
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
split at heq
State after:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ x = y

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ x = y

case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Tactic:
. next hcase2 =>
  apply RelabelNat.State.ofAIG_find_unique
  . assumption
  . rw [heq]
    assumption
State after:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Tactic:
. next hcase2 =>
  exfalso
  rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
  simp[hcase2] at hn
State after:
no goals

State before:
case h_1
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ x = y
Tactic:
next hcase2 =>
apply RelabelNat.State.ofAIG_find_unique
. assumption
. rw [heq]
  assumption
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ x = y
Tactic:
apply RelabelNat.State.ofAIG_find_unique
State after:
case ha
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? x = some ?n

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? y = some ?n

case n
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ Nat

case aig
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ AIG α

State before:
case ha
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? x = some ?n

case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? y = some ?n

case n
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ Nat

case aig
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ AIG α
Tactic:
. assumption
State after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝¹

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝¹
Tactic:
. rw [heq]
  assumption
State after:
no goals

State before:
case ha
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig).find? x = some ?n
Tactic:
assumption
State after:
no goals

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝¹
Tactic:
rw [heq]
State after:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝

State before:
case a
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝¹ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig).find? y = some var✝
Tactic:
assumption
State after:
no goals

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Tactic:
next hcase2 =>
exfalso
rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
simp[hcase2] at hn
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ x = y
Tactic:
exfalso
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ False

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
⊢ False
Tactic:
rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩
State after:
case intro
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
n : Nat
hn : (RelabelNat.State.ofAIG aig).find? y = some n
⊢ False

State before:
case intro
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝¹ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig).find? x = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig).find? y = none
heq : var✝ = 0
n : Nat
hn : (RelabelNat.State.ofAIG aig).find? y = some n
⊢ False
Tactic:
simp[hcase2] at hn
State after:
no goals

State before:
case h_2
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
next hcase =>
exfalso
rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩
simp[hcase] at hn
State after:
no goals

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ x = y
Tactic:
exfalso
State after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ False

State before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
⊢ False
Tactic:
rcases RelabelNat.State.ofAIG_find_some x hx with ⟨n, hn⟩
State after:
case intro
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
n : Nat
hn : (RelabelNat.State.ofAIG aig).find? x = some n
⊢ False

State before:
case intro
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
idx : Nat
inst✝ : Nonempty α
aig : AIG α
hidx1 : idx < aig.relabelNat.decls.size
hidx2 : idx < aig.decls.size
x y : α
hx : x ∈ aig
hy : y ∈ aig
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig).find? x = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig).find? y with
    | some var => var
    | none => 0
n : Nat
hn : (RelabelNat.State.ofAIG aig).find? x = some n
⊢ False
Tactic:
simp[hcase] at hn
State after:
no goals