have ⟨_, ho₂⟩ := obj?_some_iff e |>.mp ⟨_, ho₁⟩
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
⊢ some val✝ = rtr₂[Component.rcn][i]
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
w✝ : Component.type α Component.rcn
ho₂ : rtr₂[Component.rcn][i] = some w✝
⊢ some val✝ = rtr₂[Component.rcn][i]