have ⟨m⟩ := Object.iff_obj?_some.mpr ho
α : Type
inst✝ : Hierarchical α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
cpt : Component
i : ID
o : Component.type (Component.type α Component.rtr) cpt
ho : rtr[Component.rtr][c] = some con
hc : con{cpt}{i} = some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
α : Type
inst✝ : Hierarchical α
rtr : α
c : Component.idType Component.rtr
cpt : Component
i : ID
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}{i} = some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o