no goals
V : Type ?u.481267
W : Type ?u.481270
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type ?u.481279
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
v : V₁
⊢ v ∈ ker f ↔ ↑f v = 0
erw [f.toAddMonoidHom.mem_ker, coe_toAddMonoidHom]