induction d with
| prio h₁ h₂ h₃ =>
  have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
  exact prio h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
| depOverlap h₁ h₂ =>
  exact depOverlap (e.obj?_rcn_eq.symm ▸ h₁) (e.obj?_rcn_eq.symm ▸ h₂) ‹_› ‹_› ‹_›
| mutNorm h₁ h₂ h₃ =>
  have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
  exact mutNorm h₁' (get?_rcn_eq e ▸ h₂) (get?_rcn_eq e ▸ h₃) ‹_› ‹_›
| mutNest h₁ h₂ h₃ _ h₄ =>
  have ⟨_, h₁', e⟩ := obj?_rtr_equiv' e h₁
  have ⟨_, h₂'⟩ := get?_some_iff e (cpt := .rtr) |>.mpr ⟨_, h₂⟩
  have h₄' := mem_get?_iff (get?_rtr_some_equiv e h₂' h₂) (cpt := .rcn) |>.mpr h₄
  exact mutNest h₁' h₂' (get?_rcn_eq e ▸ h₃) ‹_› h₄'
| trans _ _ d₁ d₂ =>
  exact trans d₁ d₂
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
j₁ j₂ : ID
e : rtr₁ ≈ rtr₂
d : j₁ <[rtr₂] j₂
⊢ j₁ <[rtr₁] j₂
no goals