exact depOverlap (e.obj?_rcn_eq.symm ▸ h₁) (e.obj?_rcn_eq.symm ▸ h₂) ‹_› ‹_› ‹_›
case depOverlap
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
i₁✝ : Component.idType Component.rcn
rcn₁✝ : Component.type α Component.rcn
i₂✝ : Component.idType Component.rcn
rcn₂✝ : Component.type α Component.rcn
d✝ : Reaction.Dependency
h₁ : rtr₂[Component.rcn][i₁✝] = some rcn₁✝
h₂ : rtr₂[Component.rcn][i₂✝] = some rcn₂✝
a✝² : d✝ ∈ rcn₁✝.deps Kind.out
a✝¹ : d✝ ∈ rcn₂✝.deps Kind.in
a✝ : d✝.cpt ≠ Component.Valued.stv
⊢ i₁✝ <[rtr₁] i₂✝
no goals