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

Tactic:
rcases Exists.choose_spec h with ⟨_, 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
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

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

Tactic:
simp [hinj]

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

Tactic:
let g : β → α := fun b =>
  have em := Classical.propDecidable
  if h : ∃ a, a ∈ aig ∧ r a = b then h.choose else Classical.choice inferInstance

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

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

Tactic:
simp only [denote_relabel] at h'

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

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

Tactic:
simp only [Function.comp_apply, g]

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 (if h : ∃ a_1, a_1 ∈ aig ∧ r a_1 = r a then h.choose else 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 : ¬r a = r a
⊢ assign a = assign (Classical.choice ⋯)

Tactic:
contradiction

Result:
no goals