awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, f x * HPow.hPow (α := ℝ) (-1) x

Tactic:
hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

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

Tactic:
exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

Premises used: norm_sum_neg_one_pow_le, Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ ∃ (l : ℝ), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) i * f i) atTop (𝓝 l)

Tactic:
cauchySeq_tendsto_of_complete <| hfa.cauchySeq_alternating_series_of_tendsto_zero hf0

Premises used: cauchySeq_tendsto_of_complete, Monotone.cauchySeq_alternating_series_of_tendsto_zero
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
hfa : Antitone 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
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, f x * HPow.hPow (α := ℝ) (-1) x

Tactic:
hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

Premises used: norm_sum_neg_one_pow_le, Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, f x * HPow.hPow (α := ℝ) (-1) x

Tactic:
exact hfa.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le

Premises used: norm_sum_neg_one_pow_le, Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ ∃ (l : ℝ), Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) i * f i) atTop (𝓝 l)

Tactic:
cauchySeq_tendsto_of_complete <| hfa.cauchySeq_alternating_series_of_tendsto_zero hf0

Premises used: cauchySeq_tendsto_of_complete, Antitone.cauchySeq_alternating_series_of_tendsto_zero
-- 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)
hfm : Monotone f
k : ℕ
⊢ Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), 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)
hfm : Monotone f
k : ℕ
refine :
  ∀ (n : ℕ),
    LE.le.{u_4} (α := E) (∑ i ∈ Finset.range (2 * (n + 1)), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
⊢ Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), 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)
hfm : Monotone f
k n : ℕ
⊢ 2 * (n + 1) = 2 * n + 1 + 1

Tactic:
ring
-- 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)
hfm : Monotone f
k n : ℕ
rw :
  ∑ x ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) x * f x + HPow.hPow (α := E) (-1) (2 * n) * f (2 * n) +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
⊢ LE.le.{u_4} (α := E) (∑ i ∈ Finset.range (2 * (n + 1)), HPow.hPow (α := E) (-1) i * f i)
    (∑ i ∈ Finset.range (2 * n), 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)
hfm : Monotone f
k n : ℕ
⊢ HPow.hPow (α := E) (-1) (2 * n) = 1

Tactic:
simp
-- 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)
hfm : Monotone f
k n : ℕ
simp_rw :
  ∑ x ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) x * f x + f (2 * n) ≤
    ∑ x ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) x * f x + f (2 * n + 1)
⊢ ∑ x ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) x * f x + HPow.hPow (α := E) (-1) (2 * n) * f (2 * n) +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i

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

Premises used: sub_eq_add_neg, neg_one_mul, sub_le_iff_le_add, 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)
hfm : Monotone f
k n : ℕ
bc : f (2 * n) ≤ f (2 * n + 1)
⊢ ∑ x ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) x * f x + f (2 * n) ≤
    ∑ x ∈ Finset.range (2 * n), 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)
hfm : Monotone f
k n : ℕ
⊢ 2 * 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)
hfm : Monotone f
k n : ℕ
⊢ f (2 * n) ≤ f (2 * n + 1)

Tactic:
exact hfm (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)
hfm : Monotone f
k : ℕ
⊢ Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i

Tactic:
have ha : Antitone (fun n ↦ ∑ i ∈ range (2 * n), (-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, one_mul,
      ← sub_eq_add_neg, sub_le_iff_le_add]
    gcongr
    exact hfm (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)
hfm : Monotone f
k : ℕ
ha : Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
n : ℕ
dsimp : n ≤ 2 * n
⊢ id n ≤ 2 * n

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)
hfm : Monotone f
k : ℕ
ha : Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
n : ℕ
⊢ n ≤ 2 * n

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)
hfm : Monotone f
k : ℕ
ha : Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
⊢ l ≤ ∑ i ∈ Finset.range (2 * k), 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_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)
hfm : Monotone f
k : ℕ
⊢ Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i

Tactic:
monotone_nat_of_le_succ (fun n ↦ ?_)

Premises used: monotone_nat_of_le_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)
hfm : Monotone f
k : ℕ
refine :
  ∀ (n : ℕ),
    LE.le.{u_4} (α := E) (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * (n + 1) + 1), HPow.hPow (α := E) (-1) i * f i)
