case final.get?_rtr_some_equiv e _ _ =>
  intro j _ _ h₁ h₂
  have h := e (c := .rtr) (j := j) (.inl $ by simp)
  simp_all
  apply Equivalent.refl
α : 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₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
no goals