case _ v _ =>
  have e := @LawfulUpdatable.equiv _ cpt hd v _ rtr
  have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
  exact hi ho' hv ht
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : 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 ∈ tail✝ → go rtr cpt vs tail✝[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✝
ht : i ∈ tail✝
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
⊢ go (update rtr cpt hd v) cpt vs tail✝[Component.val cpt][i] = some v✝
no goals