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

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
x : α
⊢ idx < aig.decls.size
Tactic:
rw [← relabel_size_eq_size (f := f)]
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
x : α
⊢ idx < (relabel f aig).decls.size

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
x : α
⊢ idx < (relabel f aig).decls.size
Tactic:
omega
State after:
no goals

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
⊢ ∃ x, aig.decls[idx] = Decl.atom x ∧ a = f x
Tactic:
apply Decl.relabel_atom
State after:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
⊢ Decl.relabel (fun x => f x) aig.decls[idx] = Decl.atom a

State before:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
a : β
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.atom a
⊢ Decl.relabel (fun x => f x) aig.decls[idx] = Decl.atom a
Tactic:
simpa [relabel] using h
State after:
no goals