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

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ 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
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ idx < (relabel f aig).decls.size

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ 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
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ aig.decls[idx] = Decl.const b
Tactic:
apply Decl.relabel_const
State after:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ Decl.relabel ?f aig.decls[idx] = Decl.const b

case β
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ Type

case f
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ α → ?β

State before:
case h
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ Decl.relabel ?f aig.decls[idx] = Decl.const b

case β
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx : Nat
b : Bool
aig : AIG α
f : α → β
hidx : idx < (relabel f aig).decls.size
h : (relabel f aig).decls[idx] = Decl.const b
⊢ Type

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