case inl h =>
  have ⟨m', h'⟩ := Object.def.mp h.choose_spec
  simp [←h', m.unique m']
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∃ o, Object rtr cpt i o
⊢ some (Exists.choose h) = some (Member.object m)
no goals