awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a : ℕ
hn : 1 ≤ ‖f (a + 1)‖ / ‖f a‖
hc : ‖f a‖ = 0
hn₁ : LE.le (α := ℝ) 1 0
⊢ ‖f a‖ = 0

Tactic:
rw [hc, _root_.div_zero] at hn

Premises used: div_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
a : ℕ
hn : LE.le (α := ℝ) 1 0
hc : ‖f a‖ = 0
linarith : -1 + HSub.hSub (α := ℝ) 1 0 = 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0

Tactic:
have key : ∀ᶠ n in atTop, ‖f n‖ ≠ 0 := by
    filter_upwards [h.eventually_const_le hl] with _ hn hc
    rw [hc, _root_.div_zero] at hn
    linarith
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
rcases : ∀ (r : ℝ) (hr₀ : 1 < r) (hr₁ : r < l), ¬Summable f
⊢ ¬Summable f

Tactic:
rcases exists_between hl with ⟨r, hr₀, hr₁⟩

Premises used: exists_between
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
⊢ ¬Summable f

Tactic:
not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently ?_

Premises used: Filter.Eventually.frequently, not_summable_of_ratio_norm_eventually_ge
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
refine : ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖
⊢ ¬Summable f

Tactic:
refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently ?_

Premises used: Filter.Eventually.frequently, not_summable_of_ratio_norm_eventually_ge
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
a : ℕ
h₁ : r ≤ ‖f (a + 1)‖ / ‖f a‖ → ‖f a‖ ≠ 0 → r * ‖f a‖ ≤ ‖f (a + 1)‖
⊢ r ≤ ‖f (a + 1)‖ / ‖f a‖ → ‖f a‖ ≠ 0 → r * ‖f a‖ ≤ ‖f (a + 1)‖

Tactic:
_
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
h₁ : ∀ (a : ℕ), r ≤ ‖f (a + 1)‖ / ‖f a‖ → ∀ (h₁ : ‖f a‖ ≠ 0), r * ‖f a‖ ≤ ‖f (a + 1)‖
⊢ ∀ᶠ (n : ℕ) in atTop, r * ‖f n‖ ≤ ‖f (n + 1)‖

Tactic:
filter_upwards [h.eventually_const_le hr₁, key] with _ _ h₁

Premises used: Filter.Tendsto.eventually_const_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_4
inst : SeminormedAddCommGroup α
f : ℕ → α
l : ℝ
hl : 1 < l
h : Tendsto (fun (n : ℕ) ↦ ‖f (n + 1)‖ / ‖f n‖) atTop (𝓝 l)
key : ∀ᶠ (n : ℕ) in atTop, ‖f n‖ ≠ 0
r : ℝ
hr₀ : 1 < r
hr₁ : r < l
a : ℕ
h_1 : r ≤ ‖f (a + 1)‖ / ‖f a‖
h₁ : ‖f a‖ ≠ 0
h₂ h₃ h₄ h₅ : r ≤ ‖f (a + 1)‖ / ‖f a‖
⊢ r * ‖f a‖ ≤ ‖f (a + 1)‖

Tactic:
rwa [← le_div_iff₀ (lt_of_le_of_ne (norm_nonneg _) h₁.symm)]

Premises used: Ne.symm, le_div_iff₀, norm_nonneg, lt_of_le_of_ne
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
⊢ 0 < ‖w‖

Tactic:
have hw : 0 < ‖w‖ := (norm_nonneg z).trans_lt hz
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
obtain : ∀ (C : ℝ) (hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C), Summable.{u_1, 0} (α := α) fun (n : ℕ) ↦ f n * z ^ n
⊢ Summable.{u_1, 0} (α := α) fun (n : ℕ) ↦ f n * z ^ n

Tactic:
obtain ⟨C, hC⟩ := exists_norm_le_of_cauchySeq h

Premises used: exists_norm_le_of_cauchySeq
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
rw : CauchySeq.{u_1, 0} (α := α) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b * z ^ b
⊢ Summable.{u_1, 0} (α := α) fun (n : ℕ) ↦ f n * z ^ n

Tactic:
rw [summable_iff_cauchySeq_finset]

Premises used: summable_iff_cauchySeq_finset
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
⊢ CauchySeq.{u_1, 0} (α := α) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b * z ^ b

