have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
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
e : rtr ≈ update rtr cpt i v
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
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
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v