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