case H
G : Type u_1
inst✝³ : SeminormedAddCommGroup G
H : Type u_2
inst✝² : SeminormedAddCommGroup H
inst✝¹ : SeparatedSpace H
inst✝ : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom (Completion G) H
hg : ∀ (v : G), ↑f v = ↑g (↑G v)
v : Completion G
⊢ ↑(extension f) v = ↑g v
G : Type u_1
inst✝³ : SeminormedAddCommGroup G
H : Type u_2
inst✝² : SeminormedAddCommGroup H
inst✝¹ : SeparatedSpace H
inst✝ : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom (Completion G) H
hg : ∀ (v : G), ↑f v = ↑g (↑G v)
⊢ extension f = g
ext v
no goals
case H
G : Type u_1
inst✝³ : SeminormedAddCommGroup G
H : Type u_2
inst✝² : SeminormedAddCommGroup H
inst✝¹ : SeparatedSpace H
inst✝ : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom (Completion G) H
hg : ∀ (v : G), ↑f v = ↑g (↑G v)
v : Completion G
⊢ ↑(extension f) v = ↑g v
rw [NormedAddGroupHom.extension_coe_to_fun,
  Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]