-- 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:
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 ⋯)

Tactic:
next h =>
simp only [not_exists, not_and] at h
specialize h a hmem
contradiction

Result:
no goals

Proof state:
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
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' : (relabel g (relabel r aig)).UnsatAt idx ⋯
⊢ ⟦assign, { aig := aig, ref := { gate := idx, hgate := hidx2 } }⟧ = false

Tactic:
specialize h' assign

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
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, { aig := relabel g (relabel r aig), ref := { gate := idx, hgate := ⋯ } }⟧ = false
⊢ ⟦assign, { aig := aig, ref := { gate := idx, hgate := hidx2 } }⟧ = false

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
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 : ∀ (x : α), x ∈ aig → ¬r x = r a
⊢ assign a = assign (Classical.choice ⋯)

Tactic:
specialize h a hmem

Result:
α : 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 : ¬r a = r a
⊢ assign a = assign (Classical.choice ⋯)

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

Tactic:
simp only [not_exists, not_and] at h

Result:
α : 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 : ∀ (x : α), x ∈ aig → ¬r x = r a
⊢ assign a = assign (Classical.choice ⋯)

Proof state:
case intro
α : 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
left✝ : h.choose ∈ aig
heq : r h.choose = r a
⊢ assign a = assign h.choose

Tactic:
specialize hinj _ _ (by assumption) (by assumption) heq

Result:
case intro
α : 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
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
left✝ : h.choose ∈ aig
heq : r h.choose = r a
hinj : h.choose = a
⊢ assign a = assign h.choose

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 : α), a ∈ aig → assign a = ((assign ∘ g) ∘ r) a

Tactic:
intro a hmem

Result:
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 ∘ g) ∘ r) a