case H.a
V : Type ?u.514605
W : Type ?u.514608
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₂ φ
hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ
hf' : NormedAddGroupHom.comp ψ' f₂ = NormedAddGroupHom.comp f₃ φ'
hg' : NormedAddGroupHom.comp ψ' g₂ = NormedAddGroupHom.comp g₃ φ'
x✝ : { x // x ∈ equalizer f₁ g₁ }
⊢ ↑(↑(NormedAddGroupHom.comp (map φ' ψ' hf' hg') (map φ ψ hf hg)) x✝) =
    ↑(↑(map (NormedAddGroupHom.comp φ' φ) (NormedAddGroupHom.comp ψ' ψ)
            (_ :
              NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) f₁ =
                NormedAddGroupHom.comp f₃ (NormedAddGroupHom.comp φ' φ))
            (_ :
              NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) g₁ =
                NormedAddGroupHom.comp g₃ (NormedAddGroupHom.comp φ' φ)))
        x✝)
V : Type ?u.514605
W : Type ?u.514608
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₂ φ
hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ
hf' : NormedAddGroupHom.comp ψ' f₂ = NormedAddGroupHom.comp f₃ φ'
hg' : NormedAddGroupHom.comp ψ' g₂ = NormedAddGroupHom.comp g₃ φ'
⊢ NormedAddGroupHom.comp (map φ' ψ' hf' hg') (map φ ψ hf hg) =
    map (NormedAddGroupHom.comp φ' φ) (NormedAddGroupHom.comp ψ' ψ)
      (_ :
        NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) f₁ =
          NormedAddGroupHom.comp f₃ (NormedAddGroupHom.comp φ' φ))
      (_ :
        NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) g₁ =
          NormedAddGroupHom.comp g₃ (NormedAddGroupHom.comp φ' φ))
ext
no goals
case H.a
V : Type ?u.514605
W : Type ?u.514608
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₂ φ
hg : NormedAddGroupHom.comp ψ g₁ = NormedAddGroupHom.comp g₂ φ
hf' : NormedAddGroupHom.comp ψ' f₂ = NormedAddGroupHom.comp f₃ φ'
hg' : NormedAddGroupHom.comp ψ' g₂ = NormedAddGroupHom.comp g₃ φ'
x✝ : { x // x ∈ equalizer f₁ g₁ }
⊢ ↑(↑(NormedAddGroupHom.comp (map φ' ψ' hf' hg') (map φ ψ hf hg)) x✝) =
    ↑(↑(map (NormedAddGroupHom.comp φ' φ) (NormedAddGroupHom.comp ψ' ψ)
            (_ :
              NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) f₁ =
                NormedAddGroupHom.comp f₃ (NormedAddGroupHom.comp φ' φ))
            (_ :
              NormedAddGroupHom.comp (NormedAddGroupHom.comp ψ' ψ) g₁ =
                NormedAddGroupHom.comp g₃ (NormedAddGroupHom.comp φ' φ)))
        x✝)
rfl