awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i ≤ f (2 * n) + ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
Tactic: rwa [sub_le_iff_le_add, add_comm]
-- 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 ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i)
      (∑' (i : ℕ), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n)
have inl : ∑ 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]
-- 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 : 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
have 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)
Tactic: obtain ⟨n, rfl⟩ := odd_iff_exists_bit1.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 : 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)
have 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)
Tactic: specialize upper (n + 1)
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 : 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)
⊢ |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)
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 : 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)
⊢ |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)
have 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
Tactic: rw [Nat.mul_add, Finset.sum_range_succ] at upper
Cleared hypotheses: upper, 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 : 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 : ℕ), HPow.hPow (α := E) (-1) i * f i)
        (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i)| ≤
    f (2 * n + 1)
have 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)
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 : 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 : ℕ), 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)
have 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)
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 : 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 : ℕ), 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)
have 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)
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 : 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 : ℕ), HPow.hPow (α := E) (-1) i * f i)
      (∑ i ∈ Finset.range (2 * n + 1), HPow.hPow (α := E) (-1) i * f i) ≤
    f (2 * n + 1)
have 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)
Tactic: rw [sub_le_iff_le_add, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
x : ℝ
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ x ^ n / (↑n ! : ℝ)
have A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
Tactic: have A : (0 : ℝ) < ⌊‖x‖⌋₊ + 1 := zero_lt_one.trans_le (by simp)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ x ^ n / (↑n ! : ℝ)
have B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
Tactic: have B : ‖x‖ / (⌊‖x‖⌋₊ + 1) < 1 := (div_lt_one A).2 (Nat.lt_floor_add_one _)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ x ^ n / (↑n ! : ℝ)
have suffices : ∀ n ≥ ⌊‖x‖⌋₊, ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ ≤ ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 * ‖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⟩)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have rw : ‖x * x ^ n / (↑(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]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have rw₁ : ‖x * x ^ n / (↑((n + 1) * n !) : ℝ)‖ = ‖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]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have rw₂ : ‖x * x ^ n / HMul.hMul (α := ℝ) (↑(n + 1) : ℝ) (↑n ! : ℝ)‖ = ‖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]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have rw₃ : ‖x / (↑(n + 1) : ℝ) * (x ^ n / (↑n ! : ℝ))‖ = ‖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]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have rw₄ : ‖x / (↑(n + 1) : ℝ)‖ * ‖x ^ n / (↑n ! : ℝ)‖ = ‖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]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have rw₅ : ‖x‖ / Norm.norm (E := ℝ) (↑(n + 1) : ℝ) * ‖x ^ n / (↑n ! : ℝ)‖ =
  ‖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]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have rw₆ : ‖x‖ / (↑(n + 1) : ℝ) * ‖x ^ n / (↑n ! : ℝ)‖ = ‖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]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have rw₇ : ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖ = ‖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]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖ ≤
    ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have ha : 0 ≤ ‖x ^ n / (↑n ! : ℝ)‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
ha : 0 ≤ ‖x ^ n / (↑n ! : ℝ)‖
⊢ ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖ ≤
    ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have hbc : 0 ≤ ‖x‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
x : ℝ
A : 0 < HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1
B : ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 < 1
n : ℕ
hn : n ≥ ⌊‖x‖⌋₊
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ ≤ ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have n₁ : ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ = ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 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
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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 ! : ℝ)‖
⊢ ‖x ^ (n + 1) / (↑(n + 1)! : ℝ)‖ ≤ ‖x‖ / HAdd.hAdd (α := ℝ) (↑⌊‖x‖⌋₊ : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖
have n₂ : ‖x‖ / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * ‖x ^ n / (↑n ! : ℝ)‖ ≤
  ‖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
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
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)
⊢ Tendsto g l (𝓝 0)
have obtain : ∀ (c : ℝ) (hc : ∀ᶠ (x : α) in l, ‖f x • g x‖ ≤ c), Tendsto g l (𝓝 0)
Tactic: obtain ⟨c, hc⟩ := hmul.eventually_le