case final.final e₁ _ h₁' _ _ h₂' e₂ =>
  exact RootEqualUpTo.ext (RootEqualUpTo.trans e₁.symm e₂) (h₂' ▸ h₁')
α : Type
inst✝ : Readable α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₁✝ rtr₂✝ : α
o✝¹ : Component.type α (Component.val cpt)
e₁ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝¹
h₁' : rtr₂✝{Component.val cpt}{i} = some v
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂' : rtr₂{Component.val cpt}{i} = some v
e₂ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ rtr₂✝ = rtr₂
no goals