Theorem: Decl.relabel_gate (LeanSAT/AIG/Relabel.lean)

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h : relabel f decls[idx] = gate lhs rhs linv rinv
⊢ decls[idx] = gate lhs rhs linv rinv
Tactic:
unfold relabel at h
State after:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (f a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    gate lhs rhs linv rinv
⊢ decls[idx] = gate lhs rhs linv rinv

State before:
α : Type
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : DecidableEq α
β : Type
inst✝² : BEq β
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
decls : Array (Decl α)
f : α → β
hidx : idx < decls.size
h :
  (match decls[idx] with
    | const b => const b
    | atom a => atom (f a)
    | gate lhs rhs linv rinv => gate lhs rhs linv rinv) =
    gate lhs rhs linv rinv
⊢ decls[idx] = gate lhs rhs linv rinv
Tactic:
split at h <;> simp_all
State after:
no goals