case final.mem_get?_iff e h₁ h₂ =>
  intro c j
  by_cases hc : c = cpt <;> try subst hc
  case neg => exact e.mem_iff (.inl hc)
  case pos =>
    by_cases hj : j = i <;> try subst hj
    case neg => exact e.mem_iff (.inr hj)
    case pos => simp [Partial.mem_iff, h₁, h₂]
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
no goals