no goals
V : Type ?u.210329
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.210338
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g✝ f g : NormedAddGroupHom V₁ V₂
h : toAddMonoidHom f = toAddMonoidHom g
⊢ ↑f = ↑g
rw [←coe_toAddMonoidHom f, ←coe_toAddMonoidHom g, h]