awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
n : α
h : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖

Tactic:
exact h_sum.of_norm_bounded <| by simpa only [norm_norm] using h

Premises used: Summable.of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
⊢ ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖

Tactic:
have h_suma : ∀ᶠ n in 𝓕, Summable (‖f n ·‖) := by
    filter_upwards [h_bound] with n h
    exact h_sum.of_norm_bounded <| by simpa only [norm_norm] using h
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
inr : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
⊢ Tendsto.{u_1, u_3} (β := G) (fun (x : α) ↦ ∑' (k : β), f x k) 𝓕 (𝓝 (∑' (k : β), g k))

Tactic:
rw [Metric.tendsto_nhds]

Premises used: Metric.tendsto_nhds
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
inr : ∀ (S : ℝ) (hS : HasSum bound S), ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
⊢ ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε

Tactic:
let ⟨S, hS⟩ := h_sum
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
⊢ ∀ ε > 0, ∀ᶠ (x : Finset β) in (SummationFilter.unconditional β).filter, dist (∑ b ∈ x, bound b) S < ε

Tactic:
rw [HasSum, Metric.tendsto_nhds] at hS

Premises used: Metric.tendsto_nhds, HasSum, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : ∀ ε > 0, ∀ᶠ (x : Finset β) in (SummationFilter.unconditional β).filter, dist (∑ b ∈ x, bound b) S < ε
⊢ ε / 3 > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : ∀ ε > 0, ∀ᶠ (x : Finset β) in (SummationFilter.unconditional β).filter, dist (∑ b ∈ x, bound b) S < ε
⊢ ∃ (T : Finset β), dist (∑ b ∈ T, bound b) S < ε / 3

Tactic:
exact Eventually.exists <| hS _ (by positivity)

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : ∀ ε > 0, ∀ᶠ (x : Finset β) in (SummationFilter.unconditional β).filter, dist (∑ b ∈ x, bound b) S < ε
⊢ ∃ (T : Finset β), dist (∑ b ∈ T, bound b) S < ε / 3

Tactic:
classical exact Eventually.exists <| hS _ (by positivity)

Premises used: Filter.Eventually.exists
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
inr :
  ∀ (T : Finset β) (hT : dist (∑ b ∈ T, bound b) S < ε / 3),
    ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
⊢ ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε

Tactic:
obtain ⟨T, hT⟩ : ∃ (T : Finset β), dist (∑ b ∈ T, bound b) S < ε / 3 := by
    rw [HasSum, Metric.tendsto_nhds] at hS
    classical exact Eventually.exists <| hS _ (by positivity)

Premises used: Finset
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
⊢ ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) ≤
    norm (E := ℝ) (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β))

Tactic:
Real.le_norm_self _

Premises used: Real.le_norm_self
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
⊢ norm (E := ℝ) (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β)) = ‖S - ∑ b ∈ T, bound b‖

Tactic:
congrArg _ ?_

Premises used: congrArg
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
rwa : ∀ (hT : ‖∑ b ∈ T, bound b - S‖ < ε / 3), ‖S - ∑ b ∈ T, bound b‖ < ε / 3
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hT : ‖S - ∑ b ∈ T, bound b‖ < ε / 3), ‖S - ∑ b ∈ T, bound b‖ < ε / 3
⊢ ‖S - ∑ b ∈ T, bound b‖ < ε / 3

Tactic:
rwa [dist_eq_norm, norm_sub_rev] at hT

Premises used: dist_eq_norm, norm_sub_rev
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
calc : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) = S - ∑ b ∈ T, bound b
⊢ ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3

Tactic:
calc _ ≤ ‖∑' (k : (Tᶜ : Set β)), bound k‖ := Real.le_norm_self _
         _ = ‖S - ∑ b ∈ T, bound b‖           := congrArg _ ?_
         _ < ε / 3                            := by rwa [dist_eq_norm, norm_sub_rev] at hT

Premises used: congrArg, Compl.compl, SetLike.coe, Real.le_norm_self
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
⊢ ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) = S - ∑ b ∈ T, bound b

