case some =>
  have ⟨_, ho₂⟩ := obj?_some_iff u |>.mp ⟨_, ho₁⟩ 
  have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
  have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
  simp [ho₂, m₁.lawfulMemUpdate_object_preserved u h 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
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
⊢ rtr₂[Component.val c][j] = some val✝
no goals