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
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' * (‖f‖ * δ) < ε

Tactic:
simpa only [add_mul, one_mul, mul_assoc] using hδ

Premises used: add_mul, mul_assoc, one_mul
-- 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‖ * δ
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‖ * δ)
calc₃ : δ + 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)‖ <
    ε

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δ

Premises used: Norm.norm, UniformSpace.Completion.coe', HMul.hMul, HSub.hSub, norm_add_le, add_lt_add_of_lt_of_le, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
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
v : G
⊢ Eq.{u_2 + 1} (α := H) ((f.extension : (a : Completion G) → H) (↑v : Completion G) : H)
    (Completion.extension (⇑f : (a : G) → H) (↑v : Completion G) : H)

Tactic:
rfl

Premises used: UniformSpace.Completion.extension, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
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
v : G
⊢ Eq.{u_2 + 1} (α := H) ((f.extension : (a : Completion G) → H) (↑v : Completion G) : H) ((f : (a : G) → H) v : H)

Tactic:
AddMonoidHom.extension_coe _ f.continuous _

Premises used: AddMonoidHom.extension_coe, UniformSpace.Completion.extension, AbstractCompletion.extend, ite
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
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
⊢ Eq (α := (a : Completion G) → H) (⇑f.extension : (a : Completion G) → H) (Completion.extension (⇑f : (a : G) → H))

Tactic:
rfl

Premises used: UniformSpace.Completion.extension, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
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)
H₁ :
  ∀ (v : Completion G),
    Eq.{u_2 + 1} (α := H) ((f.extension : (a : Completion G) → H) v : H) ((g : (a : Completion G) → H) v : H)
⊢ f.extension = g

