-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem Monotone.tendsto_le_alternating_series
    (hfl : Tendsto (fun n ↦ ∑ i ∈ range n, (-1) ^ i * f i) atTop (𝓝 l))
    (hfm : Monotone f) (k : ℕ) : l ≤ ∑ i ∈ range (2 * k), (-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)
hfm : Monotone f
k : ℕ
ha : Antitone 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)
hfm : Monotone f
k : ℕ
ha : Antitone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
⊢ l ≤ ∑ i ∈ Finset.range (2 * k), (-1) ^ i * f i

Tactic:
exact ha.le_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)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n) ≤ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n + 1)

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)
hfm : Monotone f
k n : ℕ
⊢ f (2 * n) ≤ 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)
hfm : Monotone f
k n : ℕ
⊢ 2 * (n + 1) = 2 * n + 1 + 1

Tactic:
ring

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)
hfm : Monotone f
k n : ℕ
⊢ f (2 * n) ≤ f (2 * n + 1)

Tactic:
exact hfm (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)
hfm : Monotone f
k : ℕ
⊢ l ≤ ∑ i ∈ Finset.range (2 * k), (-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 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)
hfm : Monotone f
k : ℕ
ha : Antitone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
⊢ l ≤ ∑ i ∈ Finset.range (2 * k), (-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)
hfm : Monotone f
k : ℕ
⊢ Antitone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i

Tactic:
refine antitone_nat_of_succ_le (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)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * (n + 1)), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-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)
hfm : Monotone f
k n : ℕ
⊢ ∑ i ∈ Finset.range (2 * (n + 1)), (-1) ^ i * f i ≤ ∑ i ∈ Finset.range (2 * n), (-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)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n), (-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)
hfm : Monotone 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)
hfm : Monotone f
k n : ℕ
⊢ 2 * n ≤ 2 * n + 1

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)
hfm : Monotone f
k : ℕ
ha : Antitone 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)
hfm : Monotone f
k : ℕ
ha : Antitone fun n => ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i
n : ℕ
⊢ n ≤ 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)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + (-1) ^ (2 * n) * f (2 * n) + (-1) ^ (2 * n + 1) * f (2 * n + 1) ≤
    ∑ i ∈ Finset.range (2 * n), (-1) ^ i * f i

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]

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)
hfm : Monotone f
k n : ℕ
⊢ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n) ≤ ∑ x ∈ Finset.range (2 * n), (-1) ^ x * f x + f (2 * n + 1)