-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_unsat_iff [Nonempty α] {aig : AIG α} {r : α → β} {hidx1} {hidx2}
    (hinj : ∀ x y, x ∈ aig → y ∈ aig → r x = r y → x = y) :
    (aig.relabel r).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2

Proof state:
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
r : α → β
hidx1 : idx < (relabel r aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y
⊢ (relabel r aig).UnsatAt idx hidx1 ↔ aig.UnsatAt idx hidx2

Tactic:
constructor

Result:
case mp
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
r : α → β
hidx1 : idx < (relabel r aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y
⊢ (relabel r aig).UnsatAt idx hidx1 → aig.UnsatAt idx hidx2

case mpr
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
r : α → β
hidx1 : idx < (relabel r aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y
⊢ aig.UnsatAt idx hidx2 → (relabel r aig).UnsatAt idx hidx1

Proof state:
case mp.h
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
r : α → β
hidx1 : idx < (relabel r aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y
h : (relabel r aig).UnsatAt idx hidx1
assign : α → Bool
g : β → α :=
  fun b =>
    let_fun em := Classical.propDecidable;
    if h : ∃ a, a ∈ aig ∧ r a = b then h.choose else Classical.choice ⋯
h' : ⟦(assign ∘ g) ∘ r, { aig := aig, ref := { gate := idx, hgate := ⋯ } }⟧ = false
a : α
hmem : a ∈ aig
⊢ assign a = assign (if h : ∃ a_1, a_1 ∈ aig ∧ r a_1 = r a then h.choose else Classical.choice ⋯)

Tactic:
split

Result:
case mp.h.isTrue
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
r : α → β
hidx1 : idx < (relabel r aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y
h : (relabel r aig).UnsatAt idx hidx1
assign : α → Bool
g : β → α :=
  fun b =>
    let_fun em := Classical.propDecidable;
    if h : ∃ a, a ∈ aig ∧ r a = b then h.choose else Classical.choice ⋯
h' : ⟦(assign ∘ g) ∘ r, { aig := aig, ref := { gate := idx, hgate := ⋯ } }⟧ = false
a : α
hmem : a ∈ aig
h✝ : ∃ a_1, a_1 ∈ aig ∧ r a_1 = r a
⊢ assign a = assign h✝.choose

case mp.h.isFalse
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
r : α → β
hidx1 : idx < (relabel r aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y
h : (relabel r aig).UnsatAt idx hidx1
assign : α → Bool
g : β → α :=
  fun b =>
    let_fun em := Classical.propDecidable;
    if h : ∃ a, a ∈ aig ∧ r a = b then h.choose else Classical.choice ⋯
h' : ⟦(assign ∘ g) ∘ r, { aig := aig, ref := { gate := idx, hgate := ⋯ } }⟧ = false
a : α
hmem : a ∈ aig
h✝ : ¬∃ a_1, a_1 ∈ aig ∧ r a_1 = r a
⊢ assign a = assign (Classical.choice ⋯)

Proof state:
case mpr
α : Type
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
r : α → β
hidx1 : idx < (relabel r aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y
⊢ aig.UnsatAt idx hidx2 → (relabel r aig).UnsatAt idx hidx1

Tactic:
apply unsat_relabel

Result:
no goals