case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type ?u.12924
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
x : G
⊢ ↑(NormedAddGroupHom.comp (completion f) toCompl) x = ↑(NormedAddGroupHom.comp toCompl f) x
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type ?u.12924
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
⊢ NormedAddGroupHom.comp (completion f) toCompl = NormedAddGroupHom.comp toCompl f
ext x
no goals
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type ?u.12924
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
x : G
⊢ ↑(NormedAddGroupHom.comp (completion f) toCompl) x = ↑(NormedAddGroupHom.comp toCompl f) x
simp