case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ ↑(NormedAddGroupHom.comp (completion g) (completion f)) x = ↑(completion (NormedAddGroupHom.comp g f)) x
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
⊢ NormedAddGroupHom.comp (completion g) (completion f) = completion (NormedAddGroupHom.comp g f)
ext x
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ Completion.map (↑g ∘ ↑f) x = Completion.map (↑(NormedAddGroupHom.comp g f)) x
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ ↑(NormedAddGroupHom.comp (completion g) (completion f)) x = ↑(completion (NormedAddGroupHom.comp g f)) x
rw [NormedAddGroupHom.coe_comp, NormedAddGroupHom.completion_def,
  NormedAddGroupHom.completion_coe_to_fun, NormedAddGroupHom.completion_coe_to_fun,
  Completion.map_comp g.uniformContinuous f.uniformContinuous]
no goals
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ Completion.map (↑g ∘ ↑f) x = Completion.map (↑(NormedAddGroupHom.comp g f)) x
rfl