Theorem: Reactor.Equivalent.mem_iff (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ i ∈ rtr₁[cpt] ↔ i ∈ rtr₂[cpt]
Tactic:
simp [Partial.mem_iff, obj?_some_iff e]
State after:
no goals