Theorem: Reactor.mem_ids_iff (ReactorModel/Objects/Reactor/Theorems/Finite.lean)

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