awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
⊢ ∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i ≤ l

Tactic:
exact hm.ge_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; lia) tendsto_id)) _

Premises used: Filter.tendsto_id, Monotone.ge_of_tendsto, Filter.tendsto_atTop_mono, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
⊢ Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i

Tactic:
antitone_nat_of_succ_le (fun n ↦ ?_)

Premises used: antitone_nat_of_succ_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
refine :
  ∀ (n : ℕ),
    LE.le.{u_4} (α := E) (∑ i ∈ Finset.range (2 * (n + 1) + 1), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)
⊢ Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i

Tactic:
refine antitone_nat_of_succ_le (fun n ↦ ?_)

Premises used: antitone_nat_of_succ_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
rw :
  ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
        HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) +
      HPow.hPow (α := E) (-1) (2 * n + 2) * f (2 * n + 2) ≤
    ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i
⊢ LE.le.{u_4} (α := E) (∑ i ∈ Finset.range (2 * (n + 1) + 1), HPow.hPow (α := E) (-1) i * f i)
    (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)

Tactic:
rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
simp_rw :
  ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x + f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x + f (2 * n + 1)
⊢ ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
        HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) +
      HPow.hPow (α := E) (-1) (2 * n + 2) * f (2 * n + 2) ≤
    ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i

Tactic:
simp_rw [_root_.pow_succ', show (-1 : E) ^ (2 * n) = 1 by simp, neg_one_mul, neg_neg, one_mul,
      ← sub_eq_add_neg, sub_add_eq_add_sub, sub_le_iff_le_add]

Premises used: sub_eq_add_neg, neg_one_mul, sub_le_iff_le_add, neg_neg, sub_add_eq_add_sub, pow_succ', one_mul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
bc : f (2 * n + 2) ≤ f (2 * n + 1)
⊢ ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x + f (2 * n + 2) ≤
    ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x + f (2 * n + 1)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ 2 * n + 1 ≤ 2 * n + 2

Tactic:
lia
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ f (2 * n + 2) ≤ f (2 * n + 1)

Tactic:
exact hfa (by lia)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
⊢ Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i

Tactic:
have ha : Antitone (fun n ↦ ∑ i ∈ range (2 * n + 1), (-1) ^ i * f i) := by
    refine antitone_nat_of_succ_le (fun n ↦ ?_)
    rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]
    simp_rw [_root_.pow_succ', show (-1 : E) ^ (2 * n) = 1 by simp, neg_one_mul, neg_neg, one_mul,
      ← sub_eq_add_neg, sub_add_eq_add_sub, sub_le_iff_le_add]
    gcongr
    exact hfa (by lia)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
ha : Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i
n : ℕ
dsimp : n ≤ 2 * n + 1
⊢ id n ≤ 2 * n + 1

Tactic:
dsimp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
ha : Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i
n : ℕ
⊢ n ≤ 2 * n + 1

Tactic:
lia
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_4
inst : Ring E
inst_1 : PartialOrder E
inst_2 : IsOrderedRing E
inst_3 : TopologicalSpace E
inst_4 : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
ha : Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i
⊢ l ≤ ∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i

Tactic:
exact ha.le_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; lia) tendsto_id)) _

Premises used: Filter.tendsto_id, Filter.tendsto_atTop_mono, Antitone.le_of_tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : UniformSpace E
inst_2 : IsUniformAddGroup E
inst_3 : CompleteSpace E
f : ℕ → E
hfs : Summable f
⊢ Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))

Tactic:
Summable.tendsto_sum_tsum_nat hfs.alternating

Premises used: Summable.alternating, Summable.tendsto_sum_tsum_nat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
⊢ Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))

Tactic:
obtain h := hfs.tendsto_alternating_series_tsum

Premises used: Summable.tendsto_alternating_series_tsum
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
h :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
⊢ ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)

Tactic:
have upper := hfa.alternating_series_le_tendsto h
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
h :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
upper :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
⊢ ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i)

Tactic:
have lower := hfa.tendsto_le_alternating_series h
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n_1 : ℕ
h :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
upper :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i)
n : ℕ
apply : ∀ᶠ (c : ℕ) in atTop, f c ≤ f n
⊢ 0 ≤ f n

Tactic:
apply le_of_tendsto hfs.tendsto_atTop_zero

