rw [refresh, set_updated $ h ▸ (Equivalent.ids_eq $ Equivalent.trans set_equiv set_equiv)]
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ refresh rtr acts[Component.act] = acts
no goals