awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∈ 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 ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n)

Tactic:
rw [sub_le_iff_le_add, add_comm]

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

Tactic:
upper.trans (le_add_of_nonneg_right (I (2 * n)))

Premises used: HMul.hMul, le_add_of_nonneg_right, LE.le.trans, OfNat.ofNat
-- 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)
⊢ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i ≤ ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i + f (2 * n)

Tactic:
exact upper.trans (le_add_of_nonneg_right (I (2 * n)))

Premises used: HMul.hMul, le_add_of_nonneg_right, LE.le.trans, OfNat.ofNat
-- 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 : Odd n
inr :
  ∀ (n : ℕ) (h : Odd (2 * n + 1)),
    |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
          (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)| ≤
      f (2 * n + 1)
⊢ |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⟩ := odd_iff_exists_bit1.mp h

Premises used: Iff.mp, odd_iff_exists_bit1, 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 : Odd (2 * n + 1)
⊢ LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * (n + 1)), HPow.hPow (α := E) (-1) i * f i)
    (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)

Tactic:
specialize upper (n + 1)

Premises used: HAdd.hAdd, OfNat.ofNat
-- 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 : Odd (2 * n + 1)
upper :
  LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * (n + 1)), 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 : Odd (2 * n + 1)
upper :
  LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * (n + 1)), 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)
⊢ ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i

Tactic:
rw [Nat.mul_add, Finset.sum_range_succ] at upper

Premises used: Nat.mul_add, Finset.sum_range_succ
-- 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 : Odd (2 * n + 1)
upper :
  LE.le.{u_5} (α := E) (∑ i ∈ Finset.range (2 * (n + 1)), 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)
upper₁ :
  ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑' (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:
rw [Nat.mul_add, Finset.sum_range_succ] at upper

Premises used: Nat.mul_add, Finset.sum_range_succ
-- 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 : Odd (2 * n + 1)
upper :
  ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑' (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)
inr :
  HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i) ≤
      f (2 * n + 1) ∧
    HSub.hSub (α := E) (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)
        (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i) ≤
      f (2 * n + 1)
⊢ |HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)| ≤
    f (2 * n + 1)

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 : Odd (2 * n + 1)
upper :
  ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑' (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)
inr :
  HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n + 1)
inr₁ :
  HSub.hSub (α := E) (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n + 1)
⊢ HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i) ≤
      f (2 * n + 1) ∧
    HSub.hSub (α := E) (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)
        (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i) ≤
      f (2 * n + 1)

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 : Odd (2 * n + 1)
upper :
  ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑' (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)
inr :
  ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i ≤
    ∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i + f (2 * n + 1)
⊢ HSub.hSub (α := E) (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n + 1)

Tactic:
rw [sub_le_iff_le_add, add_comm]

Premises used: sub_le_iff_le_add, add_comm
-- 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 : Odd (2 * n + 1)
upper :
  ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑' (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 + 1), HPow.hPow (α := E) (-1) i * f i + f (2 * n + 1)

Tactic:
lower.trans (le_add_of_nonneg_right (I (2 * n + 1)))

Premises used: HMul.hMul, le_add_of_nonneg_right, HAdd.hAdd, LE.le.trans, OfNat.ofNat
-- 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 : Odd (2 * n + 1)
upper :
  ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑' (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 + 1), HPow.hPow (α := E) (-1) i * f i + f (2 * n + 1)

Tactic:
exact lower.trans (le_add_of_nonneg_right (I (2 * n + 1)))

Premises used: HMul.hMul, le_add_of_nonneg_right, HAdd.hAdd, LE.le.trans, OfNat.ofNat
-- 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 : Odd (2 * n + 1)
upper :
  ∑ x ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) x * f x +
      HPow.hPow (α := E) (-1) (2 * n + 1) * f (2 * n + 1) ≤
    ∑' (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 ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n + 1)

Tactic:
simpa [Finset.sum_range_succ, add_comm, pow_add] using upper

Premises used: pow_add, add_comm, Finset.sum_range_succ
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
x : ℝ
⊢ 1 ≤ HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1

Tactic:
simp
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
x : ℝ
⊢ 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1

Tactic:
have A : (0 : ℝ) < ⌊‖x‖⌋₊ + 1 := zero_lt_one.trans_le (by simp)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
⊢ ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1

Tactic:
have B : ‖x‖ / (⌊‖x‖⌋₊ + 1) < 1 := (div_lt_one A).2 (Nat.lt_floor_add_one _)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
suffices :
  ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ ≤ ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ x ^ n / (↑n ! : ℝ)

