exact Equivalent.get?_rtr_some_equiv e h₁ h₂
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝¹ : Component.type α Component.rtr
h₁ : rtr✝{Component.rtr}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α Component.rtr
h₂ : rtr₂{Component.rtr}{i} = some o✝
⊢ object (final h₁) ≈ object (final h₂)
no goals