have ⟨_, h₁⟩ := h₁
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∃ o, rtr₁{Component.rcn}{i} = some o
w✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some w✝
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁✝ : ∃ o, rtr₁{Component.rcn}{i} = some o
w✝¹ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some w✝¹
w✝ : Component.type α Component.rcn
h₁ : rtr₁{Component.rcn}{i} = some w✝
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}