case H.a
V : Type ?u.512065
W : Type ?u.512068
V₁ : Type u_1
V₂ : Type ?u.512074
V₃ : Type ?u.512077
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_2
W₂ : Type ?u.512112
W₃ : Type ?u.512115
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₃
x✝ : { x // x ∈ equalizer f₁ g₁ }
⊢ ↑(↑(map (id V₁) (id W₁) (_ : NormedAddGroupHom.comp (id W₁) f₁ = NormedAddGroupHom.comp (id W₁) f₁)
            (_ : NormedAddGroupHom.comp (id W₁) g₁ = NormedAddGroupHom.comp (id W₁) g₁))
        x✝) =
    ↑(↑(id { x // x ∈ equalizer f₁ g₁ }) x✝)
V : Type ?u.512065
W : Type ?u.512068
V₁ : Type u_1
V₂ : Type ?u.512074
V₃ : Type ?u.512077
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_2
W₂ : Type ?u.512112
W₃ : Type ?u.512115
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₃
⊢ map (id V₁) (id W₁) (_ : NormedAddGroupHom.comp (id W₁) f₁ = NormedAddGroupHom.comp (id W₁) f₁)
      (_ : NormedAddGroupHom.comp (id W₁) g₁ = NormedAddGroupHom.comp (id W₁) g₁) =
    id { x // x ∈ equalizer f₁ g₁ }
ext
no goals
case H.a
V : Type ?u.512065
W : Type ?u.512068
V₁ : Type u_1
V₂ : Type ?u.512074
V₃ : Type ?u.512077
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type u_2
W₂ : Type ?u.512112
W₃ : Type ?u.512115
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₃
x✝ : { x // x ∈ equalizer f₁ g₁ }
⊢ ↑(↑(map (id V₁) (id W₁) (_ : NormedAddGroupHom.comp (id W₁) f₁ = NormedAddGroupHom.comp (id W₁) f₁)
            (_ : NormedAddGroupHom.comp (id W₁) g₁ = NormedAddGroupHom.comp (id W₁) g₁))
        x✝) =
    ↑(↑(id { x // x ∈ equalizer f₁ g₁ }) x✝)
rfl