case none => simp [obj?_none_iff e |>.mp ho₁]
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
ho₁ : rtr₁[Component.rcn][i] = none
⊢ none = rtr₂[Component.rcn][i]
no goals