-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem Antitone.alternating_series_le_tendsto
    (hfl : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i * f i) atTop (𝓝 l))
    (hfa : Antitone f) (k : ℕ) : ∑ i ∈ range (2 * k), (-1) ^ i * f i ≤ l

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + (-1) ^ (2 * n + 1) * f (2 * n + 1)

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

Result:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n + 1) ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
⊢ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l

Tactic:
exact hm.ge_of_tendsto (hfl.comp (tendsto_atTop_mono (fun n ↦ by dsimp; omega) tendsto_id)) _

Result:
no goals

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n

Tactic:
omega

Result:
no goals

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
⊢ Monotone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i

Tactic:
refine monotone_nat_of_le_succ (fun n ↦ ?_)

Result:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * (n + 1)), (-1) ^ i * f i

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
⊢ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l

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 omega)

Result:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
⊢ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i ≤ l

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * (n + 1)), (-1) ^ i * f i

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

Result:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i ≤
    ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + (-1) ^ (2 * n + 1) * f (2 * n + 1)

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n + 1) ≤ ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i + f (2 * n)

Tactic:
gcongr

Result:
case bc
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ f (2 * n + 1) ≤ f (2 * n)

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ (-1) ^ (2 * n) = 1

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ 2 * (n + 1) = 2 * n + 1 + 1

Tactic:
ring

Result:
no goals

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ 2 * n ≤ 2 * n + 1

Tactic:
omega

Result:
no goals

Proof state:
case bc
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k n : ℕ
⊢ f (2 * n + 1) ≤ f (2 * n)

Tactic:
exact hfa (by omega)

Result:
no goals

Proof state:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ id n ≤ 2 * n

Tactic:
dsimp

Result:
E : Type u_2
inst✝² : OrderedRing E
inst✝¹ : TopologicalSpace E
inst✝ : OrderClosedTopology E
l : E
f : ℕ → E
hfl : Tendsto (fun n => ∑ i ∈ Finset.range n, (-1) ^ i * f i) atTop (𝓝 l)
hfa : Antitone f
k : ℕ
hm : Monotone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 2 * n