no goals
V : Type ?u.109674
V₁ : Type u_2
V₂ : Type u_1
V₃ : Type ?u.109683
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f g : NormedAddGroupHom V₁ V₂
⊢ Function.Injective toFun
apply coe_inj