exact Object.iff_obj?_some.mp $ obj?_root_some ho ▸ ⟨.final h⟩
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ rtr[Component.rtr][↑i] = some o
no goals