Tactic:
ext v
-- Module: Mathlib.Analysis.Normed.Group.HomCompletion
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)
H₂ H₃ : Eq.{u_2 + 1} (α := H) ((g : (a : Completion 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)

Tactic:
rw [NormedAddGroupHom.extension_coe_to_fun,
    Completion.extension_unique f.uniformContinuous g.uniformContinuous fun a => hg a]

Premises used: NormedAddGroupHom.extension_coe_to_fun, NormedAddGroupHom.uniformContinuous, UniformSpace.Completion.extension_unique
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
a : α
⊢ ‖s.indicator f a‖ₑ = s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a

Tactic:
flip congr_fun a (indicator_comp_of_zero (enorm_zero (E := ε))).symm

Premises used: flip, Set.indicator_comp_of_zero, enorm_zero, congr_fun, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s t : Set α
h : s ⊆ t
f : α → ε
a : α
simp : LE.le (α := ENNReal) (s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a) (t.indicator (fun (a : α) ↦ ‖f a‖ₑ) a)
⊢ ‖s.indicator f a‖ₑ ≤ ‖t.indicator f a‖ₑ

Tactic:
simp only [enorm_indicator_eq_indicator_enorm]

Premises used: enorm_indicator_eq_indicator_enorm
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s t : Set α
h : s ⊆ t
f : α → ε
a : α
h₁ : 0 ≤ ‖f a‖ₑ
grw grw₁ : LE.le (α := ENNReal) (t.indicator (fun (a : α) ↦ ‖f a‖ₑ) a) (t.indicator (fun (a : α) ↦ ‖f a‖ₑ) a)
⊢ LE.le (α := ENNReal) (s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a) (t.indicator (fun (a : α) ↦ ‖f a‖ₑ) a)

Tactic:
grw [h]
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
a : α
⊢ s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a ≤ ‖f a‖ₑ

Tactic:
indicator_le_self' (fun _ _ ↦ zero_le) a

Premises used: zero_le, Set.indicator_le_self'
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
a : α
rw : s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a ≤ ‖f a‖ₑ
⊢ ‖s.indicator f a‖ₑ ≤ ‖f a‖ₑ

Tactic:
rw [enorm_indicator_eq_indicator_enorm]

Premises used: enorm_indicator_eq_indicator_enorm
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
ε : Type u_2
inst : TopologicalSpace ε
inst_1 : ESeminormedAddMonoid ε
s : Set α
f : α → ε
a : α
⊢ s.indicator (fun (a : α) ↦ ‖f a‖ₑ) a ≤ ‖f a‖ₑ

Tactic:
apply indicator_enorm_le_enorm_self

Premises used: indicator_enorm_le_enorm_self
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s : Set α
f : α → E
a : α
⊢ ‖s.indicator f a‖ = s.indicator (fun (a : α) ↦ ‖f a‖) a

Tactic:
flip congr_fun a (indicator_comp_of_zero norm_zero).symm

Premises used: norm_zero, flip, Set.indicator_comp_of_zero, congr_fun, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s : Set α
f : α → E
a : α
⊢ ‖s.indicator f a‖₊ = s.indicator (fun (a : α) ↦ ‖f a‖₊) a

Tactic:
flip congr_fun a (indicator_comp_of_zero nnnorm_zero).symm

Premises used: flip, nnnorm_zero, Set.indicator_comp_of_zero, congr_fun, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
simp : LE.le (α := ℝ) (s.indicator (fun (a : α) ↦ ‖f a‖) a) (t.indicator (fun (a : α) ↦ ‖f a‖) a)
⊢ ‖s.indicator f a‖ ≤ ‖t.indicator f a‖

Tactic:
simp only [norm_indicator_eq_indicator_norm]

Premises used: norm_indicator_eq_indicator_norm
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s t : Set α
h : s ⊆ t
f : α → E
a : α
h₁ : 0 ≤ ‖f a‖
grw grw₁ : LE.le (α := ℝ) (t.indicator (fun (a : α) ↦ ‖f a‖) a) (t.indicator (fun (a : α) ↦ ‖f a‖) a)
⊢ LE.le (α := ℝ) (s.indicator (fun (a : α) ↦ ‖f a‖) a) (t.indicator (fun (a : α) ↦ ‖f a‖) a)

Tactic:
grw [h]
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s : Set α
f : α → E
a : α
⊢ s.indicator (fun (a : α) ↦ ‖f a‖) a ≤ ‖f a‖

Tactic:
indicator_le_self' (fun _ _ => norm_nonneg _) a

Premises used: Set.indicator_le_self', norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s : Set α
f : α → E
a : α
rw : s.indicator (fun (a : α) ↦ ‖f a‖) a ≤ ‖f a‖
⊢ ‖s.indicator f a‖ ≤ ‖f a‖

Tactic:
rw [norm_indicator_eq_indicator_norm]

Premises used: norm_indicator_eq_indicator_norm
-- Module: Mathlib.Analysis.Normed.Group.Indicator
Goal:
α : Type u_1
E : Type u_2
inst : SeminormedAddGroup E
s : Set α
f : α → E
a : α
⊢ s.indicator (fun (a : α) ↦ ‖f a‖) a ≤ ‖f a‖

Tactic:
apply indicator_norm_le_norm_self

Premises used: indicator_norm_le_norm_self
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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) < ε
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
⊢ (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) < ε

Tactic:
rw [cauchySeq_finset_iff_sum_vanishing, nhds_basis_ball.forall_iff]

Premises used: Filter.HasBasis.forall_iff, cauchySeq_finset_iff_sum_vanishing, Metric.nhds_basis_ball
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
⊢ (∀ (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:
simp only [ball_zero_eq, Set.mem_setOf_eq]

Premises used: ball_zero_eq, Set.mem_setOf_eq
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
s t : Set E
hst : s ⊆ t
s' : Finset ι
hs' : ∀ (t : Finset ι), Disjoint t s' → ∑ b ∈ t, f b ∈ s
⊢ ∃ (s : Finset ι), ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t

Tactic:
⟨s', fun t' ht' => hst <| hs' _ ht'⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
s t : Set E
hst : s ⊆ t
s' : Finset ι
hs' : ∀ (t : Finset ι), Disjoint t s' → ∑ b ∈ t, f b ∈ s
⊢ ∃ (s : Finset ι), ∀ (t_1 : Finset ι), Disjoint t_1 s → ∑ b ∈ t_1, f b ∈ t

Tactic:
exact ⟨s', fun t' ht' => hst <| hs' _ ht'⟩
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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) < ε
rw₁ 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) < ε
⊢ Summable f ↔ ∀ ε > 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]

Premises used: cauchySeq_finset_iff_vanishing_norm, summable_iff_cauchySeq_finset
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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

