awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
K : Type u_3
inst_2 : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
H₁ :
  Eq.{u_3 + 1} (α := Completion K)
    (Completion.map (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := H) (⇑g : (a : H) → K) (⇑f : (a : G) → H)) x)
    (Completion.map (⇑(g.comp f) : (a : G) → K) x)
⊢ Eq.{u_3 + 1} (α := Completion K)
    ((g.completion.comp f.completion : (a : Completion G) → Completion K) x : Completion K)
    (((g.comp f).completion : (a : Completion G) → Completion K) x : Completion K)

Tactic:
rw [NormedAddGroupHom.coe_comp, NormedAddGroupHom.completion_def,
    NormedAddGroupHom.completion_coe_to_fun, NormedAddGroupHom.completion_coe_to_fun,
    Completion.map_comp g.uniformContinuous f.uniformContinuous]

Premises used: NormedAddGroupHom.completion_def, NormedAddGroupHom.coe_comp, NormedAddGroupHom.uniformContinuous, UniformSpace.Completion.map_comp, NormedAddGroupHom.completion_coe_to_fun
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
K : Type u_3
inst_2 : SeminormedAddCommGroup K
f : NormedAddGroupHom G H
g : NormedAddGroupHom H K
x : Completion G
⊢ Eq.{u_3 + 1} (α := Completion K)
    (Completion.map (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := H) (⇑g : (a : H) → K) (⇑f : (a : G) → H)) x)
    (Completion.map (⇑(g.comp f) : (a : G) → K) x)

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
⊢ (-f).completion = -f.completion

Tactic:
map_neg (normedAddGroupHomCompletionHom : NormedAddGroupHom G H →+ _) f

Premises used: AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.ofLipschitz, NormedAddGroupHom.completion, map_neg, normedAddGroupHomCompletionHom
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f g : NormedAddGroupHom G H
⊢ (f + g).completion = f.completion + g.completion

Tactic:
normedAddGroupHomCompletionHom.map_add f g

Premises used: AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.ofLipschitz, NormedAddGroupHom.completion, normedAddGroupHomCompletionHom, AddMonoidHom.map_add
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f g : NormedAddGroupHom G H
⊢ (f - g).completion = f.completion - g.completion

Tactic:
map_sub (normedAddGroupHomCompletionHom : NormedAddGroupHom G H →+ _) f g

Premises used: map_sub, AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.ofLipschitz, NormedAddGroupHom.completion, normedAddGroupHomCompletionHom
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
⊢ Eq (α := NormedAddGroupHom.{u_1, u_2} (Completion G) (Completion H)) (completion 0) 0

Tactic:
normedAddGroupHomCompletionHom.map_zero

Premises used: AddMonoidHom.map_zero, AddMonoidHom.mkNormedAddGroupHom, NormedAddGroupHom.ofLipschitz, NormedAddGroupHom.completion, normedAddGroupHomCompletionHom
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
K : Type u_3
inst_2 : SeminormedAddCommGroup K
⊢ ∀ (v : G), norm (E := Completion G) (↑v : Completion G) ≤ 1 * ‖v‖

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
x : G
⊢ norm (E := Completion G) ((toCompl : (a : G) → Completion G) x : Completion G) = ‖x‖

Tactic:
Completion.norm_coe x

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.norm_coe, SeparationQuotient.mk
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
⊢ DenseRange.{u_1, u_1} (X := Completion G) (α := G) (⇑toCompl : (a : G) → Completion G)

Tactic:
Completion.isDenseInducing_coe.dense

Premises used: UniformSpace.Completion.coe', IsDenseInducing.dense, SeparationQuotient.mk, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
H₁ :
  ∀ (x : G),
    Eq.{u_2 + 1} (α := Completion H) ((f.completion.comp toCompl : (a : G) → Completion H) x : Completion H)
      ((NormedAddGroupHom.comp toCompl f : (a : G) → Completion H) x : Completion H)
⊢ f.completion.comp toCompl = NormedAddGroupHom.comp toCompl f

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : G
⊢ Eq.{u_2 + 1} (α := Completion H) ((f.completion.comp toCompl : (a : G) → Completion H) x : Completion H)
    ((NormedAddGroupHom.comp toCompl f : (a : G) → Completion H) x : Completion H)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : G
