awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (hypothesis)
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 β), dist (∑ b ∈ T, bound b) S < ε / 3
have hS₁ : ∀ ε > 0, ∀ᶠ (x : Finset β) in (SummationFilter.unconditional β).filter, dist (∑ b ∈ x, bound b) S < ε
Tactic: rw [HasSum, Metric.tendsto_nhds] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
⊢ ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
have inr : ∀ (T : Finset β) (hT : dist (∑ b ∈ T, bound b) S < ε / 3),
  ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
⊢ ‖S - ∑ b ∈ T, bound b‖ < ε / 3
have rwa : ∀ (hT : ‖∑ b ∈ T, bound b - S‖ < ε / 3), ‖S - ∑ b ∈ T, bound b‖ < ε / 3
Tactic: rwa [dist_eq_norm, norm_sub_rev] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
⊢ ‖S - ∑ b ∈ T, bound b‖ < ε / 3
have rwa₁ : ∀ (hT : ‖S - ∑ b ∈ T, bound b‖ < ε / 3), ‖S - ∑ b ∈ T, bound b‖ < ε / 3
Tactic: rwa [dist_eq_norm, norm_sub_rev] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
have calc : ∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β) = S - ∑ b ∈ T, bound b
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (hypothesis)
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
⊢ ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
have h1 : ∑' (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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (hypothesis)
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
⊢ ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
have h2 : 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (hypothesis)
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))
⊢ ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
have h2₁ : ∀ ε > 0, ∀ᶠ (x : α) in 𝓕, dist (∑ k ∈ T, f x k) (T.sum g) < ε
Tactic: rw [Metric.tendsto_nhds] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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) < ε
⊢ ∀ᶠ (x : α) in 𝓕, dist.{u_3} (α := G) (∑' (k : β), f x k) (∑' (k : β), g k) < ε
have 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) < ε
Tactic: filter_upwards [h2 (ε / 3) (by positivity), h_suma, h_bound] with n hn h_suma h_bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
⊢ dist.{u_3} (α := G) (∑' (k : β), f n k) (∑' (k : β), g k) < ε
have 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)
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))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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)
have h : norm.{u_3} (E := G) (∑ x ∈ T, (f n x - g x)) < ε / 3
Tactic: refine (norm_add_le _ _).trans_lt (add_lt_add ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
⊢ ‖HAdd.hAdd (α := G) (∑ x ∈ T, (f n x - g x)) (∑' (x : (↑(↑T : Set β)ᶜ : Type u_2)), (f n (↑x : β) - g (↑x : β)))‖ <
    ε / 3 + (ε / 3 + ε / 3)
have h₁ : norm.{u_3} (E := G) (∑' (x : (↑(↑T : Set β)ᶜ : Type u_2)), (f n (↑x : β) - g (↑x : β))) < ε / 3 + ε / 3
Tactic: refine (norm_add_le _ _).trans_lt (add_lt_add ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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 : Set β)ᶜ : Type u_2)), (f n (↑x : β) - g (↑x : β))) < ε / 3 + ε / 3
have h : ‖HSub.hSub (α := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β))
      (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β))‖ <
  ε / 3 + ε / 3
Tactic: rw [(h_suma.subtype _).of_norm.tsum_sub (h_sumg.subtype _).of_norm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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
have h : norm.{u_3} (E := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β)) < ε / 3
Tactic: refine (norm_sub_le _ _).trans_lt (add_lt_add ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β)) < ε / 3
⊢ ‖HSub.hSub (α := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β))
        (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β))‖ <
    ε / 3 + ε / 3
have h₁ : norm.{u_3} (E := G) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β)) < ε / 3
Tactic: refine (norm_sub_le _ _).trans_lt (add_lt_add ?_ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), f n (↑b : β)) < ε / 3
have h : LE.le (α := ℝ) (∑' (i : { x : β // x ∈ (↑T : Set β)ᶜ }), ‖f n (↑i : β)‖)
  (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β))
