have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
w✝ : Component.type α (Component.val c)
ho₂ : rtr₂[Component.val c][j] = some w✝
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
m₂ : Member (Component.val c) j rtr₂
ho₂ : rtr₂[Component.val c][j] = some (Member.object m₂)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)