Tactic:
suffices ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / (n + 1)!‖ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖ from
    summable_of_ratio_norm_eventually_le B (eventually_atTop.2 ⟨⌊‖x‖⌋₊, this⟩)
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
rw : ‖x * x ^ n / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
rw₁ : ‖x * x ^ n / (↑((n + 1) * n !) : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
rw₂ :
  ‖x * x ^ n / HMul.hMul (α := ℝ) (↑(n + 1) : ℝ) (↑n ! : ℝ)‖ =
    ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
rw₃ : ‖x / (↑(n + 1) : ℝ) * (x ^ n / (↑n ! : ℝ))‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
rw₄ : ‖x / (↑(n + 1) : ℝ)‖ * ‖x ^ n / (↑n ! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
rw₅ :
  ‖x‖ / Norm.norm (E := ℝ) (↑(n + 1) : ℝ) * ‖x ^ n / (↑n ! : ℝ)‖ =
    ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
rw₆ : ‖x‖ / (↑(n + 1) : ℝ) * ‖x ^ n / (↑n ! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
rw₇ rw₈ :
  ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖ =
    ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖

Tactic:
rw [_root_.pow_succ', Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul,
        norm_div, Real.norm_natCast, Nat.cast_succ]

Premises used: Nat.cast_succ, Nat.factorial_succ, Real.norm_natCast, div_mul_div_comm, norm_mul, Nat.cast_mul, norm_div, pow_succ'
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
ha : 0 ≤ ‖x ^ n / (↑n ! : ℝ)‖
hbc : 0 ≤ ‖x‖
hbc₁ : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
⊢ ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖ ≤
    ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
n₁ : ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
n₂ :
  ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖ ≤
    ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ ≤ ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖

Tactic:
calc
    ‖x ^ (n + 1) / (n + 1)!‖ = ‖x‖ / (n + 1) * ‖x ^ n / (n !)‖ := by
      rw [_root_.pow_succ', Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul,
        norm_div, Real.norm_natCast, Nat.cast_succ]
    _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ := by gcongr

Premises used: Norm.norm, HAdd.hAdd, Nat.factorial, Nat.floor, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
obtain : ∀ (c : ℝ) (hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c), Tendsto g l (𝓝 0)
⊢ Tendsto g l (𝓝 0)

Tactic:
obtain ⟨c, hc⟩ := hmul.eventually_le

Premises used: Filter.IsBoundedUnder.eventually_le
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
⊢ Tendsto g l (𝓝 0)

Tactic:
Metric.nhds_basis_closedBall.tendsto_right_iff.mpr fun ε hε0 ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_right_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
refine : ∀ (ε : ℝ) (hε0 : 0 < ε), ∀ᶠ (x : α) in l, Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
⊢ Tendsto g l (𝓝 0)

Tactic:
refine Metric.nhds_basis_closedBall.tendsto_right_iff.mpr fun ε hε0 ↦ ?_

Premises used: Iff.mpr, Filter.HasBasis.tendsto_right_iff, Metric.nhds_basis_closedBall
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
h :
  ∀ (x : α) (hfgc : ‖f x • g x‖ ≤ c) (hεf : c / ε ≤ ‖f x‖) (hf0 : f x ≠ 0),
    Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
⊢ ∀ᶠ (x : α) in l, Membership.mem (γ := Set R) (closedBall 0 ε) (g x)

Tactic:
filter_upwards [hc, hasBasis_cobounded_norm.tendsto_right_iff.mp hf (c / ε) trivial,
    hf.eventually_ne_cobounded 0] with x hfgc hεf hf0

Premises used: trivial, HDiv.hDiv, Filter.hasBasis_cobounded_norm, Iff.mp, Filter.Tendsto.eventually_ne_cobounded, Filter.HasBasis.tendsto_right_iff, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Normed
Goal:
α : Type u_1
R : Type u_4
K : Type u_5
inst : NormedRing K
inst_1 : IsDomain K
inst_2 : NormedAddCommGroup R
inst_3 : Module K R
inst_4 : IsTorsionFree K R
inst_5 : NormSMulClass K R
f : α → K
g : α → R
l : Filter α
hmul : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) l fun (x : α) ↦ ‖f x • g x‖
hf : Tendsto f l (cobounded K)
c : ℝ
hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c
ε : ℝ
hε0 : 0 < ε
x : α
hfgc : ‖f x • g x‖ ≤ c
hεf : c / ε ≤ ‖f x‖
hf0 : f x ≠ 0
h :
  ∀ (hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ 0) (hfgc : ‖f x • g x‖ ≤ 0) (hεf : 0 / ε ≤ ‖f x‖),
    Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
h₁ : ∀ (hc0 : 0 < c), Membership.mem (γ := Set R) (closedBall 0 ε) (g x)
⊢ Membership.mem (γ := Set R) (closedBall 0 ε) (g x)

Tactic:
rcases eq_or_lt_of_le ((norm_nonneg _).trans hfgc) with rfl | hc0

Premises used: eq_or_lt_of_le, LE.le.trans, norm_nonneg, rfl