awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n * z ^ n‖ ≤ C * (‖z‖ / ‖w‖) ^ n
have rw : ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n
Tactic: rw [norm_mul, norm_pow, div_pow, ← mul_comm_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
| ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
have enter : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
Tactic: enter [n]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n_1 n : ℕ
| ‖f n * w ^ n‖ ≤ C
have rw : ‖f n‖ ≤ C / ‖w‖ ^ n
Tactic: rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
| ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
have enter : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
Tactic: enter [n]; rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n * w ^ n‖ ≤ C
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n
have conv : ∀ (hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n) (n : ℕ), ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n
Tactic: conv at hC => enter [n]; rw [norm_mul, norm_pow, ← _root_.le_div_iff₀ (by positivity)]
Cleared hypotheses: hC, n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedDivisionRing α
inst_1 : CompleteSpace α
f : ℕ → α
w z : α
h : CauchySeq.{u_1, 0} (α := α) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i * w ^ i
hz : ‖z‖ < ‖w‖
hw : 0 < ‖w‖
C : ℝ
hC : ∀ (n : ℕ), ‖f n‖ ≤ C / ‖w‖ ^ n
n : ℕ
⊢ ‖f n‖ * ‖z‖ ^ n ≤ C / ‖w‖ ^ n * ‖z‖ ^ n
have hbc : ‖f n‖ ≤ C / ‖w‖ ^ n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i • z i
have rw : CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), f i • z i
Tactic: rw [← cauchySeq_shift 1]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (n + 1), f i • z i
have simp_rw : CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
  HSMul.hSMul (β := E) (f n) (∑ i ∈ Finset.range n.succ, z i) +
    -∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
