case final.nested e _ _ _ _ _ hn => exact nested hn (e (c := .rtr) (.inl $ by simp) ▸ hn) (refl _)
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
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
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝ : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn a✝ ∼ StrictMember.nested ⋯ a✝
no goals