awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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 (α := ℝ) (∑ i ∈ range n, g i) (∑ i ∈ range N, g i) < ε

Tactic:
specialize hg n hn
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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) < ε
rw : ∀ (hg : norm (E := ℝ) (∑ k ∈ Ico N n, g k) < ε), norm.{u_3} (E := E) (∑ k ∈ Ico N n, f k) < ε
⊢ dist.{u_3} (α := E) (∑ i ∈ range n, f i) (∑ i ∈ range N, f i) < ε

Tactic:
rw [dist_eq_norm, ← sum_Ico_eq_sub _ hn] at hg ⊢

Premises used: dist_eq_norm, Finset.sum_Ico_eq_sub
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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 : norm (E := ℝ) (∑ k ∈ Ico N n, g k) < ε
⊢ norm.{u_3} (E := E) (∑ k ∈ Ico N n, f k) ≤ ∑ k ∈ Ico N n, ‖f k‖

Tactic:
norm_sum_le _ _

Premises used: norm_sum_le
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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 : norm (E := ℝ) (∑ k ∈ Ico N n, g k) < ε
⊢ LE.le (α := ℝ) (∑ k ∈ Ico N n, ‖f k‖) (∑ k ∈ Ico N n, g k)

Tactic:
sum_le_sum fun x _ => hf x

Premises used: Finset.sum_le_sum
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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 : norm (E := ℝ) (∑ k ∈ Ico N n, g k) < ε
⊢ ∑ k ∈ Ico N n, g k ≤ norm (E := ℝ) (∑ k ∈ Ico N n, g k)

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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 : norm (E := ℝ) (∑ k ∈ Ico N n, g k) < ε
⊢ norm (E := ℝ) (∑ k ∈ Ico N n, g k) < ε

Tactic:
hg
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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 : norm (E := ℝ) (∑ k ∈ Ico N n, g k) < ε
⊢ norm.{u_3} (E := E) (∑ k ∈ Ico N n, f k) < ε

Tactic:
calc
    ‖∑ k ∈ Ico N n, f k‖ ≤ ∑ k ∈ _, ‖f k‖ := norm_sum_le _ _
    _ ≤ ∑ k ∈ _, g k := sum_le_sum fun x _ => hf x
    _ ≤ ‖∑ k ∈ _, g k‖ := le_abs_self _
    _ < ε := hg

Premises used: le_abs_self, Finset.Ico, Finset.sum_le_sum, norm_sum_le
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
hf : Summable (α := ℝ) fun (a : ι) ↦ ‖f a‖
⊢ CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ a ∈ s, f a

Tactic:
cauchySeq_finset_of_norm_bounded hf fun _i => le_rfl

Premises used: le_rfl, cauchySeq_finset_of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
α : Type u_2
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
hf : Summable (α := ℝ) fun (a : ι) ↦ ‖f a‖
s : α → Finset ι
p : Filter α
inst_1 : p.NeBot
hs : Tendsto s p atTop
a : E
ha : Tendsto (fun (b : α) ↦ ∑ i ∈ s b, f i) p (𝓝 a)
⊢ HasSum f a

Tactic:
tendsto_nhds_of_cauchySeq_of_subseq (cauchySeq_finset_of_summable_norm hf) hs ha

Premises used: iInf, cauchySeq_finset_of_summable_norm, tendsto_nhds_of_cauchySeq_of_subseq, Filter.atTop, HasSum
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
E : Type u_3
inst : SeminormedAddCommGroup E
f : ℕ → E
a : E
hf : Summable (α := ℝ) fun (i : ℕ) ↦ ‖f i‖
⊢ HasSum f a ↔ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop (𝓝 a)

Tactic:
⟨fun h => h.tendsto_sum_nat, fun h => hasSum_of_subseq_of_summable hf tendsto_finset_range h⟩

Premises used: HasSum.tendsto_sum_nat, Filter.tendsto_finset_range, Iff.intro, hasSum_of_subseq_of_summable
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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
rw : CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ b ∈ s, f b
⊢ Summable f

Tactic:
rw [summable_iff_cauchySeq_finset]

Premises used: summable_iff_cauchySeq_finset
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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
⊢ CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ b ∈ s, f b

Tactic:
cauchySeq_finset_of_norm_bounded hg h

Premises used: cauchySeq_finset_of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
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
⊢ CauchySeq.{u_3, u_1} (α := E) fun (s : Finset ι) ↦ ∑ b ∈ s, f b

Tactic:
exact cauchySeq_finset_of_norm_bounded hg h

