rw [
  refresh, set_preserves (by simp : .inp ≠ .act), set_preserves (by simp : .inp ≠ .out), 
  set_updated $ 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.inp] = Partial.map (fun x => Value.absent) (rtr[Component.inp])
no goals