case cons.inl tl hi h =>
  subst h
  simp [go, hv]
  have e := @LawfulUpdatable.equiv _ cpt i v _ rtr
  have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
  by_cases ht : i ∈ tl
  case pos => exact hi ho' hv ht
  case neg => simp [set.go_preserves ho' (.inr $ .inl ht), ho' ▸ obj?_updated, ho]
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h : i = head✝
⊢ go rtr cpt vs (head✝ :: tl)[Component.val cpt][i] = some v
no goals