Tactic:
simpa only [h_sum.sum_add_tsum_compl, eq_sub_iff_add_eq'] using hS.tsum_eq

Premises used: eq_sub_iff_add_eq', Summable.sum_add_tsum_compl, HasSum.tsum_eq
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
⊢ ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3

Tactic:
have h1 : ∑' (k : (Tᶜ : Set β)), bound k < ε / 3 := by
    calc _ ≤ ‖∑' (k : (Tᶜ : Set β)), bound k‖ := Real.le_norm_self _
         _ = ‖S - ∑ b ∈ T, bound b‖           := congrArg _ ?_
         _ < ε / 3                            := by rwa [dist_eq_norm, norm_sub_rev] at hT
    simpa only [h_sum.sum_add_tsum_compl, eq_sub_iff_add_eq'] using hS.tsum_eq
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
⊢ Tendsto (fun (x : α) ↦ ∑ k ∈ T, f x k) 𝓕 (𝓝 (T.sum g))

Tactic:
have h2 : Tendsto (∑ k ∈ T, f · k) 𝓕 (𝓝 (T.sum g)) := tendsto_finsetSum _ (fun i _ ↦ hab i)
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : Tendsto (fun (x : α) ↦ ∑ k ∈ T, f x k) 𝓕 (𝓝 (T.sum g))
⊢ ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε

Tactic:
rw [Metric.tendsto_nhds] at h2

Premises used: Metric.tendsto_nhds
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
⊢ ε / 3 > 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
h :
  ∀ (n : α) (hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3) (h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖)
    (h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k), dist.{u_3} (α := G) (∑' (k : β), f n k) (∑' (k : β), g k) < ε
⊢ ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε

Tactic:
filter_upwards [h2 (ε / 3) (by positivity), h_suma, h_bound] with n hn h_suma h_bound

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ε = ε / 3 + (ε / 3 + ε / 3)

Tactic:
ring
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
h :
  ‖HAdd.hAdd (α := G) (∑ x ∈ T, (f n x - g x)) (∑' (x : (↑(↑T : Set β)ᶜ : Type u_2)), (f n (↑x : β) - g (↑x : β)))‖ <
    ε / 3 + (ε / 3 + ε / 3)
⊢ dist.{u_3} (α := G) (∑' (k : β), f n k) (∑' (k : β), g k) < ε

Tactic:
rw [dist_eq_norm, ← h_suma.of_norm.tsum_sub h_sumg.of_norm,
    ← (h_suma.of_norm.sub h_sumg.of_norm).sum_add_tsum_compl (s := T),
    (by ring : ε = ε / 3 + (ε / 3 + ε / 3))]

Premises used: Summable.sum_add_tsum_compl, dist_eq_norm, Summable.of_norm, Summable.sub, Summable.tsum_sub
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖HAdd.hAdd (α := G) (∑ x ∈ T, (f n x - g x)) (∑' (x : (↑(↑T : Set β)ᶜ : Type u_2)), (f n (↑x : β) - g (↑x : β)))‖ <
    ε / 3 + (ε / 3 + ε / 3)

Tactic:
(norm_add_le _ _).trans_lt (add_lt_add ?_ ?_)

Premises used: norm_add_le, add_lt_add, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
h : norm.{u_3} (E := G) (∑ x ∈ T, (f n x - g x)) < ε / 3
h₁ : norm.{u_3} (E := G) (∑' (x : (↑(↑T : Set β)ᶜ : Type u_2)), (f n (↑x : β) - g (↑x : β))) < ε / 3 + ε / 3
⊢ ‖HAdd.hAdd (α := G) (∑ x ∈ T, (f n x - g x)) (∑' (x : (↑(↑T : Set β)ᶜ : Type u_2)), (f n (↑x : β) - g (↑x : β)))‖ <
    ε / 3 + (ε / 3 + ε / 3)

Tactic:
refine (norm_add_le _ _).trans_lt (add_lt_add ?_ ?_)

Premises used: norm_add_le, add_lt_add, LE.le.trans_lt
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ norm.{u_3} (E := G) (∑ x ∈ T, (f n x - g x)) < ε / 3

Tactic:
simpa only [dist_eq_norm, Finset.sum_sub_distrib] using hn

Premises used: dist_eq_norm, Finset.sum_sub_distrib
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h_1 : Nonempty β
h_2 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
h :
  ‖HSub.hSub (α := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β))
        (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β))‖ <
    ε / 3 + ε / 3
⊢ norm.{u_3} (E := G) (∑' (x : (↑(↑T : Set β)ᶜ : Type u_2)), (f n (↑x : β) - g (↑x : β))) < ε / 3 + ε / 3

Tactic:
rw [(h_suma.subtype _).of_norm.tsum_sub (h_sumg.subtype _).of_norm]

Premises used: Summable.of_norm, Summable.subtype, Summable.tsum_sub
-- Module: Mathlib.Analysis.Normed.Group.Tannery
Goal:
α : Type u_1
β : Type u_2
G : Type u_3
𝓕 : Filter α
inst : NormedAddCommGroup G
inst_1 : CompleteSpace G
f : α → β → G
g : β → G
bound : β → ℝ
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound_1 : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : Nonempty β
h_1 : 𝓕.NeBot
h_g_le : ∀ (k : β), ‖g k‖ ≤ bound k
h_sumg : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
h_suma_1 : ∀ᶠ (n : α) in 𝓕, Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
ε : ℝ
hε : ε > 0
S : ℝ
hS : HasSum bound S
T : Finset β
hT : dist (∑ b ∈ T, bound b) S < ε / 3
h1 : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) < ε / 3
h2 : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
n : α
hn : dist (∑ k ∈ T, f n k) (T.sum g) < ε / 3
h_suma : Summable (α := ℝ) fun (x : β) ↦ ‖f n x‖
h_bound : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ ‖HSub.hSub (α := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β))
        (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β))‖ <
    ε / 3 + ε / 3

Tactic:
(norm_sub_le _ _).trans_lt (add_lt_add ?_ ?_)

Premises used: norm_sub_le, add_lt_add, LE.le.trans_lt