case final h₁ h₂ => 
  rw [get?_some_to_obj?_some h₁, get?_some_to_obj?_some h₂, Option.map_some]
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
no goals