simp [Finite.ids, ←Partial.mem_def, Partial.mem_iff]
α : Type
cpt : Component
inst✝¹ : Hierarchical α
inst✝ : Finite α
rtr : α
i : Component.idType cpt
⊢ i ∈ Finite.ids rtr cpt ↔ ∃ o, rtr[cpt][i] = some o
no goals