Tactic:
cauchySeq_finset_of_geometric_bound (r := ‖z‖ / ‖w‖) (C := C) ((div_lt_one hw).mpr hz)
    (fun n ↦ ?_)

Premises used: Iff.mpr, div_lt_one, cauchySeq_finset_of_geometric_bound
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
refine : ∀ (n : ℕ), ‖f n * z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n
⊢ CauchySeq.{u_1, 0} (α := α) fun (s : Finset ℕ) ↦ ∑ b ∈ s, f b * z ^ b

Tactic:
refine cauchySeq_finset_of_geometric_bound (r := ‖z‖ / ‖w‖) (C := C) ((div_lt_one hw).mpr hz)
    (fun n ↦ ?_)

Premises used: Iff.mpr, div_lt_one, cauchySeq_finset_of_geometric_bound
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
rw : ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n
⊢ ‖f n * z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n

Tactic:
rw [norm_mul, norm_pow, div_pow, ← mul_comm_div]

Premises used: norm_pow, norm_mul, mul_comm_div, div_pow
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
enter : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
| ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C

Tactic:
enter [n]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n_1 n : ℕ
⊢ 0 < ‖w‖ ^ n

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n_1 n : ℕ
rw : ‖f n‖ ≤ C / ‖w‖ ^ n
| ‖f n * w ^ n‖ ≤ C

Tactic:
rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]

Premises used: norm_pow, norm_mul, le_div_iff₀
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
enter : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
| ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C

Tactic:
enter [n]; rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]

Premises used: norm_pow, norm_mul, le_div_iff₀
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
conv : ∀ (hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n) (n : ℕ), ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n

Tactic:
conv at hC => enter [n]; rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]

Premises used: norm_pow, norm_mul, le_div_iff₀
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
n : ℕ
hbc : ‖f n‖ ≤ C / ‖w‖ ^ n
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
n : ℕ
⊢ ‖f n‖ ≤ C / ‖w‖ ^ n

Tactic:
hC n
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
n : ℕ
⊢ ‖f n‖ ≤ C / ‖w‖ ^ n

Tactic:
exact hC n
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i
hz : ‖z‖ < 1
⊢ CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * HPow.hPow (α := α) 1 i

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i
hz : ‖z‖ < 1
⊢ ‖z‖ < norm.{u_1} (E := α) 1

Tactic:
simp [hz]
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
rw : CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), f i • z i
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i • z i

Tactic:
rw [← cauchySeq_shift 1]

Premises used: cauchySeq_shift, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
simp_rw :
  CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    HSMul.hSMul (β := E) (f n) (∑ i ∈ Finset.range n.succ, z i) +
      -∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), f i • z i

Tactic:
simp_rw [Finset.sum_range_by_parts _ _ (Nat.succ _), sub_eq_add_neg, Nat.succ_sub_succ_eq_sub,
    tsub_zero]

Premises used: sub_eq_add_neg, tsub_zero, Finset.sum_range_by_parts, Nat.succ, Nat.succ_sub_succ_eq_sub
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
apply :
  CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    -∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    HSMul.hSMul (β := E) (f n) (∑ i ∈ Finset.range n.succ, z i) +
      -∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)

Tactic:
apply (NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0
    ⟨b, eventually_map.mpr <| Eventually.of_forall fun n ↦ hgb <| n + 1⟩).cauchySeq.add

Premises used: Iff.mpr, NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded, Filter.Tendsto.cauchySeq, Filter.Eventually.of_forall, CauchySeq.add, Filter.eventually_map, HAdd.hAdd, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    -∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)

Tactic:
CauchySeq.neg ?_

Premises used: CauchySeq.neg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
refine :
  CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    ∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    -∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)

Tactic:
refine CauchySeq.neg ?_

Premises used: CauchySeq.neg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    ∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)

Tactic:
cauchySeq_range_of_norm_bounded ?_
    (fun n ↦ ?_ : ∀ n, ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|)

Premises used: cauchySeq_range_of_norm_bounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
refine_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, b * |f (i + 1) - f i|
refine_2 : ∀ (n : ℕ), ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    ∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)

Tactic:
refine cauchySeq_range_of_norm_bounded ?_
    (fun n ↦ ?_ : ∀ n, ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|)

Premises used: cauchySeq_range_of_norm_bounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
refine_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ b * ∑ i ∈ Finset.range n, (f i.succ - f i)
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, b * |f (i + 1) - f i|

