awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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 : ℕ
⊢ ∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i ≤ l
have hm : 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ
⊢ id n ≤ 2 * n
have dsimp : n ≤ 2 * n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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
have 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)
Tactic: refine antitone_nat_of_succ_le (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ
⊢ 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)
have 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
Tactic: rw [show 2 * (n + 1) = 2 * n + 1 + 1 by ring, sum_range_succ, sum_range_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ
⊢ ∑ 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
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ
⊢ ∑ 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)
have bc : f (2 * n + 2) ≤ f (2 * n + 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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 : ℕ
⊢ l ≤ ∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i
have ha : 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ
⊢ id n ≤ 2 * n + 1
have dsimp : n ≤ 2 * n + 1
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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 : ℕ
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
    f n
have 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))
Tactic: obtain h := hfs.tendsto_alternating_series_tsum
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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))
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
    f n
have 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)
Tactic: have upper := hfa.alternating_series_le_tendsto h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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)
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
    f n
have 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)
Tactic: have lower := hfa.tendsto_le_alternating_series h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ
⊢ 0 ≤ f n
have apply : ∀ᶠ (c : ℕ) in atTop, f c ≤ f n
Tactic: apply le_of_tendsto hfs.tendsto_atTop_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ
⊢ ∀ᶠ (c : ℕ) in atTop, f c ≤ f n
have h₁ : ∀ (a : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ | x ∈ Set.Ici n → Membership.mem (γ := Set ℕ) {x : ℕ | (fun (c : ℕ) ↦ f c ≤ f n) x} x} a
Tactic: filter_upwards [Ici_mem_atTop n] with m hm using hfa hm
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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
⊢ ∀ᶠ (c : ℕ) in atTop, f c ≤ f n
have h₂ : ∀ a ∈ Set.Ici n, f a ≤ f n
Tactic: filter_upwards [Ici_mem_atTop n] with m hm using hfa hm
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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)
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
    f n
have 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
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
    f n
have 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
Tactic: obtain (h | h) := even_or_odd n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
    f n
have 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
Tactic: obtain (h | h) := even_or_odd n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range n, HPow.hPow (α := E) (-1) i * f i)| ≤
    f n
have 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)
Tactic: obtain ⟨n, rfl⟩ := even_iff_exists_two_mul.mp h
Cleared hypotheses: n, h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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)
⊢ |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)
have 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)
Tactic: specialize upper n
Cleared hypotheses: upper
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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)
⊢ |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)
have 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)
Tactic: specialize lower n
Cleared hypotheses: lower
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
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)
⊢ |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)
have lower₁ : ∑' (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
Cleared hypotheses: lower
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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)
⊢ |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)
have 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)
Tactic: rw [abs_sub_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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)
⊢ 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 : ℕ), 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)
have 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)
Tactic: constructor