Tactic: refine ((norm_tsum_le_tsum_norm (h_suma.subtype _)).trans ?_).trans_lt h1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Tannery (goal)
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) (∑' (b : { x : β // x ∈ (↑T : Set β)ᶜ }), g (↑b : β)) < ε / 3
have h : LE.le (α := ℝ) (∑' (i : { x : β // x ∈ (↑T : Set β)ᶜ }), ‖g (↑i : β)‖)
  (∑' (k : (↑(↑T : Set β)ᶜ : Type u_2)), bound (↑k : β))
Tactic: refine ((norm_tsum_le_tsum_norm <| h_sumg.subtype _).trans ?_).trans_lt h1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
⊢ LE.le (α := ℝ) ((fun (x : R) ↦ ‖x‖) (x + y)) (max ((fun (x : R) ↦ ‖x‖) x) ((fun (x : R) ↦ ‖x‖) y))
have h : (fun (x : R) ↦ ‖x‖) (x + y) = dist 0 (x + y)
Tactic: convert! dist_triangle_max 0 x (x + y) using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
h : (fun (x : R) ↦ ‖x‖) (x + y) = dist 0 (x + y)
⊢ LE.le (α := ℝ) ((fun (x : R) ↦ ‖x‖) (x + y)) (max ((fun (x : R) ↦ ‖x‖) x) ((fun (x : R) ↦ ‖x‖) y))
have h₁ : max ((fun (x : R) ↦ ‖x‖) x) ((fun (x : R) ↦ ‖x‖) y) = max (dist 0 x) (dist x (x + y))
Tactic: convert! dist_triangle_max 0 x (x + y) using 1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
⊢ max ((fun (x : R) ↦ ‖x‖) x) ((fun (x : R) ↦ ‖x‖) y) = max (dist 0 x) (dist x (x + y))
have h : (fun (x : R) ↦ ‖x‖) x = dist 0 x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
R : Type u_4
inst : SeminormedAddCommGroup R
inst_1 : IsUltrametricDist R
x y : R
h : (fun (x : R) ↦ ‖x‖) x = dist 0 x
⊢ max ((fun (x : R) ↦ ‖x‖) x) ((fun (x : R) ↦ ‖x‖) y) = max (dist 0 x) (dist x (x + y))
have h₁ : (fun (x : R) ↦ ‖x‖) y = dist x (x + y)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x y : S
h : ‖x‖ ≠ ‖y‖
⊢ ‖x * y‖ = max ‖x‖ ‖y‖
have rw : max (dist x⁻¹ 1) (dist 1 y) = max ‖x⁻¹⁻¹‖ ‖y‖
Tactic: rw [← inv_inv x, ← dist_eq_norm_inv_mul, dist_eq_max_of_dist_ne_dist _ 1 _ (by simp [h])]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
n : ℕ
⊢ ‖x ^ n‖₊ ≤ ‖x‖₊
have zero : ‖HPow.hPow (β := ℕ) x 0‖₊ ≤ ‖x‖₊
Tactic: induction n with
  | zero => simp
  | succ n hn => simpa [pow_add, hn] using nnnorm_mul_le_max (x ^ n) x
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
n : ℕ
zero : ‖HPow.hPow (β := ℕ) x 0‖₊ ≤ ‖x‖₊
⊢ ‖x ^ n‖₊ ≤ ‖x‖₊
have succ : ∀ (n : ℕ) (hn : ‖x ^ n‖₊ ≤ ‖x‖₊), ‖x ^ (n + 1)‖₊ ≤ ‖x‖₊
Tactic: induction n with
  | zero => simp
  | succ n hn => simpa [pow_add, hn] using nnnorm_mul_le_max (x ^ n) x
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
z : ℤ
⊢ ‖x ^ z‖₊ ≤ ‖x‖₊
have ofNat : ∀ (a : ℕ), ‖x ^ Int.ofNat a‖₊ ≤ ‖x‖₊
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
S : Type u_1
inst : SeminormedGroup S
inst_1 : IsUltrametricDist S
x : S
z : ℤ
ofNat : ∀ (a : ℕ), ‖x ^ Int.ofNat a‖₊ ≤ ‖x‖₊
⊢ ‖x ^ z‖₊ ≤ ‖x‖₊
have negSucc : ∀ (a : ℕ), ‖x ^ Int.negSucc a‖₊ ≤ ‖x‖₊
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
x y : S
hx : Membership.mem (γ := Set S) (ball 1 r) x
hy : Membership.mem (γ := Set S) (ball 1 r) y
⊢ Membership.mem (γ := Set S) (ball 1 r) (x * y)
have simp : ∀ (hx : ‖x‖ < r) (hy : ‖y‖ < r), ‖x * y‖ < r
Tactic: simp only [Metric.mem_ball, dist_eq_norm_inv_mul', inv_one, one_mul] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
S : Type u_1
S' : Type u_2
ι : Type u_3
inst : SeminormedGroup S
inst_1 : SeminormedGroup S'
inst_2 : IsUltrametricDist S
r : ℝ
hr : 0 < r
x y : S
hx : Membership.mem (γ := Set S) (closedBall 1 r) x
hy : Membership.mem (γ := Set S) (closedBall 1 r) y
⊢ Membership.mem (γ := Set S) (closedBall 1 r) (x * y)
have simp : ∀ (hx : ‖x‖ ≤ r) (hy : ‖y‖ ≤ r), ‖x * y‖ ≤ r
Tactic: simp only [Metric.mem_closedBall, dist_eq_norm_inv_mul', inv_one, one_mul] at hx hy ⊢
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
hs : s.Nonempty
f : ι → M
⊢ norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ s.sup' hs fun (x : ι) ↦ ‖f x‖
have simp : ∃ b ∈ s, norm.{u_1} (E := M) (∏ i ∈ s, f i) ≤ ‖f b‖
Tactic: simp only [Finset.le_sup'_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs : t.Nonempty
IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖
⊢ ∃ b ∈ Finset.cons j t hj, norm.{u_1} (E := M) (∏ i ∈ Finset.cons j t hj, f i) ≤ ‖f b‖
have cons : ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖ ∨ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖
Tactic: simp only [Finset.prod_cons, Finset.mem_cons, exists_eq_or_imp]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Group.Ultra (goal)
Goal:
M : Type u_1
ι : Type u_2
inst : SeminormedCommGroup M
inst_1 : IsUltrametricDist M
s : Finset ι
f : ι → M
j : ι
t : Finset ι
hj : j ∉ t
hs : t.Nonempty
IH : ∃ b ∈ t, norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f b‖
⊢ ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖ ∨ ∃ a ∈ t, ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f a‖
have cons : norm.{u_1} (E := M) (∏ i ∈ t, f i) ≤ ‖f j‖ → ‖f j * ∏ i ∈ t, f i‖ ≤ ‖f j‖
Tactic: refine (le_total ‖∏ i ∈ t, f i‖ ‖f j‖).imp ?_ ?_