rw [
  refresh, set_preserves (by simp : .stv ≠ .act), set_preserves (by simp : .stv ≠ .out), 
  set_preserves (by simp : .stv ≠ .inp)
]
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ refresh rtr acts[Component.stv] = rtr[Component.stv]
no goals