Theorem: Reactor.Equivalent.obj?_some_iff (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∃ o₁, rtr₁[cpt][i] = some o₁) ↔ ∃ o₂, rtr₂[cpt][i] = some o₂
Tactic:
simp [←Object.iff_obj?_some, Object.equiv_exists_object_iff e]
State after:
no goals