no goals
V : Type ?u.513561
W : Type ?u.513564
V₁ : Type u_1
V₂ : Type u_4
V₃ : Type u_6
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_3
W₂ : Type u_2
W₃ : Type u_5
inst✝² : SeminormedAddCommGroup W₁
inst✝¹ : SeminormedAddCommGroup W₂
inst✝ : SeminormedAddCommGroup W₃
g : NormedAddGroupHom V W
f₁ g₁ : NormedAddGroupHom V₁ W₁
f₂ g₂ : NormedAddGroupHom V₂ W₂
f₃ g₃ : NormedAddGroupHom V₃ W₃
φ : NormedAddGroupHom V₁ V₂
ψ : NormedAddGroupHom W₁ W₂
φ' : NormedAddGroupHom V₂ V₃
ψ' : NormedAddGroupHom W₂ W₃
hf : NormedAddGroupHom.comp ψ f₁ = NormedAddGroupHom.comp f₂ φ
hf' : NormedAddGroupHom.comp ψ' f₂ = NormedAddGroupHom.comp f₃ φ'
⊢ NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) f₁ = NormedAddGroupHom.comp f₃ (NormedAddGroupHom.comp φ' φ)
rw [comp_assoc, hf, ← comp_assoc, hf', comp_assoc]