case neg =>
  have h₂ := get?_some_iff e |>.not.mp h₁
  push_neg at h₁ h₂
  simp [Option.eq_none_iff_forall_not_mem.mpr h₁, Option.eq_none_iff_forall_not_mem.mpr 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