simp [←Object.iff_obj?_some, Object.equiv_exists_object_iff e]
α : 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₂
no goals