exact ⟨_, h₁, Equivalent.obj?_rtr_equiv e h₁ h₂⟩
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₂ : rtr₂[Component.rtr][i] = some n₂
w✝ : Component.type α Component.rtr
h₁ : rtr₁[Component.rtr][i] = some w✝
⊢ ∃ n₁, rtr₁[Component.rtr][i] = some n₁ ∧ n₁ ≈ n₂
no goals