Premises used: Summable.tendsto_atTop_zero, le_of_tendsto
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n_1 : ℕ
h :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
upper :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i)
n m : ℕ
hm : m ∈ Set.Ici n
⊢ f m ≤ f n

Tactic:
hfa hm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n_1 : ℕ
h :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
upper :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i)
n : ℕ
h₁ :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ | x ∈ Set.Ici n → Membership.mem (γ := Set ℕ) {x : ℕ | (fun (c : ℕ) ↦ f c ≤ f n) x} x} a
h₂ h₃ : ∀ (m : ℕ) (hm : m ∈ Set.Ici n), f m ≤ f n
⊢ ∀ᶠ (c : ℕ) in atTop, f c ≤ f n

Tactic:
filter_upwards [Ici_mem_atTop n] with m hm using hfa hm

Premises used: Filter.Ici_mem_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
h :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
upper :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i)
⊢ ∀ (n : ℕ), 0 ≤ f n

Tactic:
have I (n : ℕ) : 0 ≤ f n := by
    apply le_of_tendsto hfs.tendsto_atTop_zero
    filter_upwards [Ici_mem_atTop n] with m hm using hfa hm
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
h :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
upper :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i)
I : ∀ (n : ℕ), 0 ≤ f n
inl :
  ∀ (h : Even n),
    |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
          (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
      f n
inr :
  ∀ (h : Odd n),
    |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
          (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
      f n
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
    f n

Tactic:
obtain (h | h) := even_or_odd n

Premises used: Nat.even_or_odd
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
n : ℕ
h_1 :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
upper :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i)
I : ∀ (n : ℕ), 0 ≤ f n
h : Even n
inl :
  ∀ (n : ℕ) (h : Even (2 * n)),
    |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
          (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)| ≤
      f (2 * n)
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
    f n

Tactic:
obtain ⟨n, rfl⟩ := even_iff_exists_two_mul.mp h

Premises used: Iff.mp, even_iff_exists_two_mul, rfl
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h_1 :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
upper :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i)
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
h : Even (2 * n)
⊢ LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
    (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)

Tactic:
specialize upper n
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h_1 :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
lower :
  ∀ (k : ℕ),
    LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i)
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
h : Even (2 * n)
upper :
  LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
    (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
⊢ LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
    (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)

Tactic:
specialize lower n
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h_1 :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
h : Even (2 * n)
upper :
  LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
    (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  LE.le.{u_5} (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
    (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)
⊢ ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i ≤ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i + f (2 * n)

Tactic:
simp only [sum_range_succ, even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul] at lower

Premises used: one_pow, even_two, Even.neg_pow, Even.mul_right, Finset.sum_range_succ, one_mul
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h_1 :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
h : Even (2 * n)
upper :
  LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
    (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i ≤ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i + f (2 * n)
inl :
  HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i) ≤
      f (2 * n) ∧
    HSub.hSub (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
        (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i) ≤
      f (2 * n)
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)| ≤
    f (2 * n)

Tactic:
rw [abs_sub_le_iff]

Premises used: abs_sub_le_iff
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h_1 :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
h : Even (2 * n)
upper :
  LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
    (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i ≤ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i + f (2 * n)
inl :
  HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n)
inl₁ :
  HSub.hSub (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n)
⊢ HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i) ≤
      f (2 * n) ∧
    HSub.hSub (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
        (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i) ≤
      f (2 * n)

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
E : Type u_5
inst : Ring E
inst_1 : LinearOrder E
inst_2 : IsOrderedRing E
inst_3 : UniformSpace E
inst_4 : IsUniformAddGroup E
inst_5 : CompleteSpace E
inst_6 : OrderClosedTopology E
f : ℕ → E
hfa : Antitone f
hfs : Summable f
h_1 :
  Tendsto.{0, u_5} (β := E) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i) atTop
    (𝓝 (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i))
I : ∀ (n : ℕ), 0 ≤ f n
n : ℕ
h : Even (2 * n)
upper :
  LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
    (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
lower :
  ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i ≤ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i + f (2 * n)
inl :
  ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i ≤ f (2 * n) + ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
inl₁ inl₂ inl₃ inl₄ :
  ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i ≤ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i + f (2 * n)
⊢ HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n)

Tactic:
rwa [sub_le_iff_le_add, add_comm]

Premises used: sub_le_iff_le_add, add_comm