⊢ Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i

Tactic:
refine monotone_nat_of_le_succ (fun n ↦ ?_)

Premises used: monotone_nat_of_le_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)
hfm : Monotone f
k n : ℕ
rw :
  ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i ≤
    ∑ 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 + 1 + 1) * f (2 * n + 1 + 1)
⊢ LE.le.{u_4} (α := E) (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)
    (∑ i ∈ Finset.range (2 * (n + 1) + 1), HPow.hPow (α := E) (-1) i * f i)

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

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat, 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)
hfm : Monotone f
k n : ℕ
simp_rw :
  ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i + f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i + f (2 * n + 1 + 1)
⊢ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i ≤
    ∑ 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 + 1 + 1) * f (2 * n + 1 + 1)

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, le_sub_iff_add_le]

Premises used: sub_eq_add_neg, neg_one_mul, neg_neg, le_sub_iff_add_le, 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)
hfm : Monotone f
k n : ℕ
bc : f (2 * n + 1) ≤ f (2 * n + 1 + 1)
⊢ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i + f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i + f (2 * n + 1 + 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)
hfm : Monotone f
k n : ℕ
⊢ 2 * n + 1 ≤ 2 * n + 1 + 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)
hfm : Monotone f
k n : ℕ
⊢ f (2 * n + 1) ≤ f (2 * n + 1 + 1)

Tactic:
exact hfm (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)
hfm : Monotone f
k : ℕ
⊢ Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i

Tactic:
have hm : Monotone (fun n ↦ ∑ i ∈ range (2 * n + 1), (-1) ^ i * f i) := by
    refine monotone_nat_of_le_succ (fun n ↦ ?_)
    rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring,
      sum_range_succ _ (2 * n + 1 + 1), sum_range_succ _ (2 * n + 1)]
    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, le_sub_iff_add_le]
    gcongr
    exact hfm (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)
hfm : Monotone f
k : ℕ
hm : Monotone.{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)
hfm : Monotone f
k : ℕ
hm : Monotone.{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)
hfm : Monotone f
k : ℕ
hm : Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i
⊢ ∑ i ∈ Finset.range (2 * k + 1), 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 : ℕ
⊢ Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i

Tactic:
monotone_nat_of_le_succ (fun n ↦ ?_)

Premises used: monotone_nat_of_le_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 : ℕ
refine :
  ∀ (n : ℕ),
    LE.le.{u_4} (α := E) (∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * (n + 1)), HPow.hPow (α := E) (-1) i * f i)
⊢ Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i

Tactic:
refine monotone_nat_of_le_succ (fun n ↦ ?_)

Premises used: monotone_nat_of_le_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 : ℕ
⊢ 2 * (n + 1) = 2 * n + 1 + 1

Tactic:
ring
-- 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 :
  ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i ≤
    ∑ x ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) x * f x + HPow.hPow (α := E) (-1) (2 * n) * f (2 * n) +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1)
⊢ LE.le.{u_4} (α := E) (∑ i ∈ Finset.range (2 * n), 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 : ℕ
⊢ HPow.hPow (α := E) (-1) (2 * n) = 1

Tactic:
simp
-- 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 :
  ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i + f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i + f (2 * n)
⊢ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i ≤
    ∑ x ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) x * f x + HPow.hPow (α := E) (-1) (2 * n) * f (2 * n) +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1)

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

Premises used: sub_eq_add_neg, neg_one_mul, le_sub_iff_add_le, 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 + 1) ≤ f (2 * n)
⊢ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i + f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i + f (2 * n)

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 ≤ 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 n : ℕ
⊢ f (2 * n + 1) ≤ f (2 * n)

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 : ℕ
⊢ Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i

Tactic:
have hm : Monotone (fun n ↦ ∑ i ∈ range (2 * n), (-1) ^ i * f i) := by
    refine monotone_nat_of_le_succ (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, one_mul,
      ← sub_eq_add_neg, le_sub_iff_add_le]
    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 : ℕ
hm : Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
n : ℕ
dsimp : n ≤ 2 * n
⊢ id n ≤ 2 * n

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 : ℕ
hm : Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
n : ℕ
⊢ n ≤ 2 * n

Tactic:
lia