Tactic: simp_rw [Finset.sum_range_by_parts _ _ (Nat.succ _), sub_eq_add_neg, Nat.succ_sub_succ_eq_sub,
    tsub_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    HSMul.hSMul (β := E) (f n) (∑ i ∈ Finset.range n.succ, z i) +
      -∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
have apply : CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
  -∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
Tactic: apply (NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0
    ⟨b, eventually_map.mpr <| Eventually.of_forall fun n ↦ hgb <| n + 1⟩).cauchySeq.add
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    -∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
have refine : CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
  ∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
Tactic: refine CauchySeq.neg ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    ∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
have refine_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, b * |f (i + 1) - f i|
Tactic: refine cauchySeq_range_of_norm_bounded ?_
    (fun n ↦ ?_ : ∀ n, ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
refine_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, b * |f (i + 1) - f i|
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦
    ∑ x ∈ Finset.range n, HSMul.hSMul (β := E) (f (x + 1) + -f x) (∑ i ∈ Finset.range (x + 1), z i)
have refine_2 : ∀ (n : ℕ), ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|
Tactic: refine cauchySeq_range_of_norm_bounded ?_
    (fun n ↦ ?_ : ∀ n, ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, b * |f (i + 1) - f i|
have refine_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ b * ∑ i ∈ Finset.range n, (f i.succ - f i)
Tactic: simp_rw [abs_of_nonneg (sub_nonneg_of_le (hfa (Nat.le_succ _))), ← mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ b * ∑ i ∈ Finset.range n, (f i.succ - f i)
have refine_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (f i.succ - f i)
Tactic: apply Real.uniformContinuous_const_mul.comp_cauchySeq
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (f i.succ - f i)
have refine_1 : CauchySeq (α := ℝ) fun (n : ℕ) ↦ f n + -f 0
Tactic: simp_rw [sum_range_sub, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
hgb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
n : ℕ
⊢ ‖(f (n + 1) + -f n) • (Finset.range (n + 1)).sum z‖ ≤ b * |f (n + 1) - f n|
have refine_2 : ‖(Finset.range (n + 1)).sum z‖ * ‖f (n + 1) + -f n‖ ≤ b * |f (n + 1) - f n|
Tactic: rw [norm_smul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i • z i
have hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
Tactic: have hfa' : Monotone fun n ↦ -f n := fun _ _ hab ↦ neg_le_neg <| hfa hab
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ -f n) atTop (𝓝 0)
have h : Eq (α := ℝ) 0 (-0)
Tactic: convert! hf0.neg
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i • z i
have hf0' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ -f n) atTop (𝓝 0)
Tactic: have hf0' : Tendsto (fun n ↦ -f n) atTop (𝓝 0) := by
    convert! hf0.neg
    simp
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℕ → ℝ
z : ℕ → E
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
hzb : ∀ (n : ℕ), norm.{u_4} (E := E) (∑ i ∈ Finset.range n, z i) ≤ b
hfa' : Monotone (β := ℝ) fun (n : ℕ) ↦ -f n
hf0' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ -f n) atTop (𝓝 0)
⊢ CauchySeq.{u_4, 0} (α := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i • z i
have h : ∀ (x : ℕ), Eq.{u_4 + 1} (α := E) (∑ i ∈ Finset.range x, f i • z i) ((-fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, -f i • z i) x)
Tactic: convert! (hfa'.cauchySeq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
n : ℕ
⊢ norm (E := ℝ) (∑ i ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) i) ≤ 1
have rw : norm (E := ℝ) (if Even n then 0 else 1) ≤ 1
Tactic: rw [neg_one_geom_sum]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
n : ℕ
⊢ norm (E := ℝ) (if Even n then 0 else 1) ≤ 1
have pos : Even n → norm (E := ℝ) 0 ≤ 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
n : ℕ
pos : Even n → norm (E := ℝ) 0 ≤ 1
⊢ norm (E := ℝ) (if Even n then 0 else 1) ≤ 1
have neg : ¬Even n → norm (E := ℝ) 1 ≤ 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
f : ℕ → ℝ
hfa : Monotone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) i * f i
have simp_rw : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, f x * HPow.hPow (α := ℝ) (-1) x
Tactic: simp_rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
f : ℕ → ℝ
hfa : Antitone f
hf0 : Tendsto f atTop (𝓝 0)
⊢ CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, HPow.hPow (α := ℝ) (-1) i * f i
have simp_rw : CauchySeq (α := ℝ) fun (n : ℕ) ↦ ∑ x ∈ Finset.range n, f x * HPow.hPow (α := ℝ) (-1) x
Tactic: simp_rw [mul_comm]
-- 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)
hfm : Monotone f
k : ℕ
⊢ Antitone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
have 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)
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)
hfm : Monotone f
k 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)
have 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
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)
hfm : Monotone f
k n : ℕ
⊢ ∑ 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
have 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)
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]
-- 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)
hfm : Monotone f
k n : ℕ
⊢ ∑ 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)
have bc : f (2 * n) ≤ 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)
hfm : Monotone f
k : ℕ
⊢ l ≤ ∑ i ∈ Finset.range (2 * k), HPow.hPow (α := E) (-1) i * f i
have ha : 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)
-- 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)
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 : ℕ
⊢ 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)
hfm : Monotone f
k : ℕ
⊢ Monotone.{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), HPow.hPow (α := E) (-1) i * f i)
    (∑ i ∈ Finset.range (2 * (n + 1) + 1), HPow.hPow (α := E) (-1) i * f i)
Tactic: refine monotone_nat_of_le_succ (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)
hfm : Monotone f
k 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)
have 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)
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)]
-- 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)
hfm : Monotone f
k n : ℕ
⊢ ∑ 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)
have 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)
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]
-- 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)
hfm : Monotone f
k n : ℕ
⊢ ∑ 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)
have bc : f (2 * n + 1) ≤ f (2 * n + 1 + 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)
hfm : Monotone f
k : ℕ
⊢ ∑ i ∈ Finset.range (2 * k + 1), HPow.hPow (α := E) (-1) i * f i ≤ l
have hm : 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)
-- 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)
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 : ℕ
⊢ id n ≤ 2 * n + 1
have dsimp : n ≤ 2 * n + 1
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 : ℕ
⊢ Monotone.{0, u_4} (β := E) fun (n : ℕ) ↦ ∑ i ∈ Finset.range (2 * n), HPow.hPow (α := E) (-1) i * f i
have 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)
Tactic: refine monotone_nat_of_le_succ (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), HPow.hPow (α := E) (-1) i * f i)
    (∑ i ∈ Finset.range (2 * (n + 1)), HPow.hPow (α := E) (-1) i * f i)
have 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)
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 : ℕ
⊢ ∑ 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)
have 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)
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]
-- 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 : ℕ
⊢ ∑ 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)
have bc : f (2 * n + 1) ≤ f (2 * n)
Tactic: gcongr