simp [Option.eq_none_iff_forall_not_mem, iff_obj?_some]
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
⊢ (∀ (o : Component.type α cpt), ¬Object rtr cpt i o) ↔ rtr[cpt][i] = none
no goals