⊢ norm.{u_2} (E := H) ((f : (a : G) → H) x : H) ≤ ‖f.completion‖ * ‖x‖

Tactic:
simpa using f.completion.le_opNorm x

Premises used: UniformSpace.Completion.coe', NormedAddGroupHom.completion, NormedAddGroupHom.le_opNorm
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
g : G
h₀ : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g : H) (0 : H)
⊢ Membership.mem (α := Completion G) f.completion.ker
    (((NormedAddGroupHom.comp toCompl (incl f.ker)).toAddMonoidHom : (a : ↥f.ker) → Completion G)
        (Subtype.mk (p := fun (x : G) ↦ x ∈ f.ker) g h₀) :
      Completion G)

Tactic:
simp [h₀, mem_ker, Completion.coe_zero]

Premises used: NormedAddGroupHom.mem_ker, UniformSpace.Completion.coe_zero
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
⊢ (↑f.completion.ker : Set (Completion G)) =
    closure (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G))

Tactic:
le_antisymm ?_ (closure_minimal f.ker_le_ker_completion f.completion.isClosed_ker)

Premises used: closure_minimal, NormedAddGroupHom.completion, NormedAddGroupHom.isClosed_ker, le_antisymm, NormedAddGroupHom.ker_le_ker_completion
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
refine :
  (↑f.completion.ker : Set (Completion G)) ≤
    closure (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G))
⊢ (↑f.completion.ker : Set (Completion G)) =
    closure (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G))

Tactic:
refine le_antisymm ?_ (closure_minimal f.ker_le_ker_completion f.completion.isClosed_ker)

Premises used: closure_minimal, NormedAddGroupHom.completion, NormedAddGroupHom.isClosed_ker, le_antisymm, NormedAddGroupHom.ker_le_ker_completion
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
rw :
  ∀ (ε : ℝ), 0 < ε → ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
⊢ hatg ∈ closure (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G))

Tactic:
rw [SeminormedAddCommGroup.mem_closure_iff]

