rw [Equivalent.ids_eq set_equiv, Partial.const_ids _ _]
α : Type
inst✝¹ : Proper α
inst✝ : Finite α
acts : ID ⇀ Value
rtr : α
h : Partial.ids acts = Partial.ids (rtr[Component.act])
⊢ Partial.ids (Partial.const (Partial.ids (rtr[Component.out])) Value.absent) =
    Partial.ids
      (set rtr Component.Valued.inp
          (Partial.const (Partial.ids (rtr[Component.inp])) Value.absent)[Component.val Component.Valued.out])
no goals