-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Relabel.lean
theorem relabel_gate {aig : AIG α} {r : α → β} {hidx : idx < (relabel r aig).decls.size}
    (h : (relabel r aig).decls[idx]'hidx = .gate lhs rhs linv rinv) :
    aig.decls[idx]'(by rw [← relabel_size_eq_size (r := r)]; omega) = .gate lhs rhs linv rinv

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ idx < aig.decls.size

Tactic:
rw [← relabel_size_eq_size (r := r)]

Result:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ idx < (relabel r aig).decls.size

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ idx < (relabel r aig).decls.size

Tactic:
omega

Result:
no goals

Proof state:
case h
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ Decl.relabel ?r aig.decls[idx] = Decl.gate lhs rhs linv rinv

case β
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ Type

case r
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ α → ?β

Tactic:
simpa [relabel] using h

Result:
no goals

Proof state:
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ aig.decls[idx] = Decl.gate lhs rhs linv rinv

Tactic:
apply Decl.relabel_gate

Result:
case h
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ Decl.relabel ?r aig.decls[idx] = Decl.gate lhs rhs linv rinv

case β
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ Type

case r
α : Type
inst✝³ : Hashable α
inst✝² : DecidableEq α
β : Type
inst✝¹ : Hashable β
inst✝ : DecidableEq β
idx lhs rhs : Nat
linv rinv : Bool
aig : AIG α
r : α → β
hidx : idx < (relabel r aig).decls.size
h : (relabel r aig).decls[idx] = Decl.gate lhs rhs linv rinv
⊢ α → ?β