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

Tactic:
rw [← 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 } }⟧ =
    ⟦(assign ∘ g) ∘ r, { aig := aig, ref := { gate := idx, hgate := ⋯ } }⟧

Proof state:
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

Tactic:
next h =>
rcases Exists.choose_spec h with ⟨_, heq⟩
specialize hinj _ _ (by assumption) (by assumption) heq
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
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

Tactic:
have h' := unsat_relabel g 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' : (relabel g (relabel r aig)).UnsatAt idx ⋯
⊢ ⟦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
⊢ (relabel r aig).UnsatAt idx hidx1 → aig.UnsatAt idx hidx2

Tactic:
intro 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
⊢ ⟦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 : ∃ a_1, a_1 ∈ aig ∧ r a_1 = r a
left✝ : h.choose ∈ aig
heq : r h.choose = r a
⊢ a ∈ aig

Tactic:
assumption

Result:
no goals

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
left✝ : h.choose ∈ aig
heq : r h.choose = r a
⊢ h.choose ∈ aig

Tactic:
assumption

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

Tactic:
apply denote_congr

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