-- 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
x✝ : Option Nat
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig)[x]? = some var✝
heq :
  var✝ =
    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
hcase1 : (RelabelNat.State.ofAIG aig)[x]? = some var✝¹
x✝ : Option Nat
var✝ : Nat
heq✝ : (RelabelNat.State.ofAIG aig)[y]? = some var✝
heq : var✝¹ = var✝
⊢ 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
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig)[x]? = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig)[y]? = none
heq : var✝ = 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
⊢ (relabel
          (fun x =>
            match (RelabelNat.State.ofAIG aig)[x]? with
            | some var => var
            | none => 0)
          aig).UnsatAt
      idx hidx1 ↔
    aig.UnsatAt idx hidx2

Tactic:
rw [relabel_unsat_iff]

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 : α),
    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

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
hcase : (RelabelNat.State.ofAIG aig)[x]? = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig)[y]? with
    | some var => var
    | none => 0
n : Nat
hn : (RelabelNat.State.ofAIG aig)[x]? = some n
⊢ False

Tactic:
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
⊢ aig.relabelNat.UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2

Tactic:
dsimp only [relabelNat, relabelNat']

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

Tactic:
exfalso

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
x✝ : Option Nat
hcase : (RelabelNat.State.ofAIG aig)[x]? = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig)[y]? with
    | some var => var
    | none => 0
⊢ False

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
⊢ x = y

Tactic:
exfalso

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

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
hcase : (RelabelNat.State.ofAIG aig)[x]? = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig)[y]? with
    | some var => var
    | none => 0
⊢ False

Tactic:
rcases RelabelNat.State.ofAIG_find_some x hx 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
hcase : (RelabelNat.State.ofAIG aig)[x]? = none
heq :
  0 =
    match (RelabelNat.State.ofAIG aig)[y]? with
    | some var => var
    | none => 0
n : Nat
hn : (RelabelNat.State.ofAIG aig)[x]? = some n
⊢ False

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
var✝ : Nat
hcase1 : (RelabelNat.State.ofAIG aig)[x]? = some var✝
x✝ : Option Nat
heq✝ : (RelabelNat.State.ofAIG aig)[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

Result:
no goals

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:
rw [heq]

Result:
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✝