case nested e => simp_all [e (c := c) (.inl $ by simp)]
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr✝ : α
o✝¹ : Component.type α (Component.val c)
h₁ : rtr✝{Component.val c}{j} = some o✝¹
rtr₂ : α
o✝ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr✝{Component.rtr}{j✝} = some n₁✝
a✝ : rtr₂{Component.rtr}{j✝} = some n₂✝
e : rtr✝ ≃[Component.rtr][j✝] rtr₂
⊢ o✝¹ = o✝
no goals