case H
V : Type ?u.478704
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type u_3
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ ↑(NormedAddGroupHom.comp 0 f) x✝ = ↑0 x✝
V : Type ?u.478704
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type u_3
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
⊢ NormedAddGroupHom.comp 0 f = 0
ext
no goals
case H
V : Type ?u.478704
V₁ : Type u_1
V₂ : Type u_2
V₃ : Type u_3
inst✝³ : SeminormedAddCommGroup V
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f✝ g f : NormedAddGroupHom V₁ V₂
x✝ : V₁
⊢ ↑(NormedAddGroupHom.comp 0 f) x✝ = ↑0 x✝
rfl