awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Completion G)‖ + norm (E := Completion G) (↑g' : Completion G) = ‖hatg - (↑g : Completion G)‖ + ‖g'‖
have rw : ‖hatg - (↑g : Completion G)‖ + ‖g'‖ = ‖hatg - (↑g : Completion G)‖ + ‖g'‖
Tactic: rw [Completion.norm_coe]
-- 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‖ * δ
⊢ δ + C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ δ + C' * (‖f‖ * δ)
have bc : 0 ≤ C'
Tactic: 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‖ * δ
⊢ ‖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 calc : ‖hatg - (↑(g - g') : Completion G)‖ = ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖
Tactic: 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δ
-- 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‖ * δ
calc : ‖hatg - (↑(g - g') : Completion G)‖ = ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖
⊢ ‖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 calc₁ : ‖hatg - (↑g : Completion G)‖ + norm (E := Completion G) (↑g' : Completion G) = ‖hatg - (↑g : Completion G)‖ + ‖g'‖
Tactic: 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δ
-- 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‖ * δ
calc : ‖hatg - (↑(g - g') : Completion G)‖ = ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖
calc₁ :
  ‖hatg - (↑g : Completion G)‖ + norm (E := Completion G) (↑g' : Completion G) = ‖hatg - (↑g : Completion G)‖ + ‖g'‖
⊢ ‖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 calc₂ : δ + C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ δ + C' * (‖f‖ * δ)
Tactic: 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δ
-- 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‖ * δ
calc : ‖hatg - (↑(g - g') : Completion G)‖ = ‖hatg - (↑g : Completion G) + (↑g' : Completion G)‖
calc₁ :
  ‖hatg - (↑g : Completion G)‖ + norm (E := Completion G) (↑g' : Completion G) = ‖hatg - (↑g : Completion G)‖ + ‖g'‖
calc₂ : δ + C' * norm.{u_2} (E := H) ((f : (a : G) → H) g : H) ≤ δ + C' * (‖f‖ * δ)
⊢ ‖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 calc₃ : δ + C' * (‖f‖ * δ) < ε
Tactic: 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δ
-- 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
inst_2 : T0Space H
inst_3 : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom.{u_1, u_2} (Completion G) H
hg : ∀ (v : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) v : H) ((g : (a : Completion G) → H) (↑v : Completion G) : H)
⊢ f.extension = g
have H₁ : ∀ (v : Completion G),
  Eq.{u_2 + 1} (α := H) ((f.extension : (a : Completion G) → H) v : H) ((g : (a : Completion G) → H) v : H)
Tactic: ext v
-- 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
inst_2 : T0Space H
inst_3 : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom.{u_1, u_2} (Completion G) H
hg : ∀ (v : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) v : H) ((g : (a : Completion G) → H) (↑v : Completion G) : H)
v : Completion G
⊢ Eq.{u_2 + 1} (α := H) ((f.extension : (a : Completion G) → H) v : H) ((g : (a : Completion G) → H) v : H)
have H₁ : Eq.{u_2 + 1} (α := H) (Completion.extension (⇑f : (a : G) → H) v : H) ((g : (a : Completion G) → H) v : H)
Tactic: rw [NormedAddGroupHom.extension_coe_to_fun,
    Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]
-- 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
inst_2 : T0Space H
inst_3 : CompleteSpace H
f : NormedAddGroupHom G H
g : NormedAddGroupHom.{u_1, u_2} (Completion G) H
hg : ∀ (v : G), Eq.{u_2 + 1} (α := H) ((f : (a : G) → H) v : H) ((g : (a : Completion G) → H) (↑v : Completion G) : H)
v : Completion G
H₁ : Eq.{u_2 + 1} (α := H) (Completion.extension (⇑f : (a : G) → H) v : H) ((g : (a : Completion G) → H) v : H)
⊢ Eq.{u_2 + 1} (α := H) ((f.extension : (a : Completion G) → H) v : H) ((g : (a : Completion G) → H) v : H)
have H₂ : Eq.{u_2 + 1} (α := H) ((g : (a : Completion G) → H) v : H) ((g : (a : Completion G) → H) v : H)
Tactic: rw [NormedAddGroupHom.extension_coe_to_fun,
    Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Indicator (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s t : Set α
h : s ⊆ t
f : α → ε
a : α
⊢ ‖s.indicator f a‖ₑ ≤ ‖t.indicator f a‖ₑ
have simp : LE.le (α := ENNReal) (s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a) (t.indicator (fun (a : α) ↦ ‖f a‖ₑ) a)
Tactic: simp only [enorm_indicator_eq_indicator_enorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Indicator (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s t : Set α
h : s ⊆ t
f : α → ε
a : α
⊢ LE.le (α := ENNReal) (s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a) (t.indicator (fun (a : α) ↦ ‖f a‖ₑ) a)
have h₁ : 0 ≤ ‖f a‖ₑ
Tactic: grw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Indicator (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s t : Set α
h : s ⊆ t
f : α → ε
a : α
h₁ : 0 ≤ ‖f a‖ₑ
⊢ LE.le (α := ENNReal) (s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a) (t.indicator (fun (a : α) ↦ ‖f a‖ₑ) a)
have grw : LE.le (α := ENNReal) (t.indicator (fun (a : α) ↦ ‖f a‖ₑ) a) (t.indicator (fun (a : α) ↦ ‖f a‖ₑ) a)
Tactic: grw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Indicator (goal)
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
a : α
⊢ ‖s.indicator f a‖ₑ ≤ ‖f a‖ₑ
have rw : s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a ≤ ‖f a‖ₑ
Tactic: rw [enorm_indicator_eq_indicator_enorm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
⊢ ‖s.indicator f a‖ ≤ ‖t.indicator f a‖
have simp : LE.le (α := ℝ) (s.indicator (fun (a : α) ↦ ‖f a‖) a) (t.indicator (fun (a : α) ↦ ‖f a‖) a)
Tactic: simp only [norm_indicator_eq_indicator_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
⊢ LE.le (α := ℝ) (s.indicator (fun (a : α) ↦ ‖f a‖) a) (t.indicator (fun (a : α) ↦ ‖f a‖) a)
have h₁ : 0 ≤ ‖f a‖
Tactic: grw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
h₁ : 0 ≤ ‖f a‖
⊢ LE.le (α := ℝ) (s.indicator (fun (a : α) ↦ ‖f a‖) a) (t.indicator (fun (a : α) ↦ ‖f a‖) a)
have grw : LE.le (α := ℝ) (t.indicator (fun (a : α) ↦ ‖f a‖) a) (t.indicator (fun (a : α) ↦ ‖f a‖) a)
Tactic: grw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Indicator (goal)
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s : Set α
f : α → E
a : α
⊢ ‖s.indicator f a‖ ≤ ‖f a‖
have rw : s.indicator (fun (a : α) ↦ ‖f a‖) a ≤ ‖f a‖
Tactic: rw [norm_indicator_eq_indicator_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
⊢ (CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ i ∈ s, f i) ↔
    ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
have rw : (∀ (i : ℝ),
    0 < i → ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → Membership.mem (γ := Set E) (ball 0 i) (∑ b ∈ t, f b)) ↔
  ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
Tactic: rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
rw :
  (∀ (i : ℝ),
      0 < i →
        ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → Membership.mem (γ := Set E) (ball 0 i) (∑ b ∈ t, f b)) ↔
    ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
⊢ (CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ i ∈ s, f i) ↔
    ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
have rw₁ : ∀ ⦃s t : Set E⦄,
  s ⊆ t →
    (∃ (s_1 : Finset ι), ∀ (t : Finset ι), Disjoint t s_1 → ∑ b ∈ t, f b ∈ s) →
      ∃ (s : Finset ι), ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t
Tactic: rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ι → E
⊢ Summable f ↔ ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
have rw : (CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ b ∈ s, f b) ↔
  ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
Tactic: rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ι → E
rw :
  (CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ b ∈ s, f b) ↔
    ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
⊢ Summable f ↔ ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
have rw₁ : (∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε) ↔
  ∀ ε > 0, ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
Tactic: rw [summable_iff_cauchySeq_finset, cauchySeq_finset_iff_vanishing_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
⊢ CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ i ∈ s, f i
have refine : ∀ (ε : ℝ) (hε : ε > 0), ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
Tactic: refine cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
have rcases : ∀ (s : Finset ι) (hs : ∀ (t : Finset ι), Disjoint t s → norm (E := ℝ) (∑ i ∈ t, g i) < ε),
  ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
Tactic: rcases summable_iff_vanishing_norm.1 hg ε hε with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → norm (E := ℝ) (∑ i ∈ t, g i) < ε
⊢ ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
have refine : ∀ (t : Finset ι) (ht : Disjoint t (s ∪ Set.Finite.toFinset (s := {x : ι | (fun (i : ι) ↦ ‖f i‖ ≤ g i) x}ᶜ) h)),
  norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
Tactic: refine ⟨s ∪ h.toFinset, fun t ht => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (hypothesis)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → norm (E := ℝ) (∑ i ∈ t, g i) < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset (s := {x : ι | (fun (i : ι) ↦ ‖f i‖ ≤ g i) x}ᶜ) h)
i : ι
hi : i ∈ t
⊢ ‖f i‖ ≤ g i
have ht₁ : ∀ ⦃a : ι⦄, a ∈ t → a ∉ s ∧ Membership.mem (γ := Set ι) {x : ι | ‖f x‖ ≤ g x} a
Tactic: simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
      Classical.not_not] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (hypothesis)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → norm (E := ℝ) (∑ i ∈ t, g i) < ε
t : Finset ι
ht : Disjoint t (s ∪ Set.Finite.toFinset (s := {x : ι | (fun (i : ι) ↦ ‖f i‖ ≤ g i) x}ᶜ) h)
⊢ norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
have this : ∀ i ∈ t, ‖f i‖ ≤ g i
Tactic: have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
    intro i hi
    simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
      Classical.not_not] at ht
    exact (ht hi).2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → norm (E := ℝ) (∑ i ∈ t, g i) < ε
⊢ ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
have refine : ∀ (t : Finset ι) (ht : Disjoint t (s ∪ Set.Finite.toFinset (s := {x : ι | (fun (i : ι) ↦ ‖f i‖ ≤ g i) x}ᶜ) h)),
  norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
Tactic: classical
  refine ⟨s ∪ h.toFinset, fun t ht => ?_⟩
  have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
    intro i hi
    simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
      Classical.not_not] at ht
    exact (ht hi).2
  calc
    ‖∑ i ∈ t, f i‖ ≤ ∑ i ∈ t, g i := norm_sum_le_of_le _ this
    _ ≤ ‖∑ i ∈ t, g i‖ := le_abs_self _
    _ < ε := hs _ (ht.mono_right le_sup_left)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
s : Finset ι
hs : ∀ (t : Finset ι), Disjoint t s → norm (E := ℝ) (∑ i ∈ t, g i) < ε
refine :
  ∀ (t : Finset ι) (ht : Disjoint t (s ∪ Set.Finite.toFinset (s := {x : ι | (fun (i : ι) ↦ ‖f i‖ ≤ g i) x}ᶜ) h)),
    norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
⊢ ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
have refine₁ : ∀ (t : Finset ι) (ht : Disjoint t (s ∪ Set.Finite.toFinset (s := {x : ι | (fun (i : ι) ↦ ‖f i‖ ≤ g i) x}ᶜ) h))
  (this : ∀ i ∈ t, ‖f i‖ ≤ g i), norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε
Tactic: classical
  refine ⟨s ∪ h.toFinset, fun t ht => ?_⟩
  have : ∀ i ∈ t, ‖f i‖ ≤ g i := by
    intro i hi
    simp only [disjoint_left, mem_union, not_or, h.mem_toFinset, Set.mem_compl_iff,
      Classical.not_not] at ht
    exact (ht hi).2
  calc
    ‖∑ i ∈ t, f i‖ ≤ ∑ i ∈ t, g i := norm_sum_le_of_le _ this
    _ ≤ ‖∑ i ∈ t, g i‖ := le_abs_self _
    _ < ε := hs _ (ht.mono_right le_sup_left)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
E : Type u_3
inst : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
⊢ CauchySeq.{u_3, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ range n, f i
have refine : ∀ (ε : ℝ) (hε : ε > 0), ∃ (N : ℕ), ∀ n ≥ N, dist.{u_3} (α := E) (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
Tactic: refine Metric.cauchySeq_iff'.2 fun ε hε => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
E : Type u_3
inst : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, dist.{u_3} (α := E) (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
have refine : ∀ (N : ℕ) (hg : ∀ n ≥ N, dist (α := ℝ) (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε) (n : ℕ) (hn : n ≥ N),
  dist.{u_3} (α := E) (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
Tactic: refine (Metric.cauchySeq_iff'.1 hg ε hε).imp fun N hg n hn => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (hypothesis)
Goal:
E : Type u_3
inst : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N : ℕ
hg : ∀ n ≥ N, dist (α := ℝ) (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε
n : ℕ
hn : n ≥ N
⊢ dist.{u_3} (α := E) (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
have hg₁ : dist (α := ℝ) (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε
Tactic: specialize hg n hn
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
E : Type u_3
inst : SeminormedAddCommGroup E
f : ℕ → E
g : ℕ → ℝ
hg_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ range n, g i
hf : ∀ (i : ℕ), ‖f i‖ ≤ g i
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hg : dist (α := ℝ) (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε
⊢ dist.{u_3} (α := E) (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
have rw : ∀ (hg : norm (E := ℝ) (∑ k ∈ Ico N n, g k) < ε), norm.{u_3} (E := E) (∑ k ∈ Ico N n, f k) < ε
Tactic: rw [dist_eq_norm, ← sum_Ico_eq_sub _ hn] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.InfiniteSum (goal)
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ Summable f
have rw : CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ b ∈ s, f b
Tactic: rw [summable_iff_cauchySeq_finset]