Premises used: cauchySeq_finset_of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ε
b : ℝ≥0∞
hf : HasSum f a
hg : HasSum g b
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
⊢ ‖a‖ₑ ≤ b

Tactic:
le_of_tendsto_of_tendsto' hf.enorm hg fun _s ↦ enorm_sum_le_of_le _ fun i _hi ↦ h i

Premises used: enorm_sum_le_of_le, Filter.Tendsto.enorm, le_of_tendsto_of_tendsto'
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ε
b : ℝ≥0∞
hf : HasSum f a
hg : HasSum g b
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
⊢ ‖a‖ₑ ≤ b

Tactic:
exact le_of_tendsto_of_tendsto' hf.enorm hg fun _s ↦ enorm_sum_le_of_le _ fun i _hi ↦ h i

Premises used: enorm_sum_le_of_le, Filter.Tendsto.enorm, le_of_tendsto_of_tendsto'
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : E
b : ℝ
hf : HasSum f a
hg : HasSum g b
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ ‖a‖ ≤ b

Tactic:
le_of_tendsto_of_tendsto' hf.norm hg fun _s ↦ norm_sum_le_of_le _ fun i _hi ↦ h i

Premises used: Filter.Tendsto.norm, norm_sum_le_of_le, le_of_tendsto_of_tendsto'
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : E
b : ℝ
hf : HasSum f a
hg : HasSum g b
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ ‖a‖ ≤ b

Tactic:
exact le_of_tendsto_of_tendsto' hf.norm hg fun _s ↦ norm_sum_le_of_le _ fun i _hi ↦ h i

Premises used: Filter.Tendsto.norm, norm_sum_le_of_le, le_of_tendsto_of_tendsto'
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
pos : ∀ (hf : Summable f), enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a
neg : ∀ (hf : ¬Summable f), enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a
⊢ enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a

Tactic:
by_cases hf : Summable f

Premises used: Summable, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
hf : Summable f
⊢ enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a

Tactic:
hf.hasSum.enorm_le_of_bounded hg h

Premises used: Summable.hasSum, HasSum.enorm_le_of_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
hf : Summable f
⊢ enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a

Tactic:
exact hf.hasSum.enorm_le_of_bounded hg h

Premises used: Summable.hasSum, HasSum.enorm_le_of_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
f : ι → ε
g : ι → ℝ≥0∞
a : ℝ≥0∞
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ₑ ≤ g i
hf : ¬Summable f
⊢ enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ a

Tactic:
simp [tsum_eq_zero_of_not_summable hf]

Premises used: tsum_eq_zero_of_not_summable
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
ε : Type u_5
inst : TopologicalSpace ε
inst_1 : ESeminormedAddCommMonoid ε
f : ι → ε
⊢ enorm.{u_5} (E := ε) (∑' (i : ι), f i) ≤ ∑' (i : ι), ‖f i‖ₑ

Tactic:
tsum_of_enorm_bounded ENNReal.summable.hasSum fun _i => le_rfl

Premises used: le_rfl, ENNReal.summable, tsum_of_enorm_bounded, Summable.hasSum
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
pos : ∀ (hf : Summable f), norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a
neg : ∀ (hf : ¬Summable f), norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a

Tactic:
by_cases hf : Summable f

Premises used: Summable, SummationFilter.unconditional
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : Summable f
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a

Tactic:
hf.hasSum.norm_le_of_bounded hg h

Premises used: HasSum.norm_le_of_bounded, Summable.hasSum
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : Summable f
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a

Tactic:
exact hf.hasSum.norm_le_of_bounded hg h

Premises used: HasSum.norm_le_of_bounded, Summable.hasSum
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
neg : 0 ≤ a
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a

Tactic:
rw [tsum_eq_zero_of_not_summable hf, norm_zero]

Premises used: norm_zero, tsum_eq_zero_of_not_summable
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a

Tactic:
ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)

Premises used: Finset.sum_nonneg, ge_of_tendsto', LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a

Tactic:
exact ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)

Premises used: Finset.sum_nonneg, ge_of_tendsto', LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ
a : ℝ
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖ ≤ g i
hf : ¬Summable f
⊢ 0 ≤ a

Tactic:
classical exact ge_of_tendsto' hg fun s => sum_nonneg fun i _hi => (norm_nonneg _).trans (h i)

Premises used: Finset.sum_nonneg, ge_of_tendsto', LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
hf : Summable (α := ℝ) fun (i : ι) ↦ ‖f i‖
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ ∑' (i : ι), ‖f i‖