Tactic:
cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => ?_

Premises used: Iff.mpr, cauchySeq_finset_iff_vanishing_norm
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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
refine :
  ∀ (ε : ℝ) (hε : ε > 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

Tactic:
refine cauchySeq_finset_iff_vanishing_norm.2 fun ε hε => ?_

Premises used: Iff.mpr, cauchySeq_finset_iff_vanishing_norm
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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
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) < ε
⊢ ∃ (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⟩

Premises used: summable_iff_vanishing_norm, Iff.mp
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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) < ε

Tactic:
⟨s ∪ h.toFinset, fun t ht => ?_⟩

Premises used: Set.Finite.toFinset, Exists.intro, Union.union
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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) < ε

Tactic:
refine ⟨s ∪ h.toFinset, fun t ht => ?_⟩
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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
⊢ ∀ ⦃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

Premises used: Classical.not_not, Set.Finite.mem_toFinset, not_or, Finset.mem_union, Finset.disjoint_left, Set.mem_compl_iff
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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 ι
i : ι
hi : i ∈ t
ht : ∀ ⦃a : ι⦄, a ∈ t → a ∉ s ∧ Membership.mem (γ := Set ι) {x : ι | ‖f x‖ ≤ g x} a
⊢ ‖f i‖ ≤ g i

Tactic:
(ht hi).2

Premises used: Set.Mem, And.right
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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 ι
i : ι
hi : i ∈ t
ht : ∀ ⦃a : ι⦄, a ∈ t → a ∉ s ∧ Membership.mem (γ := Set ι) {x : ι | ‖f x‖ ≤ g x} a
⊢ ‖f i‖ ≤ g i

Tactic:
exact (ht hi).2

Premises used: And.right
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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 ∈ 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
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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)
this : ∀ i ∈ t, ‖f i‖ ≤ g i
⊢ norm.{u_3} (E := E) (∑ i ∈ t, f i) ≤ ∑ i ∈ t, g i

Tactic:
norm_sum_le_of_le _ this

Premises used: norm_sum_le_of_le
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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)
this : ∀ i ∈ t, ‖f i‖ ≤ g i
⊢ ∑ i ∈ t, g i ≤ norm (E := ℝ) (∑ i ∈ t, g i)

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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)
this : ∀ i ∈ t, ‖f i‖ ≤ g i
⊢ norm (E := ℝ) (∑ i ∈ t, g i) < ε

Tactic:
hs _ (ht.mono_right le_sup_left)

Premises used: le_sup_left, Disjoint.mono_right
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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)
this : ∀ i ∈ t, ‖f i‖ ≤ g i
⊢ norm.{u_3} (E := E) (∑ i ∈ t, f i) < ε

Tactic:
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)

Premises used: le_abs_self, le_sup_left, norm_sum_le_of_le, Disjoint.mono_right
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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) < ε
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) < ε
⊢ ∃ (s : Finset ι), ∀ (t : Finset ι), Disjoint t s → 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)

Premises used: le_abs_self
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ i ∈ s, f i

Tactic:
cauchySeq_finset_of_norm_bounded_eventually hg <| Eventually.of_forall h

Premises used: cauchySeq_finset_of_norm_bounded_eventually, Filter.Eventually.of_forall
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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

Tactic:
Metric.cauchySeq_iff'.2 fun ε hε => ?_

Premises used: Iff.mpr, Metric.cauchySeq_iff'
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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
refine : ∀ (ε : ℝ) (hε : ε > 0), ∃ (N : ℕ), ∀ n ≥ N, dist.{u_3} (α := E) (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε
⊢ CauchySeq.{u_3, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ range n, f i

Tactic:
refine Metric.cauchySeq_iff'.2 fun ε hε => ?_

Premises used: Iff.mpr, Metric.cauchySeq_iff'
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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) < ε

Tactic:
(Metric.cauchySeq_iff'.1 hg ε hε).imp fun N hg n hn => ?_

Premises used: Exists.imp, Iff.mp, Metric.cauchySeq_iff'
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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
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) < ε
⊢ ∃ (N : ℕ), ∀ 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 => ?_

Premises used: Exists.imp, Iff.mp, Metric.cauchySeq_iff'