rw [
  refresh, set_preserves (by simp : .out ≠ .act),
  set_updated $ by rw [Equivalent.ids_eq set_equiv, Partial.const_ids _ _],
  Partial.const_eq_map_const
]
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ refresh rtr acts[Component.out] = Partial.map (fun x => Value.absent) (rtr[Component.out])
no goals