exact set.go_updated ho ‹_› $ mem_ids_iff.mpr ⟨_, ho⟩
case h.some.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
x✝ : Value
heq✝ : vs i = some x✝
⊢ set rtr cpt vs[Component.val cpt][i] = some x✝
no goals