case H
V : Type ?u.485294
W : Type ?u.485297
V₁ : Type u_1
V₂ : Type u_3
V₃ : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : NormedAddGroupHom.comp g f = 0
x✝ : V₁
⊢ ↑(NormedAddGroupHom.comp (incl (ker g)) (lift f g h)) x✝ = ↑f x✝
V : Type ?u.485294
W : Type ?u.485297
V₁ : Type u_1
V₂ : Type u_3
V₃ : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : NormedAddGroupHom.comp g f = 0
⊢ NormedAddGroupHom.comp (incl (ker g)) (lift f g h) = f
ext
no goals
case H
V : Type ?u.485294
W : Type ?u.485297
V₁ : Type u_1
V₂ : Type u_3
V₃ : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : SeminormedAddCommGroup W
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₁ V₂
g : NormedAddGroupHom V₂ V₃
h : NormedAddGroupHom.comp g f = 0
x✝ : V₁
⊢ ↑(NormedAddGroupHom.comp (incl (ker g)) (lift f g h)) x✝ = ↑f x✝
rfl