case pos =>
  have ⟨_, h₂⟩ := get?_some_iff e |>.mp h₁
  have ⟨_, h₁⟩ := h₁
  exact get?_rcn_some_eq e h₁ h₂ ▸ h₁ |>.symm ▸ h₂
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∃ o, rtr₁{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
no goals