simp [obj?]
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ rtr[cpt][i] = some (Member.object m)
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ (if h : ∃ o, Object rtr cpt i o then some (Exists.choose h) else none) = some (Member.object m)