have h₄' := mem_get?_iff (get?_rtr_some_equiv e h₂' h₂) (cpt := .rcn) |>.mpr h₄
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
⊢ iₘ✝ <[rtr₁] iᵣ✝
case mutNest
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e✝ : rtr₁ ≈ rtr₂
i✝ : Component.idType Component.rtr
rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
iₘ✝ : ID
m✝ : Component.type (Component.type α Component.rtr) Component.rcn
iᵣ✝ : ID
h₁ : rtr₂[Component.rtr][i✝] = some rtr₁✝
h₂ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₃ : rtr₁✝{Component.rcn}{iₘ✝} = some m✝
a✝ : Reaction.Mutates m✝
h₄ : iᵣ✝ ∈ rtr₂✝{Component.rcn}
w✝¹ : Component.type α Component.rtr
h₁' : rtr₁[Component.rtr][i✝] = some w✝¹
e : w✝¹ ≈ rtr₁✝
w✝ : Component.type (Component.type α Component.rtr) Component.rtr
h₂' : w✝¹{Component.rtr}{j✝} = some w✝
h₄' : iᵣ✝ ∈ w✝{Component.rcn}
⊢ iₘ✝ <[rtr₁] iᵣ✝