Premises used: SeminormedAddCommGroup.mem_closure_iff
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
rcases :
  ∀ (C' : ℝ) (C'_pos : C' > 0) (hC' : f.SurjectiveOnWith f.range C'),
    ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε

Tactic:
rcases h.exists_pos with ⟨C', C'_pos, hC'⟩

Premises used: NormedAddGroupHom.SurjectiveOnWith.exists_pos
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
rcases :
  ∀ (δ : ℝ) (δ_pos : 0 < δ) (hδ : (1 + C' * ‖f‖) * δ < ε),
    ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε

Tactic:
rcases exists_pos_mul_lt ε_pos (1 + C' * ‖f‖) with ⟨δ, δ_pos, hδ⟩

Premises used: Norm.norm, HMul.hMul, HAdd.hAdd, exists_pos_mul_lt, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
obtain :
  ∀ (g : G) (hg : ‖hatg - (↑g : Completion G)‖ < δ),
    ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε

Tactic:
obtain ⟨_, ⟨g : G, rfl⟩, hg : ‖hatg - g‖ < δ⟩ :=
    SeminormedAddCommGroup.mem_closure_iff.mp (Completion.isDenseInducing_coe.dense hatg) δ δ_pos

Premises used: SeminormedAddCommGroup.mem_closure_iff, IsDenseInducing.dense, Iff.mp, rfl, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
obtain :
  ∀ (g' : G) (hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H))
    (hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)),
    ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε

Tactic:
obtain ⟨g' : G, hgg' : f g' = f g, hfg : ‖g'‖ ≤ C' * ‖f g‖⟩ := hC' (f g) (mem_range_self _ g)

Premises used: NormedAddGroupHom.mem_range_self, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
rw : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) (g - g') : H) (0 : H)
rw₁ : HSub.hSub (α := H) (β := H) ((f : (a : G) → H) g : H) ((f : (a : G) → H) g' : H) = 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := H) 0 0
⊢ g - g' ∈ f.ker

Tactic:
rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]

Premises used: Iff.mpr, map_sub, sub_eq_zero, NormedAddGroupHom.mem_ker, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
⊢ g - g' ∈ f.ker

Tactic:
have mem_ker : g - g' ∈ f.ker := by rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε

Tactic:
⟨_, ⟨⟨g - g', mem_ker⟩, rfl⟩, ?_⟩

Premises used: HSub.hSub, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
refine :
  ‖HSub.hSub (β := Completion G) hatg
        (((NormedAddGroupHom.comp toCompl (incl f.ker)).toAddMonoidHom : (a : ↥f.ker) → Completion G)
            (Subtype.mk (p := fun (x : G) ↦ x ∈ f.ker) (g - g') mem_ker) :
          Completion G)‖ <
    ε
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε

Tactic:
refine ⟨_, ⟨⟨g - g', mem_ker⟩, rfl⟩, ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
⊢ norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ ‖f‖ * ‖hatg - (↑g : Completion G)‖

Tactic:
simpa [map_sub, hatg_in] using f.completion.le_opNorm (hatg - g)

Premises used: UniformSpace.Completion.coe', map_sub, HSub.hSub, NormedAddGroupHom.completion, NormedAddGroupHom.le_opNorm
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
ha : 0 ≤ ‖f‖
⊢ ‖f‖ * ‖hatg - (↑g : Completion G)‖ ≤ ‖f‖ * δ

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
⊢ norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ ‖f‖ * δ

Tactic:
have : ‖f g‖ ≤ ‖f‖ * δ := calc
    ‖f g‖ ≤ ‖f‖ * ‖hatg - g‖ := by
      simpa [map_sub, hatg_in] using f.completion.le_opNorm (hatg - g)
    _ ≤ ‖f‖ * δ := by gcongr
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
this : norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ ‖f‖ * δ
rw :
  ‖hatg - HSub.hSub (α := Completion G) (↑g : Completion G) (↑g' : Completion G)‖ =
    ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖
rw₁ rw₂ :
  ‖hatg - HSub.hSub (α := Completion G) (↑g : Completion G) (↑g' : Completion G)‖ =
    ‖hatg - HSub.hSub (α := Completion G) (↑g : Completion G) (↑g' : Completion G)‖
⊢ ‖hatg - (↑(g - g') : Completion G)‖ = ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖

Tactic:
rw [Completion.coe_sub, sub_add]

Premises used: sub_add, UniformSpace.Completion.coe_sub
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
this : norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ ‖f‖ * δ
⊢ ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖ ≤
    ‖hatg - (↑g : Completion G)‖ + norm (E := Completion G) (↑g' : Completion G)

Tactic:
norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
this : norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ ‖f‖ * δ
rw rw₁ : ‖hatg - (↑g : Completion G)‖ + ‖g'‖ = ‖hatg - (↑g : Completion G)‖ + ‖g'‖
⊢ ‖hatg - (↑g : Completion G)‖ + norm (E := Completion G) (↑g' : Completion G) = ‖hatg - (↑g : Completion G)‖ + ‖g'‖

Tactic:
rw [Completion.norm_coe]

Premises used: UniformSpace.Completion.norm_coe
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
this : norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ ‖f‖ * δ
⊢ ‖hatg - (↑g : Completion G)‖ + ‖g'‖ < δ + C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)

Tactic:
add_lt_add_of_lt_of_le hg hfg

Premises used: add_lt_add_of_lt_of_le
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
C : ℝ
h : f.SurjectiveOnWith f.range C
hatg : Completion G
hatg_in :
  Eq.{u_2 + 1} (α := Completion H) ((f.completion : (a : Completion G) → Completion H) hatg : Completion H)
    (0 : Completion H)
ε : ℝ
ε_pos : 0 < ε
C' : ℝ
C'_pos : C' > 0
hC' : f.SurjectiveOnWith f.range C'
δ : ℝ
δ_pos : 0 < δ
hδ : (1 + C' * ‖f‖) * δ < ε
g : G
hg : ‖hatg - (↑g : Completion G)‖ < δ
g' : G
hgg' : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) g' : H) ((f : (a : G) → H) g : H)
hfg : ‖g'‖ ≤ C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H)
mem_ker : g - g' ∈ f.ker
this : norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ ‖f‖ * δ
bc : 0 ≤ C'
⊢ δ + C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ δ + C' * (‖f‖ * δ)

Tactic:
gcongr