case intro.mk
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type ?u.15971
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : G
h₀ : ↑f g = 0
⊢ ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g, property := h₀ } ∈ ker (completion f)
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type ?u.15971
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
⊢ range (NormedAddGroupHom.comp toCompl (incl (ker f))) ≤ ker (completion f)
rintro _ ⟨⟨g, h₀ : f g = 0⟩, rfl⟩
no goals
case intro.mk
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type ?u.15971
inst✝ : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : G
h₀ : ↑f g = 0
⊢ ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g, property := h₀ } ∈ ker (completion f)
simp [h₀, mem_ker, Completion.coe_zero]