Tactic:
tsum_of_norm_bounded hf.hasSum fun _i => le_rfl

Premises used: le_rfl, Summable.hasSum, tsum_of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum g a
h : ∀ (i : ι), ‖f i‖₊ ≤ g i
simp :
  ∀ (hg : HasSum (fun (a : ι) ↦ (↑(g a) : ℝ)) (↑a : ℝ)) (h : ∀ (i : ι), ‖f i‖ ≤ (↑(g i) : ℝ)),
    norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ (↑a : ℝ)
⊢ nnnorm.{u_3} (E := E) (∑' (i : ι), f i) ≤ a

Tactic:
simp only [← NNReal.coe_le_coe, ← NNReal.hasSum_coe, coe_nnnorm] at *

Premises used: coe_nnnorm, NNReal.hasSum_coe, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum (fun (a : ι) ↦ (↑(g a) : ℝ)) (↑a : ℝ)
h : ∀ (i : ι), ‖f i‖ ≤ (↑(g i) : ℝ)
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ (↑a : ℝ)

Tactic:
tsum_of_norm_bounded hg h

Premises used: tsum_of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
g : ι → ℝ≥0
a : ℝ≥0
hg : HasSum (fun (a : ι) ↦ (↑(g a) : ℝ)) (↑a : ℝ)
h : ∀ (i : ι), ‖f i‖ ≤ (↑(g i) : ℝ)
⊢ norm.{u_3} (E := E) (∑' (i : ι), f i) ≤ (↑a : ℝ)

Tactic:
exact tsum_of_norm_bounded hg h

Premises used: tsum_of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
f : ι → E
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ ‖f i‖₊
⊢ nnnorm.{u_3} (E := E) (∑' (i : ι), f i) ≤ ∑' (i : ι), ‖f i‖₊

Tactic:
tsum_of_nnnorm_bounded hf.hasSum fun _i => le_rfl

Premises used: le_rfl, Summable.hasSum, tsum_of_nnnorm_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ᶠ (i : ι) in cofinite, ‖f i‖ ≤ g i
⊢ Summable f

Tactic:
summable_iff_cauchySeq_finset.2 <| cauchySeq_finset_of_norm_bounded_eventually hg h

Premises used: Iff.mpr, cauchySeq_finset_of_norm_bounded_eventually, summable_iff_cauchySeq_finset
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ℕ → E
g : ℕ → ℝ
hg : Summable g
h : ∀ᶠ (i : ℕ) in atTop, ‖f i‖ ≤ g i
⊢ Summable f

Tactic:
.of_norm_bounded_eventually hg <| Nat.cofinite_eq_atTop ▸ h

Premises used: Eq.rec, Summable.of_norm_bounded_eventually, Nat.cofinite_eq_atTop, Eq.symm
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ι → E
g : ι → ℝ≥0
hg : Summable g
h : ∀ (i : ι), ‖f i‖₊ ≤ g i
⊢ Summable f

Tactic:
.of_norm_bounded (NNReal.summable_coe.2 hg) h

Premises used: NNReal.summable_coe, Iff.mpr, Summable.of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ι → E
hf : Summable (α := ℝ) fun (a : ι) ↦ ‖f a‖
⊢ Summable f

Tactic:
.of_norm_bounded hf fun _i => le_rfl

Premises used: le_rfl, Summable.of_norm_bounded
-- Module: Mathlib.Analysis.Normed.Group.InfiniteSum
Goal:
ι : Type u_1
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : CompleteSpace E
f : ι → E
hf : Summable (α := ℝ≥0) fun (a : ι) ↦ ‖f a‖₊
⊢ Summable f

Tactic:
.of_nnnorm_bounded hf fun _i => le_rfl

Premises used: le_rfl, Summable.of_nnnorm_bounded
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
α : Type u_1
m n : ℤ
simp : |HSub.hSub (α := ℝ) (↑m : ℝ) (↑n : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ)|
⊢ dist m n = norm (E := ℝ) (↑(-m + n) : ℝ)

Tactic:
simp only [dist_eq, norm, cast_add, cast_neg]

Premises used: Int.cast_neg, Norm.norm, Int.cast_add, Int.dist_eq
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
α : Type u_1
m n : ℤ
rw : |HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ)|
rw₁ rw₂ : |HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)| = |HSub.hSub (α := ℝ) (↑n : ℝ) (↑m : ℝ)|
⊢ |HSub.hSub (α := ℝ) (↑m : ℝ) (↑n : ℝ)| = |HAdd.hAdd (α := ℝ) (-(↑m : ℝ)) (↑n : ℝ)|

Tactic:
rw [abs_sub_comm, neg_add_eq_sub]

Premises used: neg_add_eq_sub, abs_sub_comm
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
m : ℤ
⊢ norm (E := ℝ) (↑m : ℝ) = ‖m‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
n : ℤ
⊢ ‖n‖ = |(↑n : ℝ)|

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
n : ℕ
⊢ norm (E := ℤ) (↑n : ℤ) = (↑n : ℝ)

Tactic:
simp [Int.norm_eq_abs]

Premises used: Int.norm_eq_abs
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
n : ℤ
⊢ (↑(↑n.natAbs : ℝ≥0) : ℝ) = (↑(↑n.natAbs : ℤ) : ℝ)

Tactic:
simp only [Int.cast_natCast, NNReal.coe_natCast]

Premises used: Int.cast_natCast, NNReal.coe_natCast
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
n : ℤ
⊢ Eq (α := ℝ) (↑(↑n.natAbs : ℤ) : ℝ) |(↑n : ℝ)|

Tactic:
simp only [Int.natCast_natAbs, Int.cast_abs]

Premises used: Int.cast_abs, Int.natCast_natAbs
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
z : ℤ
c : ℝ≥0
rw : LE.le (α := ℤ) (↑z.natAbs : ℤ) (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c
rw₁ : z.natAbs ≤ ⌊c⌋₊ ↔ ‖z‖₊ ≤ c
rw₂ : (↑z.natAbs : ℝ≥0) ≤ c ↔ ‖z‖₊ ≤ c
rw₃ rw₄ : ‖z‖₊ ≤ c ↔ ‖z‖₊ ≤ c
⊢ |z| ≤ (↑⌊c⌋₊ : ℤ) ↔ ‖z‖₊ ≤ c

Tactic:
rw [Int.abs_eq_natAbs, Int.ofNat_le, Nat.le_floor_iff zero_le, NNReal.natCast_natAbs z]

Premises used: zero_le, NNReal.natCast_natAbs, Nat.le_floor_iff, Int.ofNat_le, Int.abs_eq_natAbs
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
α : Type u_1
inst : SeminormedCommGroup α
n : ℤ
a : α
inl : ∀ (n : ℕ), ‖HPow.hPow (β := ℤ) a (↑n : ℤ)‖ ≤ norm (E := ℤ) (↑n : ℤ) * ‖a‖
inr : ∀ (n : ℕ), ‖HPow.hPow (β := ℤ) a (-(↑n : ℤ))‖ ≤ norm (E := ℤ) (-(↑n : ℤ)) * ‖a‖
⊢ ‖a ^ n‖ ≤ ‖n‖ * ‖a‖

Tactic:
rcases n.eq_nat_or_neg with ⟨n, rfl | rfl⟩

Premises used: Int.eq_nat_or_neg, rfl
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
α : Type u_1
inst : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖HPow.hPow (β := ℤ) a (↑n : ℤ)‖ ≤ norm (E := ℤ) (↑n : ℤ) * ‖a‖

Tactic:
simpa [Int.norm_natCast] using norm_pow_le_mul_norm

Premises used: norm_pow_le_mul_norm, Int.norm_natCast
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
α : Type u_1
inst : SeminormedCommGroup α
a : α
n : ℕ
⊢ ‖HPow.hPow (β := ℤ) a (-(↑n : ℤ))‖ ≤ norm (E := ℤ) (-(↑n : ℤ)) * ‖a‖

Tactic:
simpa [Int.norm_natCast] using norm_pow_le_mul_norm

Premises used: norm_pow_le_mul_norm, Int.norm_natCast
-- Module: Mathlib.Analysis.Normed.Group.Int
Goal:
α : Type u_1
inst : SeminormedCommGroup α
n : ℤ
a : α
⊢ ‖a ^ n‖₊ ≤ ‖n‖₊ * ‖a‖₊

Tactic:
simpa only [← NNReal.coe_le_coe, NNReal.coe_mul] using norm_zpow_le_mul_norm n a

Premises used: NNReal.coe_mul, norm_zpow_le_mul_norm, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.Normed.Group.Lemmas
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
x₀ : E
ε : ℝ≥0
ε_pos : 0 < ε
⊢ (fun (x : E) ↦ ‖id x - x₀‖₊) x₀ < ε

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Group.Lemmas
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
x₀ : E
ε : ℝ
ε_pos : 0 < ε
⊢ (fun (x : E) ↦ ‖id x - x₀‖) x₀ < ε

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
apply : ‖x * y‖ ≤ 0
⊢ Membership.mem (γ := Set M) {x : M | ‖x‖ = 0} (x * y)

Tactic:
apply le_antisymm _ (norm_nonneg' _)

Premises used: norm_nonneg', le_antisymm
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ ‖x * y‖ ≤ 0

Tactic:
(norm_mul_le' x y).trans_eq ?_

Premises used: LE.le.trans_eq, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
refine : ‖x‖ + ‖y‖ = 0
⊢ ‖x * y‖ ≤ 0

Tactic:
refine (norm_mul_le' x y).trans_eq ?_

Premises used: LE.le.trans_eq, norm_mul_le'
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
rw : 0 + ‖y‖ = 0
rw₁ : HAdd.hAdd (α := ℝ) 0 0 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ ‖x‖ + ‖y‖ = 0

Tactic:
rw [hx, hy, add_zero]

Premises used: add_zero
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x : M
hx : ‖x‖ = 0
⊢ Membership.mem (γ := Set M) {x : M | ‖x‖ = 0} x⁻¹

Tactic:
simpa only [Set.mem_setOf_eq, norm_inv'] using hx

Premises used: Set.mem_setOf_eq, norm_inv'
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
⊢ IsClosed (↑(nullSubgroup M) : Set M)

Tactic:
apply isClosed_singleton.preimage continuous_norm'

Premises used: continuous_norm', IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
x : M
⊢ Membership.mem (γ := Subgroup M) (nullSubgroup M) x ↔ ‖x‖ = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
apply : ‖c • x‖ ≤ 0
⊢ c • x ∈ AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (nullAddSubgroup E)))

Tactic:
apply le_antisymm _ (norm_nonneg _)

Premises used: le_antisymm, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
⊢ ‖c • x‖ ≤ 0

Tactic:
(norm_smul_le _ _).trans_eq ?_

Premises used: norm_smul_le, LE.le.trans_eq
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
refine : ‖c‖ * ‖x‖ = 0
⊢ ‖c • x‖ ≤ 0

Tactic:
refine (norm_smul_le _ _).trans_eq ?_

Premises used: norm_smul_le, LE.le.trans_eq
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
M : Type u_1
inst : SeminormedCommGroup M
𝕜 : Type u_2
E : Type u_3
inst_1 : SeminormedAddCommGroup E
inst_2 : SeminormedRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : IsBoundedSMul 𝕜 E
c : 𝕜
x : E
hx : ‖x‖ = 0
rw : ‖c‖ * 0 = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ ‖c‖ * ‖x‖ = 0

Tactic:
rw [hx, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
𝕜 : Type u_2
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : SeminormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
⊢ IsClosed (↑(nullSubmodule 𝕜 E) : Set E)

Tactic:
isClosed_nullAddSubgroup

Premises used: isClosed_nullAddSubgroup
-- Module: Mathlib.Analysis.Normed.Group.NullSubmodule
Goal:
𝕜 : Type u_2
E : Type u_3
inst : SeminormedAddCommGroup E
inst_1 : SeminormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
x : E
⊢ Membership.mem (γ := Submodule 𝕜 E) (nullSubmodule 𝕜 E) x ↔ ‖x‖ = 0

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
⊢ ∃ (R : ℝ), ∀ x ∈ s, ‖x‖ ≤ R

Tactic:
hs.exists_norm_le'

Premises used: Bornology.IsBounded.exists_norm_le'
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
obtain : ∀ (Rs : ℝ) (hRs : ∀ x ∈ s, ‖x‖ ≤ Rs), IsBounded (s * t)
⊢ IsBounded (s * t)

Tactic:
obtain ⟨Rs, hRs⟩ : ∃ R, ∀ x ∈ s, ‖x‖ ≤ R := hs.exists_norm_le'

Premises used: Bornology.IsBounded.exists_norm_le'
-- Module: Mathlib.Analysis.Normed.Group.Pointwise
Goal:
E : Type u_1
inst : SeminormedGroup E
s t : Set E
hs : IsBounded s
ht : IsBounded t
Rs : ℝ
hRs : ∀ x ∈ s, ‖x‖ ≤ Rs
⊢ ∃ (R : ℝ), ∀ x ∈ t, ‖x‖ ≤ R

Tactic:
ht.exists_norm_le'

Premises used: Bornology.IsBounded.exists_norm_le'