Theorem: AIG.Entrypoint.relabel_unsat_iff (LeanSAT/AIG/Relabel.lean)

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ (relabel f entry).unsat ↔ entry.unsat
Tactic:
simp [relabel, unsat]
State after:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ (AIG.relabel f entry.aig).unsatAt entry.ref.gate ⋯ ↔ entry.aig.unsatAt entry.ref.gate ⋯

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ (AIG.relabel f entry.aig).unsatAt entry.ref.gate ⋯ ↔ entry.aig.unsatAt entry.ref.gate ⋯
Tactic:
rw [AIG.relabel_unsat_iff]
State after:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
inst✝ : Nonempty α
entry : Entrypoint α
f : α → β
hinj : ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
⊢ ∀ (x y : α), x ∈ entry.aig → y ∈ entry.aig → f x = f y → x = y
Tactic:
assumption
State after:
no goals