case inr.inl hd tl hi _ v _ h =>
  have e := @LawfulUpdatable.equiv _ cpt ‹_› v _ rtr
  have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
  push_neg at h
  simp [hi ho' $ .inr $ .inl h.right]
  injection ho' ▸ ho ▸ obj?_preserved_id h.left
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬(i = hd ∨ i ∈ tl)
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
no goals