Theorem: Reactor.Object.not_iff_obj?_none (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

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