Tactic:
simp_rw [abs_of_nonneg (sub_nonneg_of_le (hfa (Nat.le_succ _))), ← mul_sum]

Premises used: Finset.mul_sum, sub_nonneg_of_le, Nat.le_succ, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
refine_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (f i.succ - f i)
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ b * ∑ i ∈ Finset.range n, (f i.succ - f i)

Tactic:
apply Real.uniformContinuous_const_mul.comp_cauchySeq

Premises used: Real.uniformContinuous_const_mul, UniformContinuous.comp_cauchySeq
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
refine_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ f n + -f 0
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (f i.succ - f i)

Tactic:
simp_rw [sum_range_sub, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Finset.sum_range_sub
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ f n + -f 0

Tactic:
(Tendsto.cauchySeq hf0).add_const

Premises used: Filter.Tendsto.cauchySeq, CauchySeq.add_const
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ f n + -f 0

Tactic:
exact (Tendsto.cauchySeq hf0).add_const

Premises used: Filter.Tendsto.cauchySeq, CauchySeq.add_const
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
n : ℕ
refine_2 : ‖(Finset.range (n + 1)).sum z‖ * ‖f (n + 1) + -f n‖ ≤ b * |f (n + 1) - f n|
⊢ ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|

Tactic:
rw [norm_smul, mul_comm]

Premises used: norm_smul, mul_comm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
n : ℕ
⊢ ‖(Finset.range (n + 1)).sum z‖ * ‖f (n + 1) + -f n‖ ≤ b * |f (n + 1) - f n|

Tactic:
mul_le_mul_of_nonneg_right (hgb _) (abs_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, abs_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
n : ℕ
⊢ ‖(Finset.range (n + 1)).sum z‖ * ‖f (n + 1) + -f n‖ ≤ b * |f (n + 1) - f n|

Tactic:
exact mul_le_mul_of_nonneg_right (hgb _) (abs_nonneg _)

Premises used: mul_le_mul_of_nonneg_right, abs_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ Monotone (β := ℝ) fun (n : ℕ) ↦ -f n

Tactic:
have hfa' : Monotone fun n ↦ -f n := fun _ _ hab ↦ neg_le_neg <| hfa hab
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x) atTop (𝓝 (-0))

Tactic:
hf0.neg

Premises used: Filter.Tendsto.neg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
h : Eq (α := ℝ) 0 (-0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ -f n) atTop (𝓝 0)

Tactic:
convert! hf0.neg

Premises used: Filter.Tendsto.neg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
⊢ Eq (α := ℝ) 0 (-0)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ -f n) atTop (𝓝 0)

Tactic:
have hf0' : Tendsto (fun n ↦ -f n) atTop (𝓝 0) := by
    convert! hf0.neg
    simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
hf0' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ -f n) atTop (𝓝 0)
⊢ CauchySeq.{u_4, 0} (α := E) (β := ℕ) (-fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, -f i • z i)

Tactic:
(hfa'.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg

Premises used: Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded, CauchySeq.neg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
hf0' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ -f n) atTop (𝓝 0)
h :
  ∀ (x : ℕ),
    Eq.{u_4 + 1} (α := E) (∑ i ∈ Finset.range x, f i • z i) ((-fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, -f i • z i) x)
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i • z i

Tactic:
convert! (hfa'.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg

Premises used: Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded, CauchySeq.neg
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
hf0' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ -f n) atTop (𝓝 0)
x : ℕ
⊢ Eq.{u_4 + 1} (α := E) (∑ i ∈ Finset.range x, f i • z i) ((-fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, -f i • z i) x)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
n : ℕ
rw : norm (E := ℝ) (if Even n then 0 else 1) ≤ 1
⊢ norm (E := ℝ) (∑ i ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) i) ≤ 1

Tactic:
rw [neg_one_geom_sum]

Premises used: neg_one_geom_sum
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
n : ℕ
pos : Even n → norm (E := ℝ) 0 ≤ 1
neg : ¬Even n → norm (E := ℝ) 1 ≤ 1
⊢ norm (E := ℝ) (if Even n then 0 else 1) ≤ 1

Tactic:
split_ifs
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
n : ℕ
h : Even n
⊢ norm (E := ℝ) 0 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
n : ℕ
h : ¬Even n
⊢ norm (E := ℝ) 1 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
simp_rw : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, f x * HPow.hPow (α := ℝ) (-1) x
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) i * f i

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm