case H
V : Type u_2
W : Type u_3
V₁ : Type u_1
V₂ : Type ?u.506724
V₃ : Type ?u.506727
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type ?u.506759
W₂ : Type ?u.506762
W₃ : Type ?u.506765
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
h : NormedAddGroupHom.comp f φ = NormedAddGroupHom.comp g φ
x✝ : V₁
⊢ ↑(NormedAddGroupHom.comp (ι f g) (lift φ h)) x✝ = ↑φ x✝
V : Type u_2
W : Type u_3
V₁ : Type u_1
V₂ : Type ?u.506724
V₃ : Type ?u.506727
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type ?u.506759
W₂ : Type ?u.506762
W₃ : Type ?u.506765
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
h : NormedAddGroupHom.comp f φ = NormedAddGroupHom.comp g φ
⊢ NormedAddGroupHom.comp (ι f g) (lift φ h) = φ
ext
no goals
case H
V : Type u_2
W : Type u_3
V₁ : Type u_1
V₂ : Type ?u.506724
V₃ : Type ?u.506727
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : SeminormedAddCommGroup W
inst✝⁵ : SeminormedAddCommGroup V₁
inst✝⁴ : SeminormedAddCommGroup V₂
inst✝³ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V W
W₁ : Type ?u.506759
W₂ : Type ?u.506762
W₃ : Type ?u.506765
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
h : NormedAddGroupHom.comp f φ = NormedAddGroupHom.comp g φ
x✝ : V₁
⊢ ↑(NormedAddGroupHom.comp (ι f g) (lift φ h)) x✝ = ↑φ x✝
rfl