have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
ho₂ : rtr[Component.rtr][c₂] = some con₂
hc₂ : con₂{cpt}{j} = some o₂
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
⊢ c₁ = c₂
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
m₂ : Member Component.rtr c₂ rtr
ho₂ : rtr[Component.rtr][c₂] = some (Member.object m₂)
hc₂ : Member.object m₂{cpt}{j} = some o₂
⊢ c₁ = c₂