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

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ (relabel f aig).unsatAt idx hidx1 ↔ aig.unsatAt idx hidx2
Tactic:
constructor
State after:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ (relabel f aig).unsatAt idx hidx1 → aig.unsatAt idx hidx2

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

State before:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ (relabel f aig).unsatAt idx hidx1 → aig.unsatAt idx hidx2

case mpr
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ aig.unsatAt idx hidx2 → (relabel f aig).unsatAt idx hidx1
Tactic:
. intro h assign
  have em := Classical.propDecidable
  let g : β → α := fun b =>
    if h:∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice inferInstance
  have h' := unsat_relabel g h
  specialize h' assign
  simp only [denote_relabel] at h'
  rw [← h']
  apply denote_congr
  . intro a hmem
    simp [g]
    split
    . next h =>
      rcases Exists.choose_spec h with ⟨_, heq⟩
      specialize hinj _ _ (by assumption) (by assumption) heq
      simp [hinj]
    . next h =>
      simp only [not_exists, not_and] at h
      specialize h a hmem
      contradiction
State after:
case mpr
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ aig.unsatAt idx hidx2 → (relabel f aig).unsatAt idx hidx1

State before:
case mpr
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ aig.unsatAt idx hidx2 → (relabel f aig).unsatAt idx hidx1
Tactic:
. apply unsat_relabel
State after:
no goals

State before:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ (relabel f aig).unsatAt idx hidx1 → aig.unsatAt idx hidx2
Tactic:
intro h assign
State after:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false

State before:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
have em := Classical.propDecidable
State after:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false

State before:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
let g : β → α := fun b =>
  if h:∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice inferInstance
State after:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false

State before:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
have h' := unsat_relabel g h
State after:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : (relabel g (relabel f aig)).unsatAt idx ⋯
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false

State before:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : (relabel g (relabel f aig)).unsatAt idx ⋯
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
specialize h' assign
State after:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := relabel g (relabel f aig), ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false

State before:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := relabel g (relabel f aig), ref := { gate := idx, hgate := ⋯ } }, assign⟧ = false
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
simp only [denote_relabel] at h'
State after:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false

State before:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ = false
Tactic:
rw [← h']
State after:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧

State before:
case mp
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
⊢ ⟦{ aig := aig, ref := { gate := idx, hgate := hidx2 } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧
Tactic:
apply denote_congr
State after:
case mp.h
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
⊢ ∀ (a : α), a ∈ aig → assign a = ((assign ∘ g) ∘ f) a

State before:
case mp.h
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
⊢ ∀ (a : α), a ∈ aig → assign a = ((assign ∘ g) ∘ f) a
Tactic:
. intro a hmem
  simp [g]
  split
  . next h =>
    rcases Exists.choose_spec h with ⟨_, heq⟩
    specialize hinj _ _ (by assumption) (by assumption) heq
    simp [hinj]
  . next h =>
    simp only [not_exists, not_and] at h
    specialize h a hmem
    contradiction
State after:
no goals

State before:
case mp.h
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
⊢ ∀ (a : α), a ∈ aig → assign a = ((assign ∘ g) ∘ f) a
Tactic:
intro a hmem
State after:
case mp.h
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
⊢ assign a = ((assign ∘ g) ∘ f) a

State before:
case mp.h
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
⊢ assign a = ((assign ∘ g) ∘ f) a
Tactic:
simp [g]
State after:
case mp.h
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
⊢ assign a = assign (if h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a then h.choose else Classical.choice ⋯)

State before:
case mp.h
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
⊢ assign a = assign (if h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a then h.choose else Classical.choice ⋯)
Tactic:
split
State after:
case mp.h.isTrue
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign h✝.choose

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

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

case mp.h.isFalse
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
. next h =>
  rcases Exists.choose_spec h with ⟨_, heq⟩
  specialize hinj _ _ (by assumption) (by assumption) heq
  simp [hinj]
State after:
case mp.h.isFalse
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)

State before:
case mp.h.isFalse
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
. next h =>
  simp only [not_exists, not_and] at h
  specialize h a hmem
  contradiction
State after:
no goals

State before:
case mp.h.isTrue
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f 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]
State after:
no goals

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign h.choose
Tactic:
rcases Exists.choose_spec h with ⟨_, heq⟩
State after:
case intro
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
⊢ assign a = assign h.choose

State before:
case intro
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
⊢ assign a = assign h.choose
Tactic:
specialize hinj _ _ (by assumption) (by assumption) heq
State after:
case intro
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
hinj : h.choose = a
⊢ assign a = assign h.choose

State before:
case intro
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
hinj : h.choose = a
⊢ assign a = assign h.choose
Tactic:
simp [hinj]
State after:
no goals

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
⊢ h.choose ∈ aig
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
left✝ : h.choose ∈ aig
heq : f h.choose = f a
⊢ a ∈ aig
Tactic:
assumption
State after:
no goals

State before:
case mp.h.isFalse
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h✝ : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
next h =>
simp only [not_exists, not_and] at h
specialize h a hmem
contradiction
State after:
no goals

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ¬∃ a_1, a_1 ∈ aig ∧ f a_1 = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
simp only [not_exists, not_and] at h
State after:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∀ (x : α), x ∈ aig → ¬f x = f a
⊢ assign a = assign (Classical.choice ⋯)

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ∀ (x : α), x ∈ aig → ¬f x = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
specialize h a hmem
State after:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ¬f a = f a
⊢ assign a = assign (Classical.choice ⋯)

State before:
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
h✝ : (relabel f aig).unsatAt idx hidx1
assign : α → Bool
em : (a : Prop) → Decidable a
g : β → α := fun b => if h : ∃ a, a ∈ aig ∧ f a = b then h.choose else Classical.choice ⋯
h' : ⟦{ aig := aig, ref := { gate := idx, hgate := ⋯ } }, (assign ∘ g) ∘ f⟧ = false
a : α
hmem : a ∈ aig
h : ¬f a = f a
⊢ assign a = assign (Classical.choice ⋯)
Tactic:
contradiction
State after:
no goals

State before:
case mpr
α : Type
inst✝⁶ : BEq α
inst✝⁵ : Hashable α
inst✝⁴ : DecidableEq α
β : Type
inst✝³ : BEq β
inst✝² : Hashable β
inst✝¹ : DecidableEq β
idx : Nat
inst✝ : Nonempty α
aig : AIG α
f : α → β
hidx1 : idx < (relabel f aig).decls.size
hidx2 : idx < aig.decls.size
hinj : ∀ (x y : α), x ∈ aig → y ∈ aig → f x = f y → x = y
⊢ aig.unsatAt idx hidx2 → (relabel f aig).unsatAt idx hidx1
Tactic:
apply unsat_relabel
State after:
no goals