[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
⊢ completion (id G) = id (Completion G)
[PROOFSTEP]
ext x
[GOAL]
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
x : Completion G
⊢ ↑(completion (id G)) x = ↑(id (Completion G)) x
[PROOFSTEP]
rw [NormedAddGroupHom.completion_def, NormedAddGroupHom.coe_id, Completion.map_id]
[GOAL]
case H
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
x : Completion G
⊢ _root_.id x = ↑(id (Completion G)) x
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
ext x
[GOAL]
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
[PROOFSTEP]
rw [NormedAddGroupHom.coe_comp, NormedAddGroupHom.completion_def, NormedAddGroupHom.completion_coe_to_fun,
  NormedAddGroupHom.completion_coe_to_fun, Completion.map_comp g.uniformContinuous f.uniformContinuous]
[GOAL]
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
[PROOFSTEP]
rfl
[GOAL]
G : Type u_1
inst✝² : SeminormedAddCommGroup G
H : Type u_2
inst✝¹ : SeminormedAddCommGroup H
K : Type u_3
inst✝ : SeminormedAddCommGroup K
⊢ ∀ (v : G), ‖↑G v‖ ≤ 1 * ‖v‖
[PROOFSTEP]
simp [le_refl]
[GOAL]
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
⊢ NormedAddGroupHom.comp (completion f) toCompl = NormedAddGroupHom.comp toCompl f
[PROOFSTEP]
ext x
[GOAL]
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
x : G
⊢ ↑(NormedAddGroupHom.comp (completion f) toCompl) x = ↑(NormedAddGroupHom.comp toCompl f) x
[PROOFSTEP]
simp
[GOAL]
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
x : G
⊢ ‖↑f x‖ ≤ ‖completion f‖ * ‖x‖
[PROOFSTEP]
simpa using f.completion.le_opNorm x
[GOAL]
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
⊢ range (NormedAddGroupHom.comp toCompl (incl (ker f))) ≤ ker (completion f)
[PROOFSTEP]
rintro _ ⟨⟨g, h₀ : f g = 0⟩, rfl⟩
[GOAL]
case intro.mk
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 : G
h₀ : ↑f g = 0
⊢ ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g, property := h₀ } ∈ ker (completion f)
[PROOFSTEP]
simp [h₀, mem_ker, Completion.coe_zero]
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
⊢ ↑(ker (completion f)) = closure ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f))))
[PROOFSTEP]
refine le_antisymm ?_ (closure_minimal f.ker_le_ker_completion f.completion.isClosed_ker)
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
⊢ ↑(ker (completion f)) ≤ closure ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f))))
[PROOFSTEP]
rintro hatg (hatg_in : f.completion hatg = 0)
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
⊢ hatg ∈ closure ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f))))
[PROOFSTEP]
rw [SeminormedAddCommGroup.mem_closure_iff]
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
⊢ ∀ (ε : ℝ), 0 < ε → ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
intro ε ε_pos
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
rcases h.exists_pos with ⟨C', C'_pos, hC'⟩
[GOAL]
case intro.intro
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
rcases exists_pos_mul_lt ε_pos (1 + C' * ‖f‖) with ⟨δ, δ_pos, hδ⟩
[GOAL]
case intro.intro.intro.intro
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
obtain ⟨_, ⟨g : G, rfl⟩, hg : ‖hatg - g‖ < δ⟩ :=
  SeminormedAddCommGroup.mem_closure_iff.mp (Completion.denseInducing_coe.dense hatg) δ δ_pos
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
obtain ⟨g' : G, hgg' : f g' = f g, hfg : ‖g'‖ ≤ C' * ‖f g‖⟩ := hC' (f g) (mem_range_self _ g)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
have mem_ker : g - g' ∈ f.ker := by rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
⊢ g - g' ∈ ker f
[PROOFSTEP]
rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ∃ b, b ∈ ↑(range (NormedAddGroupHom.comp toCompl (incl (ker f)))) ∧ ‖hatg - b‖ < ε
[PROOFSTEP]
refine ⟨_, ⟨⟨g - g', mem_ker⟩, rfl⟩, ?_⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ‖hatg - ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g - g', property := mem_ker }‖ < ε
[PROOFSTEP]
have : ‖f g‖ ≤ ‖f‖ * δ
[GOAL]
case this
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ‖↑f g‖ ≤ ‖f‖ * δ
case intro.intro.intro.intro.intro.intro.intro.intro.intro
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g - g', property := mem_ker }‖ < ε
[PROOFSTEP]
calc
  ‖f g‖ ≤ ‖f‖ * ‖hatg - g‖ := by simpa [hatg_in] using f.completion.le_opNorm (hatg - g)
  _ ≤ ‖f‖ * δ := by gcongr
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ‖↑f g‖ ≤ ‖f‖ * ‖hatg - ↑G g‖
[PROOFSTEP]
simpa [hatg_in] using f.completion.le_opNorm (hatg - g)
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
⊢ ‖f‖ * ‖hatg - ↑G g‖ ≤ ‖f‖ * δ
[PROOFSTEP]
gcongr
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - ↑(toAddMonoidHom (NormedAddGroupHom.comp toCompl (incl (ker f)))) { val := g - g', property := mem_ker }‖ < ε
[PROOFSTEP]
calc
  ‖hatg - ↑(g - g')‖ = ‖hatg - g + g'‖ := by rw [Completion.coe_sub, sub_add]
  _ ≤ ‖hatg - g‖ + ‖(g' : Completion G)‖ := (norm_add_le _ _)
  _ = ‖hatg - g‖ + ‖g'‖ := by rw [Completion.norm_coe]
  _ < δ + C' * ‖f g‖ := (add_lt_add_of_lt_of_le hg hfg)
  _ ≤ δ + C' * (‖f‖ * δ) := by gcongr
  _ < ε := by simpa only [add_mul, one_mul, mul_assoc] using hδ
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - ↑G (g - g')‖ = ‖hatg - ↑G g + ↑G g'‖
[PROOFSTEP]
rw [Completion.coe_sub, sub_add]
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ ‖hatg - ↑G g‖ + ‖↑G g'‖ = ‖hatg - ↑G g‖ + ‖g'‖
[PROOFSTEP]
rw [Completion.norm_coe]
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ δ + C' * ‖↑f g‖ ≤ δ + C' * (‖f‖ * δ)
[PROOFSTEP]
gcongr
[GOAL]
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
C : ℝ
h : SurjectiveOnWith f (range f) C
hatg : Completion G
hatg_in : ↑(completion f) hatg = 0
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : SurjectiveOnWith f (range f) C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - ↑G g‖ < δ
g' : G
hgg' : ↑f g' = ↑f g
hfg : ‖g'‖ ≤ C' * ‖↑f g‖
mem_ker : g - g' ∈ ker f
this : ‖↑f g‖ ≤ ‖f‖ * δ
⊢ δ + C' * (‖f‖ * δ) < ε
[PROOFSTEP]
simpa only [add_mul, one_mul, mul_assoc] using hδ
[GOAL]
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
[PROOFSTEP]
ext v
[GOAL]
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
[PROOFSTEP]
rw [NormedAddGroupHom.extension_coe_to_fun,
  Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]
