case inr h =>
  push_neg at h
  specialize h m.object
  simp [Object.def] at h
α : 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
⊢ False
no goals