case inl h h' => 
  have ⟨m', h'⟩ := Object.def.mp h'.choose_spec
  exact Option.some_inj.mp h ▸ h' ▸ ⟨m'⟩
α : Type
h✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h' : ∃ o, Object rtr cpt i o
h : some (Exists.choose h') = some o
⊢ Object rtr cpt i o
no goals