-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem relabelNat_unsat_iff [Nonempty α] {aig : AIG α} {hidx1} {hidx2} :
    (aig.relabelNat).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2

Proof state:
α : Type
inst✝² : DecidableEq α
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)[x]? with
    | some var => var
    | none => 0) =
    match (RelabelNat.State.ofAIG aig)[y]? with
    | some var => var
    | none => 0
⊢ x = y

Tactic:
split at heq

Result:
case h_1
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝
heq :
  var✝ =
    match (RelabelNat.State.ofAIG aig)[y]? with
    | some var => var
    | none => 0
⊢ x = y

case h_2
α : Type
inst✝² : DecidableEq α
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)[x]? = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig)[y]? with
    | some var => var
    | none => 0
⊢ x = y

Proof state:
α : Type
inst✝² : DecidableEq α
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)[x]? with
            | some var => var
            | none => 0) =
            match (RelabelNat.State.ofAIG aig)[y]? with
            | some var => var
            | none => 0) →
          x = y

Tactic:
intro x y hx hy heq

Result:
α : Type
inst✝² : DecidableEq α
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)[x]? with
    | some var => var
    | none => 0) =
    match (RelabelNat.State.ofAIG aig)[y]? with
    | some var => var
    | none => 0
⊢ x = y

Proof state:
case ha
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig)[x]? = some ?n

Tactic:
assumption

Result:
no goals

Proof state:
case intro
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = none
heq : var✝ = 0
n : Nat
hn : (RelabelNat.State.ofAIG aig)[y]? = some n
⊢ False

Tactic:
simp [hcase2] at hn

Result:
no goals

Proof state:
case h_2
α : Type
inst✝² : DecidableEq α
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)[x]? = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig)[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

Result:
no goals

Proof state:
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = some var✝
heq : var✝¹ = var✝
⊢ x = y

Tactic:
apply RelabelNat.State.ofAIG_find_unique

Result:
case ha
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig)[x]? = some ?n

case a
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG ?aig)[y]? = some ?n

case n
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = some var✝
heq : var✝¹ = var✝
⊢ Nat

case aig
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = some var✝
heq : var✝¹ = var✝
⊢ AIG α

Proof state:
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = none
heq : var✝ = 0
⊢ False

Tactic:
rcases RelabelNat.State.ofAIG_find_some y hy with ⟨n, hn⟩

Result:
case intro
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝
x✝ : Option Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = none
heq : var✝ = 0
n : Nat
hn : (RelabelNat.State.ofAIG aig)[y]? = some n
⊢ False

Proof state:
case a
α : Type
inst✝² : DecidableEq α
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)[x]? = some var✝¹
x✝ : Option Nat
var✝ : Nat
hcase2 : (RelabelNat.State.ofAIG aig)[y]? = some var✝
heq : var✝¹ = var✝
⊢ (RelabelNat.State.ofAIG aig)[y]? = some var✝

Tactic:
assumption

Result:
no goals