awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
s : Set β
hfu : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ s, ‖f n x‖ ≤ u n
refine :
  ∀ (ε : ℝ) (εpos : ε > 0),
    ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
refine₁ :
  ∀ (ε : ℝ) (εpos : ε > 0) (this : ∀ᶠ (b : Finset ι) in atTop, ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∀ᶠ (n : Finset ι) in atTop, ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ n, f n x) < ε
refine₂ :
  ∀ (ε : ℝ) (εpos : 0 < ε)
    (this : ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
refine₃ :
  ∀ (ε : ℝ) (εpos : 0 < ε) (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
refine₄ :
  ∀ (hfu : ∃ (v : Set ι), Membership.mem (γ := Filter ι) cofinite v ∧ ∀ y ∈ v, ∀ x ∈ s, ‖f y x‖ ≤ u y) (ε : ℝ)
    (εpos : 0 < ε) (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε),
    ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
⊢ TendstoUniformlyOn.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : ι), f n x) atTop s
have refine₅ : ∀ (ε : ℝ) (εpos : 0 < ε) (t : Finset ι) (ht : ∀ (b : Finset ι), t ⊆ b → ∑' (a : { x : ι // x ∉ b }), u (↑a : ι) < ε)
  (N : Set ι) (hN : Membership.mem (γ := Filter ι) cofinite N) (HN : ∀ y ∈ N, ∀ x ∈ s, ‖f y x‖ ≤ u y),
  ∃ (a : Finset ι), ∀ (b : Finset ι), a ⊆ b → ∀ x ∈ s, dist.{u_3} (α := F) (∑' (n : ι), f n x) (∑ n ∈ b, f n x) < ε
Tactic: classical
  refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
  have := (tendsto_order.1 (tendsto_tsum_compl_atTop_zero u)).2 _ εpos
  simp only [gt_iff_lt,
    eventually_atTop, ge_iff_le, Finset.le_eq_subset] at *
  obtain ⟨t, ht⟩ := this
  rw [eventually_iff_exists_mem] at hfu
  obtain ⟨N, hN, HN⟩ := hfu
  refine ⟨hN.toFinset ∪ t, fun n hn x hx => ?_⟩
  have A : Summable fun n => ‖f n x‖ := by
    apply Summable.add_compl (s := hN.toFinset) Summable.of_finite
    apply Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) _ (hu.subtype _)
    simp only [comp_apply, Subtype.forall, Set.mem_compl_iff, Finset.mem_coe]
    aesop
  rw [dist_eq_norm, ← A.of_norm.sum_add_tsum_subtype_compl n, add_sub_cancel_left]
  apply lt_of_le_of_lt _ (ht n (Finset.union_subset_right hn))
  apply (norm_tsum_le_tsum_norm (A.subtype _)).trans
  apply (A.subtype _).tsum_le_tsum _ (hu.subtype _)
  simp only [comp_apply, Subtype.forall]
  apply fun i hi => HN i ?_ x hx
  have : i ∉ hN.toFinset := fun hg ↦ hi (Finset.union_subset_left hn hg)
  simp_all
Cleared hypotheses: hfu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformly.{u_2, u_3, u_1} (β := F) (fun (t : Finset α) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : α), f n x) atTop
have rw : TendstoUniformlyOn.{u_2, u_3, u_1} (β := F) (fun (t : Finset α) (x : β) ↦ ∑ n ∈ t, f n x)
  (fun (x : β) ↦ ∑' (n : α), f n x) atTop univ
Tactic: rw [← tendstoUniformlyOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformly.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : ι), f n x) atTop
have rw : TendstoUniformlyOn.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
  (fun (x : β) ↦ ∑' (n : ι), f n x) atTop univ
Tactic: rw [← tendstoUniformlyOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
ι : Type u_4
f : ι → β → F
u : ι → ℝ
hu : Summable u
hfu : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn.{u_2, u_3, u_4} (β := F) (fun (t : Finset ι) (x : β) ↦ ∑ n ∈ t, f n x)
    (fun (x : β) ↦ ∑' (n : ι), f n x) atTop univ
have apply : ∀ᶠ (n : ι) in cofinite, ∀ (x : β), Membership.mem (γ := Set β) univ x → ‖f n x‖ ≤ u n
Tactic: apply tendstoUniformlyOn_tsum_of_cofinite_eventually hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑' (n : α), f n x) s
have refine : ∀ (x : Finset α), ContinuousOn.{u_2, u_3} (Y := F) (fun (x_1 : β) ↦ ∑ n ∈ x, f n x_1) s
Tactic: refine (tendstoUniformlyOn_tsum hu hfu).continuousOn (Frequently.of_forall ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
s : Set β
hf : ∀ (i : α), ContinuousOn (f i) s
hu : Summable u
hfu : ∀ (n : α), ∀ x ∈ s, ‖f n x‖ ≤ u n
⊢ ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑' (n : α), f n x) s
have refine : ∀ (x : Finset α), ContinuousOn.{u_2, u_3} (Y := F) (fun (x_1 : β) ↦ ∑ n ∈ x, f n x_1) s
Tactic: classical
    refine (tendstoUniformlyOn_tsum hu hfu).continuousOn (Frequently.of_forall ?_)
    intro t
    exact continuousOn_finsetSum _ fun i _ => hf i
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.FunctionSeries (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : CompleteSpace F
u : α → ℝ
inst_2 : TopologicalSpace β
f : α → β → F
hf : ∀ (i : α), Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (f i)
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ Continuous[inst_2, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (x : β) ↦ ∑' (n : α), f n x
have simp_rw : ∀ (hf : ∀ (i : α), ContinuousOn (f i) univ), ContinuousOn.{u_2, u_3} (Y := F) (fun (x : β) ↦ ∑' (n : α), f n x) univ
Tactic: simp_rw [← continuousOn_univ] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
⊢ Eq (α := NormedAddGroupHom (Completion G) (Completion G)) (completion (id G)) (id (Completion G))
have H : ∀ (x : Completion G),
  Eq (α := Completion G) ((completion (id G) : (a : Completion G) → Completion G) x : Completion G)
    ((id (Completion G) : (a : Completion G) → Completion G) x : Completion G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
x : Completion G
⊢ Eq (α := Completion G) ((completion (id G) : (a : Completion G) → Completion G) x : Completion G)
    ((id (Completion G) : (a : Completion G) → Completion G) x : Completion G)
have H : _root_.id x = (id (Completion G) : (a : Completion G) → Completion G) x
Tactic: rw [NormedAddGroupHom.completion_def, NormedAddGroupHom.coe_id, Completion.map_id]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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
⊢ g.completion.comp f.completion = (g.comp f).completion
have H₁ : ∀ (x : Completion G),
  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: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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)
    ((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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
Goal:
G : Type u_1
inst : SeminormedAddCommGroup G
H : Type u_2
inst_1 : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
⊢ f.completion.comp toCompl = NormedAddGroupHom.comp toCompl f
have 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: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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))
have refine : (↑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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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)
⊢ hatg ∈ closure (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G))
have rw : ∀ (ε : ℝ), 0 < ε → ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
Tactic: rw [SeminormedAddCommGroup.mem_closure_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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 < ε
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
have 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‖ < ε
Tactic: rcases h.exists_pos with ⟨C', C'_pos, hC'⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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'
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
have rcases : ∀ (δ : ℝ) (δ_pos : 0 < δ) (hδ : (1 + C' * ‖f‖) * δ < ε),
  ∃ 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δ⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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‖) * δ < ε
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
have obtain : ∀ (g : G) (hg : ‖hatg - (↑g : Completion G)‖ < δ),
  ∃ 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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)‖ < δ
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
have 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‖ < ε
Tactic: obtain ⟨g' : G, hgg' : f g' = f g, hfg : ‖g'‖ ≤ C' * ‖f g‖⟩ := hC' (f g) (mem_range_self _ g)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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
have rw : Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) (g - g') : H) (0 : H)
Tactic: rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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)
⊢ g - g' ∈ f.ker
have rw₁ : HSub.hSub (α := H) (β := H) ((f : (a : G) → H) g : H) ((f : (a : G) → H) g' : H) = 0
Tactic: rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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
⊢ g - g' ∈ f.ker
have rw₂ : Eq.{u_2 + 1} (α := H) 0 0
Tactic: rw [f.mem_ker, map_sub, sub_eq_zero.mpr hgg'.symm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (hypothesis)
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)
⊢ ∃ b ∈ (↑(NormedAddGroupHom.comp toCompl (incl f.ker)).range : Set (Completion G)), ‖hatg - b‖ < ε
have mem_ker : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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‖ < ε
have 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)‖ <
  ε
Tactic: refine ⟨_, ⟨⟨g - g', mem_ker⟩, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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
⊢ ‖f‖ * ‖hatg - (↑g : Completion G)‖ ≤ ‖f‖ * δ
have ha : 0 ≤ ‖f‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (hypothesis)
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
⊢ ‖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)‖ <
    ε
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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 - g') : Completion G)‖ = ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖
have rw : ‖hatg - HSub.hSub (α := Completion G) (↑g : Completion G) (↑g' : Completion G)‖ =
  ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖
Tactic: rw [Completion.coe_sub, sub_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.HomCompletion (goal)
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)‖
⊢ ‖hatg - (↑(g - g') : Completion G)‖ = ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖
have rw₁ : ‖hatg - HSub.hSub (α := Completion G) (↑g : Completion G) (↑g' : Completion G)‖ =
  ‖hatg - HSub.hSub (α := Completion G) (↑g : Completion G) (↑g' : Completion G)‖
Tactic: rw [Completion.coe_sub, sub_add]