Аналіз I, Розділ 7.2: Нескінченні ряди

Я (прим. перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним підходом Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підправити", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Основні конструкції та результати цього розділу:

namespace Chapter7open BigOperators

Визначення 7.2.1 (Формальні нескінченні ряди). Це схоже на послідовності з Розділу 6, але ними оперують інакше. Як і в Розділі 5, за замовчуванням початок ряду беремо з 0.

@[ext] structure Series where m : ℤ seq : ℤ → ℝ vanish : ∀ n < m, seq n = 0

Функції з ℕ у ℝ можна розглядати як ряди.

instance Series.instCoe : Coe (ℕ → ℝ) Series where coe := fun a ↦ { m := 0 seq n := if n ≥ 0 then a n.toNat else 0 vanish := a:ℕ → ℝ⊢ ∀ n < 0, (if n ≥ 0 then a n.toNat else 0) = 0 All goals completed! 🐙 }
@[simp] theorem Series.eval_coe (a: ℕ → ℝ) (n: ℕ) : (a: Series).seq n = a n := a:ℕ → ℝn:ℕ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑n = a n All goals completed! 🐙abbrev Series.mk' {m:ℤ} (a: { n // n ≥ m } → ℝ) : Series where m := m seq n := if h : n ≥ m then a ⟨n, h⟩ else 0 vanish := m:ℤa:{ n // n ≥ m } → ℝ⊢ ∀ n < m, (if h : n ≥ m then a ⟨n, h⟩ else 0) = 0 All goals completed! 🐙theorem Series.eval_mk' {m:ℤ} (a : { n // n ≥ m } → ℝ) {n : ℤ} (h:n ≥ m) : (Series.mk' a).seq n = a ⟨ n, h ⟩ := m:ℤa:{ n // n ≥ m } → ℝn:ℤh:n ≥ m⊢ (mk' a).seq n = a ⟨n, h⟩ All goals completed! 🐙

Визначення 7.2.2 (Збігання рядів)

abbrev Series.partial (s : Series) (N:ℤ) : ℝ := ∑ n ∈ Finset.Icc s.m N, s.seq n
theorem Series.partial_succ (s : Series) {N:ℤ} (h: N ≥ s.m-1) : s.partial (N+1) = s.partial N + s.seq (N+1) := s:SeriesN:ℤh:N ≥ s.m - 1⊢ s.partial (N + 1) = s.partial N + s.seq (N + 1) s:SeriesN:ℤh:N ≥ s.m - 1⊢ ∑ n ∈ Finset.Icc s.m (N + 1), s.seq n = ∑ n ∈ Finset.Icc s.m N, s.seq n + s.seq (N + 1) s:SeriesN:ℤh:N ≥ s.m - 1⊢ ∑ n ∈ Finset.Icc s.m (N + 1), s.seq n = s.seq (N + 1) + s.partial N convert Finset.sum_insert (show N+1 ∉ Finset.Icc s.m N s:SeriesN:ℤh:N ≥ s.m - 1⊢ s.partial (N + 1) = s.partial N + s.seq (N + 1) All goals completed! 🐙) s:SeriesN:ℤh:N ≥ s.m - 1⊢ insert (N + 1) (Finset.Icc s.m N) = Finset.Icc s.m (N + 1); s:SeriesN:ℤh:N ≥ s.m - 1⊢ s.m ≤ N + 1; All goals completed! 🐙theorem Series.partial_of_lt {s : Series} {N:ℤ} (h: N < s.m) : s.partial N = 0 := s:SeriesN:ℤh:N < s.m⊢ s.partial N = 0 s:SeriesN:ℤh:N < s.m⊢ ∑ n ∈ Finset.Icc s.m N, s.seq n = 0 s:SeriesN:ℤh:N < s.m⊢ ∀ x ∈ Finset.Icc s.m N, s.seq x = 0 s:SeriesN:ℤh:N < s.mn:ℤhn:n ∈ Finset.Icc s.m N⊢ s.seq n = 0; s:SeriesN:ℤh:N < s.mn:ℤhn:s.m ≤ n ∧ n ≤ N⊢ s.seq n = 0; All goals completed! 🐙abbrev Series.convergesTo (s : Series) (L:ℝ) : Prop := Filter.atTop.Tendsto (s.partial) (nhds L)abbrev Series.converges (s : Series) : Prop := ∃ L, s.convergesTo Labbrev Series.diverges (s : Series) : Prop := ¬s.convergesopen Classical in noncomputable abbrev Series.sum (s : Series) : ℝ := if h : s.converges then h.choose else 0theorem Series.converges_of_convergesTo {s : Series} {L:ℝ} (h: s.convergesTo L) : s.converges := s:SeriesL:ℝh:s.convergesTo L⊢ s.converges All goals completed! 🐙

Зауваження 7.2.3

theorem Series.sum_of_converges {s : Series} {L:ℝ} (h: s.convergesTo L) : s.sum = L := s:SeriesL:ℝh:s.convergesTo L⊢ s.sum = L s:SeriesL:ℝh:s.convergesTo L⊢ Exists.choose ⋯ = L All goals completed! 🐙
theorem Series.convergesTo_uniq {s : Series} {L L':ℝ} (h: s.convergesTo L) (h': s.convergesTo L') : L = L' := tendsto_nhds_unique h h'theorem Series.convergesTo_sum {s : Series} (h: s.converges) : s.convergesTo s.sum := s:Seriesh:s.converges⊢ s.convergesTo s.sum s:Seriesh:s.converges⊢ s.convergesTo (Exists.choose ⋯); All goals completed! 🐙

Приклад 7.2.4

noncomputable abbrev Series.example_7_2_4 := mk' (m := 1) (fun n ↦ (2:ℝ)^(-n:ℤ))
theorem declaration uses 'sorry'Series.example_7_2_4a {N:ℤ} (hN: N ≥ 1) : example_7_2_4.partial N = 1 - (2:ℝ)^(-N) := N:ℤhN:N ≥ 1⊢ example_7_2_4.partial N = 1 - 2 ^ (-N) All goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_4b : example_7_2_4.convergesTo 1 := ⊢ example_7_2_4.convergesTo 1 All goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_4c : example_7_2_4.sum = 1 := ⊢ example_7_2_4.sum = 1 All goals completed! 🐙noncomputable abbrev Series.example_7_2_4' := mk' (m := 1) (fun n ↦ (2:ℝ)^(n:ℤ))theorem declaration uses 'sorry'Series.example_7_2_4'a {N:ℤ} (hN: N ≥ 1) : example_7_2_4'.partial N = (2:ℝ)^(N+1) - 2 := N:ℤhN:N ≥ 1⊢ example_7_2_4'.partial N = 2 ^ (N + 1) - 2 All goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_4'b : example_7_2_4'.diverges := ⊢ example_7_2_4'.diverges All goals completed! 🐙

Твердження 7.2.5 / Вправа 7.2.2

theorem declaration uses 'sorry'Series.converges_iff_tail_decay (s:Series) : s.converges ↔ ∀ ε > 0, ∃ N ≥ s.m, ∀ p ≥ N, ∀ q ≥ N, |∑ n ∈ Finset.Icc p q, s.seq n| ≤ ε := s:Series⊢ s.converges ↔ ∀ ε > 0, ∃ N ≥ s.m, ∀ p ≥ N, ∀ q ≥ N, |∑ n ∈ Finset.Icc p q, s.seq n| ≤ ε All goals completed! 🐙

Наслідок 7.2.6 (Ознака нуля) / Вправа 7.2.3

theorem declaration uses 'sorry'Series.decay_of_converges {s:Series} (h: s.converges) : Filter.atTop.Tendsto s.seq (nhds 0) := s:Seriesh:s.converges⊢ Filter.Tendsto s.seq Filter.atTop (nhds 0) All goals completed! 🐙
theorem declaration uses 'sorry'Series.diverges_of_nodecay {s:Series} (h: ¬ Filter.atTop.Tendsto s.seq (nhds 0)) : s.diverges := s:Seriesh:¬Filter.Tendsto s.seq Filter.atTop (nhds 0)⊢ s.diverges All goals completed! 🐙

Приклад 7.2.7

theorem declaration uses 'sorry'Series.example_7_2_7 : ((fun n:ℕ ↦ (1:ℝ)):Series).diverges := ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1) n.toNat else 0, vanish := ⋯ }.diverges ⊢ ¬Filter.Tendsto { m := 0, seq := fun n => if n ≥ 0 then (fun n => 1) n.toNat else 0, vanish := ⋯ }.seq Filter.atTop (nhds 0) All goals completed! 🐙
theorem declaration uses 'sorry'Series.example_7_2_7' : ((fun n:ℕ ↦ (-1:ℝ)^n):Series).diverges := ⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ }.diverges ⊢ ¬Filter.Tendsto { m := 0, seq := fun n => if n ≥ 0 then (fun n => (-1) ^ n) n.toNat else 0, vanish := ⋯ }.seq Filter.atTop (nhds 0) All goals completed! 🐙

Визначення 7.2.8 (Абсолютна збіжність)

abbrev Series.abs (s:Series) : Series := mk' (m:=s.m) (fun n ↦ |s.seq n|)
abbrev Series.absConverges (s:Series) : Prop := s.abs.convergesabbrev Series.condConverges (s:Series) : Prop := s.converges ∧ ¬ s.absConverges

Твердження 7.2.9 (Критерій абсолютної збіжності) / Приклад 7.2.4

theorem declaration uses 'sorry'Series.converges_of_absConverges {s:Series} (h : s.absConverges) : s.converges := s:Seriesh:s.absConverges⊢ s.converges All goals completed! 🐙
theorem declaration uses 'sorry'Series.abs_le {s:Series} (h : s.absConverges) : |s.sum| ≤ s.abs.sum := s:Seriesh:s.absConverges⊢ |s.sum| ≤ s.abs.sum All goals completed! 🐙

Твердження 7.2.12 (Ознака знакозмінного ряду)

theorem declaration uses 'sorry'Series.converges_of_alternating {m:ℤ} {a: { n // n ≥ m} → ℝ} (ha: ∀ n, a n ≥ 0) (ha': Antitone a) : ((mk' (fun n ↦ (-1)^(n:ℤ) * a n)).converges ↔ Filter.atTop.Tendsto a (nhds 0)) := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) -- Доведення написане так, щоб відповідати структурі оригінального тексту. m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges → Filter.Tendsto a Filter.atTop (nhds 0)m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ Filter.Tendsto a Filter.atTop (nhds 0) → (mk' fun n => (-1) ^ ↑n * a n).converges m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges → Filter.Tendsto a Filter.atTop (nhds 0) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:(mk' fun n => (-1) ^ ↑n * a n).converges⊢ Filter.Tendsto a Filter.atTop (nhds 0); m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto (mk' fun n => (-1) ^ ↑n * a n).seq Filter.atTop (nhds 0)⊢ Filter.Tendsto a Filter.atTop (nhds 0) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto (fun b => dist ((mk' fun n => (-1) ^ ↑n * a n).seq b) 0) Filter.atTop (nhds 0)⊢ Filter.Tendsto (fun b => dist (a b) 0) Filter.atTop (nhds 0) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto (fun x => dist ((mk' fun n => (-1) ^ ↑n * a n).seq ↑x) 0) Filter.atTop (nhds 0)⊢ Filter.Tendsto (fun b => dist (a b) 0) Filter.atTop (nhds 0) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto (fun x => dist ((mk' fun n => (-1) ^ ↑n * a n).seq ↑x) 0) Filter.atTop (nhds 0)e_1✝:{ n // n ≥ m } = ↑(Set.Ici m)n:{ n // n ≥ m }⊢ dist (a n) 0 = dist ((mk' fun n => (-1) ^ ↑n * a n).seq ↑n) 0 All goals completed! 🐙 m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)⊢ (mk' fun n => (-1) ^ ↑n * a n).converges m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)⊢ ∃ L, Filter.Tendsto (mk' fun n => (-1) ^ ↑n * a n).partial Filter.atTop (nhds L) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 n⊢ ∃ L, Filter.Tendsto b.partial Filter.atTop (nhds L) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481⊢ ∃ L, Filter.Tendsto S Filter.atTop (nhds L) have claim0 {N:ℤ} (hN: N ≥ m) : S (N+1) = S N + (-1)^(N+1) * a ⟨ N+1, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481N:ℤhN:N ≥ m⊢ N + 1 ≥ m All goals completed! 🐙 ⟩ := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481N:ℤhN:N ≥ m⊢ (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ = b.seq (N + 1)m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481N:ℤhN:N ≥ m⊢ N ≥ b.m - 1; m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481N:ℤhN:N ≥ m⊢ N ≥ b.m - 1; All goals completed! 🐙 have claim1 {N:ℤ} (hN: N ≥ m) : S (N+2) = S N + (-1)^(N+1) * (a ⟨ N+1, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ N + 1 ≥ m All goals completed! 🐙 ⟩ - a ⟨ N+2, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ N + 2 ≥ m All goals completed! 🐙 ⟩) := calc S (N+2) = S N + (-1)^(N+1) * a ⟨ N+1, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ N + 1 ≥ m All goals completed! 🐙 ⟩ + (-1)^(N+2) * a ⟨ N+2, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ N + 2 ≥ m All goals completed! 🐙 ⟩ := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ S (N + 2) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + (-1) ^ (N + 2) * a ⟨N + 2, ⋯⟩ simp_rw [←claim0 hN, show N+2=N+1+1 m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ S (N + 2) = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + (-1) ^ (N + 2) * a ⟨N + 2, ⋯⟩ All goals completed! 🐙]; m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ N + 1 ≥ m; All goals completed! 🐙 _ = S N + (-1)^(N+1) * a ⟨ N+1, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ N + 1 ≥ m All goals completed! 🐙 ⟩ + (-1) * (-1)^(N+1) * a ⟨ N+2, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ N + 2 ≥ m All goals completed! 🐙 ⟩ := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + (-1) ^ (N + 2) * a ⟨N + 2, ⋯⟩ = S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + -1 * (-1) ^ (N + 1) * a ⟨N + 2, ⋯⟩ m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ (-1) ^ (N + 2) = -1 * (-1) ^ (N + 1); m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ (-1) ^ (N + 2) = (-1) ^ (1 + (N + 1))m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ -1 ≠ 0 m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ (-1) ^ (N + 2) = (-1) ^ (1 + (N + 1))m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ -1 ≠ 0 All goals completed! 🐙 _ = _ := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)N:ℤhN:N ≥ m⊢ S N + (-1) ^ (N + 1) * a ⟨N + 1, ⋯⟩ + -1 * (-1) ^ (N + 1) * a ⟨N + 2, ⋯⟩ = S N + (-1) ^ (N + 1) * (a ⟨N + 1, ⋯⟩ - a ⟨N + 2, ⋯⟩) All goals completed! 🐙 have claim2 {N:ℤ} (hN: N ≥ m) (h': Odd N) : S (N+2) ≥ S N := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)N:ℤhN:N ≥ mh':Odd N⊢ a ⟨N + 2, ⋯⟩ ≤ a ⟨N + 1, ⋯⟩; m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)N:ℤhN:N ≥ mh':Odd N⊢ ⟨N + 1, ⋯⟩ ≤ ⟨N + 2, ⋯⟩; All goals completed! 🐙 have claim3 {N:ℤ} (hN: N ≥ m) (h': Even N) : S (N+2) ≤ S N := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => @?_mvar.77836 N hN h'N:ℤhN:N ≥ mh':Even N⊢ a ⟨N + 2, ⋯⟩ ≤ a ⟨N + 1, ⋯⟩; m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => @?_mvar.77836 N hN h'N:ℤhN:N ≥ mh':Even N⊢ ⟨N + 1, ⋯⟩ ≤ ⟨N + 2, ⋯⟩; All goals completed! 🐙 have why1 {N:ℤ} (hN: N ≥ m) (h': Even N) (k:ℕ) : S (N+2*k) ≤ S N := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) All goals completed! 🐙 have why2 {N:ℤ} (hN: N ≥ m) (h': Even N) (k:ℕ) : S (N+2*k+1) ≥ S N - a ⟨ N+1, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (Eq.mpr (id (congrArg (fun x => @_fvar.32561 (N + 2) = x + (-1) ^ (N + 2) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Eq.symm (@_fvar.35045 N hN)))) (Eq.mpr (id (congr (congrArg (fun x => Eq (@_fvar.32561 x)) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this)) (congrArg (HAdd.hAdd (@_fvar.32561 (N + 1))) (congr (congrArg (fun x => HMul.hMul ((-1) ^ x)) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this)) (congrArg _fvar.27161 ((fun {α} {p} val val_1 e_val => Eq.rec (motive := fun val_2 e_val => ∀ (property : p val), ⟨val, property⟩ = ⟨val_2, e_val ▸ property⟩) (fun property => Eq.refl ⟨val, property⟩) e_val) (N + 2) (N + 1 + 1) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this) (Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN))))))) (@_fvar.35045 (N + 1) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.27160) (Mathlib.Tactic.Ring.atom_pf N) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.27160 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.27160 ^ Nat.rawCast 1 * Nat.rawCast 1 + (N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.atom_pf _fvar.27160) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.27160 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.27160 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.27160 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le hN)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) ((fun {α β γ} [HAdd α β γ] a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 a_4 : β), a_3 = a_4 → a + a_3 = a_2 + a_4) (fun a_2 a_3 e_a => e_a ▸ Eq.refl (a + a_2)) e_a) (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Eq.refl (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) ((-1) ^ (N + 2) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (-1 * (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) ((fun {α β γ} [HMul α β γ] a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 a_4 : β), a_3 = a_4 → a * a_3 = a_2 * a_4) (fun a_2 a_3 e_a => e_a ▸ Eq.refl (a * a_2)) e_a) ((-1) ^ (N + 2)) (-1 * (-1) ^ (N + 1)) (Eq.mpr (id (congrArg (fun _a => (-1) ^ (N + 2) = _a) (Eq.symm (zpow_one_add₀ (Chapter7.Series.converges_of_alternating._proof_6 _fvar.35045 hN) (N + 1))))) (Chapter7.Series.converges_of_alternating._proof_5 _fvar.35045 hN)) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Eq.refl (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.32561 N)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.mul_zero (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_lt (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.32561 N)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Int.negOfNat 1).rawCast))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))))claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => Eq.mpr (id (Eq.trans (Eq.trans (congrArg (fun x => x ≥ @_fvar.32561 N) (Eq.trans (@_fvar.50460 N hN) (congrArg (HAdd.hAdd (@_fvar.32561 N)) (Eq.trans (congrArg (fun x => x * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) ((fun x_0 x_1 x_2 => (fun x_0 x_1 x_2 => Even.neg_one_zpow (Odd.add_one h')) x_0 x_1 x_2) ℝ CommGroupWithZero.toDivisionCommMonoid.toDivisionMonoid NonUnitalNonAssocRing.toHasDistribNeg)) (one_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)))))) ge_iff_le._simp_1) (Eq.trans (le_mul_iff_one_le_right'._simp_4 (@_fvar.32561 N)) one_le_div'._simp_4))) (@_fvar.27163 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ (of_eq_true (Eq.trans Subtype.mk_le_mk._simp_1 (Eq.trans (mul_le_mul_iff_left._simp_4 N) Nat.one_le_ofNat._simp_1))))claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => Eq.mpr (id (Eq.trans (Eq.trans (congrArg (fun x => x ≤ @_fvar.32561 N) (Eq.trans (@_fvar.50460 N hN) (congrArg (HAdd.hAdd (@_fvar.32561 N)) (Eq.trans (Eq.trans (congrArg (fun x => x * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) ((fun x_0 x_1 => (fun x_0 x_1 => Odd.neg_one_zpow (Even.add_one h')) x_0 x_1) ℝ Real.instDivisionRing)) (neg_mul 1 (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))) (Eq.trans (congrArg Neg.neg (one_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))) (neg_sub (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))))))) (mul_le_iff_le_one_right'._simp_4 (@_fvar.32561 N))) (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (zero_add (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)))))) (@_fvar.27163 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ (of_eq_true (Eq.trans Subtype.mk_le_mk._simp_1 (Eq.trans (mul_le_mul_iff_left._simp_4 N) Nat.one_le_ofNat._simp_1))))why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => sorryN:ℤhN:N ≥ mh':Even Nk:ℕ⊢ N + 1 ≥ m All goals completed! 🐙 ⟩ := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) All goals completed! 🐙 have why3 {N:ℤ} (hN: N ≥ m) (h': Even N) (k:ℕ) : S (N+2*k+1) ≤ S (N+2*k) := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) All goals completed! 🐙 have claim4 {N:ℤ} (hN: N ≥ m) (h': Even N) (k:ℕ) : S N - a ⟨ N+1, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (Eq.mpr (id (congrArg (fun x => @_fvar.32561 (N + 2) = x + (-1) ^ (N + 2) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Eq.symm (@_fvar.35045 N hN)))) (Eq.mpr (id (congr (congrArg (fun x => Eq (@_fvar.32561 x)) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this)) (congrArg (HAdd.hAdd (@_fvar.32561 (N + 1))) (congr (congrArg (fun x => HMul.hMul ((-1) ^ x)) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this)) (congrArg _fvar.27161 ((fun {α} {p} val val_1 e_val => Eq.rec (motive := fun val_2 e_val => ∀ (property : p val), ⟨val, property⟩ = ⟨val_2, e_val ▸ property⟩) (fun property => Eq.refl ⟨val, property⟩) e_val) (N + 2) (N + 1 + 1) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this) (Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN))))))) (@_fvar.35045 (N + 1) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.27160) (Mathlib.Tactic.Ring.atom_pf N) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.27160 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.27160 ^ Nat.rawCast 1 * Nat.rawCast 1 + (N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.atom_pf _fvar.27160) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.27160 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.27160 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.27160 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le hN)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) ((fun {α β γ} [HAdd α β γ] a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 a_4 : β), a_3 = a_4 → a + a_3 = a_2 + a_4) (fun a_2 a_3 e_a => e_a ▸ Eq.refl (a + a_2)) e_a) (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Eq.refl (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) ((-1) ^ (N + 2) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (-1 * (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) ((fun {α β γ} [HMul α β γ] a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 a_4 : β), a_3 = a_4 → a * a_3 = a_2 * a_4) (fun a_2 a_3 e_a => e_a ▸ Eq.refl (a * a_2)) e_a) ((-1) ^ (N + 2)) (-1 * (-1) ^ (N + 1)) (Eq.mpr (id (congrArg (fun _a => (-1) ^ (N + 2) = _a) (Eq.symm (zpow_one_add₀ (Chapter7.Series.converges_of_alternating._proof_6 _fvar.35045 hN) (N + 1))))) (Chapter7.Series.converges_of_alternating._proof_5 _fvar.35045 hN)) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Eq.refl (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.32561 N)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.mul_zero (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_lt (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.32561 N)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Int.negOfNat 1).rawCast))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))))claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => Eq.mpr (id (Eq.trans (Eq.trans (congrArg (fun x => x ≥ @_fvar.32561 N) (Eq.trans (@_fvar.50460 N hN) (congrArg (HAdd.hAdd (@_fvar.32561 N)) (Eq.trans (congrArg (fun x => x * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) ((fun x_0 x_1 x_2 => (fun x_0 x_1 x_2 => Even.neg_one_zpow (Odd.add_one h')) x_0 x_1 x_2) ℝ CommGroupWithZero.toDivisionCommMonoid.toDivisionMonoid NonUnitalNonAssocRing.toHasDistribNeg)) (one_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)))))) ge_iff_le._simp_1) (Eq.trans (le_mul_iff_one_le_right'._simp_4 (@_fvar.32561 N)) one_le_div'._simp_4))) (@_fvar.27163 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ (of_eq_true (Eq.trans Subtype.mk_le_mk._simp_1 (Eq.trans (mul_le_mul_iff_left._simp_4 N) Nat.one_le_ofNat._simp_1))))claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => Eq.mpr (id (Eq.trans (Eq.trans (congrArg (fun x => x ≤ @_fvar.32561 N) (Eq.trans (@_fvar.50460 N hN) (congrArg (HAdd.hAdd (@_fvar.32561 N)) (Eq.trans (Eq.trans (congrArg (fun x => x * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) ((fun x_0 x_1 => (fun x_0 x_1 => Odd.neg_one_zpow (Even.add_one h')) x_0 x_1) ℝ Real.instDivisionRing)) (neg_mul 1 (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))) (Eq.trans (congrArg Neg.neg (one_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))) (neg_sub (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))))))) (mul_le_iff_le_one_right'._simp_4 (@_fvar.32561 N))) (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (zero_add (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)))))) (@_fvar.27163 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ (of_eq_true (Eq.trans Subtype.mk_le_mk._simp_1 (Eq.trans (mul_le_mul_iff_left._simp_4 N) Nat.one_le_ofNat._simp_1))))why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => sorrywhy2:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≥ @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN h' k => sorrywhy3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) := fun {N} hN h' k => sorryN:ℤhN:N ≥ mh':Even Nk:ℕ⊢ N + 1 ≥ m All goals completed! 🐙 ⟩ ≤ S (N + 2*k + 1) ∧ S (N + 2*k + 1) ≤ S (N + 2*k) ∧ S (N + 2*k) ≤ S N := ⟨ ge_iff_le.mp (why2 hN h' k), why3 hN h' k, why1 hN h' k ⟩ have why4 {N n:ℤ} (hN: N ≥ m) (h': Even N) (hn: n ≥ N) : S N - a ⟨ N+1, m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (Eq.mpr (id (congrArg (fun x => @_fvar.32561 (N + 2) = x + (-1) ^ (N + 2) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Eq.symm (@_fvar.35045 N hN)))) (Eq.mpr (id (congr (congrArg (fun x => Eq (@_fvar.32561 x)) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this)) (congrArg (HAdd.hAdd (@_fvar.32561 (N + 1))) (congr (congrArg (fun x => HMul.hMul ((-1) ^ x)) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this)) (congrArg _fvar.27161 ((fun {α} {p} val val_1 e_val => Eq.rec (motive := fun val_2 e_val => ∀ (property : p val), ⟨val, property⟩ = ⟨val_2, e_val ▸ property⟩) (fun property => Eq.refl ⟨val, property⟩) e_val) (N + 2) (N + 1 + 1) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this) (Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN))))))) (@_fvar.35045 (N + 1) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.27160) (Mathlib.Tactic.Ring.atom_pf N) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.27160 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.27160 ^ Nat.rawCast 1 * Nat.rawCast 1 + (N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.atom_pf _fvar.27160) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.27160 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.27160 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.27160 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le hN)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) ((fun {α β γ} [HAdd α β γ] a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 a_4 : β), a_3 = a_4 → a + a_3 = a_2 + a_4) (fun a_2 a_3 e_a => e_a ▸ Eq.refl (a + a_2)) e_a) (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Eq.refl (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) ((-1) ^ (N + 2) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (-1 * (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) ((fun {α β γ} [HMul α β γ] a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 a_4 : β), a_3 = a_4 → a * a_3 = a_2 * a_4) (fun a_2 a_3 e_a => e_a ▸ Eq.refl (a * a_2)) e_a) ((-1) ^ (N + 2)) (-1 * (-1) ^ (N + 1)) (Eq.mpr (id (congrArg (fun _a => (-1) ^ (N + 2) = _a) (Eq.symm (zpow_one_add₀ (Chapter7.Series.converges_of_alternating._proof_6 _fvar.35045 hN) (N + 1))))) (Chapter7.Series.converges_of_alternating._proof_5 _fvar.35045 hN)) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Eq.refl (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.32561 N)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.mul_zero (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_lt (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.32561 N)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Int.negOfNat 1).rawCast))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))))claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => Eq.mpr (id (Eq.trans (Eq.trans (congrArg (fun x => x ≥ @_fvar.32561 N) (Eq.trans (@_fvar.50460 N hN) (congrArg (HAdd.hAdd (@_fvar.32561 N)) (Eq.trans (congrArg (fun x => x * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) ((fun x_0 x_1 x_2 => (fun x_0 x_1 x_2 => Even.neg_one_zpow (Odd.add_one h')) x_0 x_1 x_2) ℝ CommGroupWithZero.toDivisionCommMonoid.toDivisionMonoid NonUnitalNonAssocRing.toHasDistribNeg)) (one_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)))))) ge_iff_le._simp_1) (Eq.trans (le_mul_iff_one_le_right'._simp_4 (@_fvar.32561 N)) one_le_div'._simp_4))) (@_fvar.27163 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ (of_eq_true (Eq.trans Subtype.mk_le_mk._simp_1 (Eq.trans (mul_le_mul_iff_left._simp_4 N) Nat.one_le_ofNat._simp_1))))claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => Eq.mpr (id (Eq.trans (Eq.trans (congrArg (fun x => x ≤ @_fvar.32561 N) (Eq.trans (@_fvar.50460 N hN) (congrArg (HAdd.hAdd (@_fvar.32561 N)) (Eq.trans (Eq.trans (congrArg (fun x => x * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) ((fun x_0 x_1 => (fun x_0 x_1 => Odd.neg_one_zpow (Even.add_one h')) x_0 x_1) ℝ Real.instDivisionRing)) (neg_mul 1 (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))) (Eq.trans (congrArg Neg.neg (one_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))) (neg_sub (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))))))) (mul_le_iff_le_one_right'._simp_4 (@_fvar.32561 N))) (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (zero_add (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)))))) (@_fvar.27163 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ (of_eq_true (Eq.trans Subtype.mk_le_mk._simp_1 (Eq.trans (mul_le_mul_iff_left._simp_4 N) Nat.one_le_ofNat._simp_1))))why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => sorrywhy2:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≥ @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN h' k => sorrywhy3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) := fun {N} hN h' k => sorryclaim4:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 (N + 2 * ↑k + 1) ∧ @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) ∧ @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => ⟨ge_iff_le.mp (@_fvar.102437 N hN h' k), ⟨@_fvar.102992 N hN h' k, @_fvar.91542 N hN h' k⟩⟩N:ℤn:ℤhN:N ≥ mh':Even Nhn:n ≥ N⊢ N + 1 ≥ m All goals completed! 🐙 ⟩ ≤ S n ∧ S n ≤ S N := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) All goals completed! 🐙 have why5 {ε:ℝ} (hε: ε > 0) : ∃ N, ∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) All goals completed! 🐙 have : CauchySeq S := m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone a⊢ (mk' fun n => (-1) ^ ↑n * a n).converges ↔ Filter.Tendsto a Filter.atTop (nhds 0) m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => @?_mvar.77836 N hN h'claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => @?_mvar.84573 N hN h'why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => @?_mvar.91541 N hN h' kwhy2:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≥ @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN h' k => @?_mvar.102436 N hN h' kwhy3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) := fun {N} hN h' k => @?_mvar.102991 N hN h' kclaim4:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 (N + 2 * ↑k + 1) ∧ @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) ∧ @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => ⟨ge_iff_le.mp (@_fvar.102437 N hN h' k), ⟨@_fvar.102992 N hN h' k, @_fvar.91542 N hN h' k⟩⟩why4:∀ {N n : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (hn : n ≥ N), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 n ∧ @_fvar.32561 n ≤ @_fvar.32561 N := fun {N n} hN h' hn => @?_mvar.138094 N n hN h' hnwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |@_fvar.32561 n - @_fvar.32561 m| ≤ ε := fun {ε} hε => @?_mvar.138638 ε hε⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (S n) (S N) < ε m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => @?_mvar.77836 N hN h'claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => @?_mvar.84573 N hN h'why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => @?_mvar.91541 N hN h' kwhy2:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≥ @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN h' k => @?_mvar.102436 N hN h' kwhy3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) := fun {N} hN h' k => @?_mvar.102991 N hN h' kclaim4:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 (N + 2 * ↑k + 1) ∧ @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) ∧ @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => ⟨ge_iff_le.mp (@_fvar.102437 N hN h' k), ⟨@_fvar.102992 N hN h' k, @_fvar.91542 N hN h' k⟩⟩why4:∀ {N n : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (hn : n ≥ N), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 n ∧ @_fvar.32561 n ≤ @_fvar.32561 N := fun {N n} hN h' hn => @?_mvar.138094 N n hN h' hnwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |@_fvar.32561 n - @_fvar.32561 m| ≤ ε := fun {ε} hε => @?_mvar.138638 ε hεε:ℝhε:ε > 0⊢ ∃ N, ∀ n ≥ N, dist (S n) (S N) < ε; m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => @?_mvar.77836 N hN h'claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => @?_mvar.84573 N hN h'why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => @?_mvar.91541 N hN h' kwhy2:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≥ @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN h' k => @?_mvar.102436 N hN h' kwhy3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) := fun {N} hN h' k => @?_mvar.102991 N hN h' kclaim4:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 (N + 2 * ↑k + 1) ∧ @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) ∧ @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => ⟨ge_iff_le.mp (@_fvar.102437 N hN h' k), ⟨@_fvar.102992 N hN h' k, @_fvar.91542 N hN h' k⟩⟩why4:∀ {N n : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (hn : n ≥ N), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 n ∧ @_fvar.32561 n ≤ @_fvar.32561 N := fun {N n} hN h' hn => @?_mvar.138094 N n hN h' hnwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |@_fvar.32561 n - @_fvar.32561 m| ≤ ε := fun {ε} hε => @?_mvar.138638 ε hεε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2⊢ ∃ N, ∀ n ≥ N, dist (S n) (S N) < ε; m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => @?_mvar.77836 N hN h'claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => @?_mvar.84573 N hN h'why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => @?_mvar.91541 N hN h' kwhy2:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≥ @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN h' k => @?_mvar.102436 N hN h' kwhy3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) := fun {N} hN h' k => @?_mvar.102991 N hN h' kclaim4:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 (N + 2 * ↑k + 1) ∧ @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) ∧ @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => ⟨ge_iff_le.mp (@_fvar.102437 N hN h' k), ⟨@_fvar.102992 N hN h' k, @_fvar.91542 N hN h' k⟩⟩why4:∀ {N n : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (hn : n ≥ N), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 n ∧ @_fvar.32561 n ≤ @_fvar.32561 N := fun {N n} hN h' hn => @?_mvar.138094 N n hN h' hnwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |@_fvar.32561 n - @_fvar.32561 m| ≤ ε := fun {ε} hε => @?_mvar.138638 ε hεε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2⊢ ∀ n ≥ N, dist (S n) (S N) < ε m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => @?_mvar.77836 N hN h'claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => @?_mvar.84573 N hN h'why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => @?_mvar.91541 N hN h' kwhy2:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≥ @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN h' k => @?_mvar.102436 N hN h' kwhy3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) := fun {N} hN h' k => @?_mvar.102991 N hN h' kclaim4:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 (N + 2 * ↑k + 1) ∧ @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) ∧ @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => ⟨ge_iff_le.mp (@_fvar.102437 N hN h' k), ⟨@_fvar.102992 N hN h' k, @_fvar.91542 N hN h' k⟩⟩why4:∀ {N n : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (hn : n ≥ N), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 n ∧ @_fvar.32561 n ≤ @_fvar.32561 N := fun {N n} hN h' hn => @?_mvar.138094 N n hN h' hnwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |@_fvar.32561 n - @_fvar.32561 m| ≤ ε := fun {ε} hε => @?_mvar.138638 ε hεε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2n:ℤhn:n ≥ N⊢ dist (S n) (S N) < ε; m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN => @?_mvar.35044 N hNclaim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (@?_mvar.50451 N hN) (@?_mvar.50456 N hN)) (@?_mvar.50459 N hN)claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => @?_mvar.77836 N hN h'claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => @?_mvar.84573 N hN h'why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => @?_mvar.91541 N hN h' kwhy2:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≥ @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN h' k => @?_mvar.102436 N hN h' kwhy3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) := fun {N} hN h' k => @?_mvar.102991 N hN h' kclaim4:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 (N + 2 * ↑k + 1) ∧ @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) ∧ @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => ⟨ge_iff_le.mp (@_fvar.102437 N hN h' k), ⟨@_fvar.102992 N hN h' k, @_fvar.91542 N hN h' k⟩⟩why4:∀ {N n : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (hn : n ≥ N), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 n ∧ @_fvar.32561 n ≤ @_fvar.32561 N := fun {N n} hN h' hn => @?_mvar.138094 N n hN h' hnwhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |@_fvar.32561 n - @_fvar.32561 m| ≤ ε := fun {ε} hε => @?_mvar.138638 ε hεε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2n:ℤhn:n ≥ N⊢ |S n - S N| < ε; linarith [hN n hn N (m:ℤa:{ n // n ≥ m } → ℝha:∀ (n : { n // n ≥ m }), a n ≥ 0ha':Antitone ah:Filter.Tendsto a Filter.atTop (nhds 0)b:Chapter7.Series := Chapter7.Series.mk' fun n => (-1) ^ ↑n * @_fvar.27161 nS:ℤ → ℝ := Chapter7.Series.partial _fvar.32481claim0:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 1) = @_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, ⋯⟩ := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim1:∀ {N : ℤ} (hN : N ≥ _fvar.27160), @_fvar.32561 (N + 2) = @_fvar.32561 N + (-1) ^ (N + 1) * (@_fvar.27161 ⟨N + 1, ⋯⟩ - @_fvar.27161 ⟨N + 2, ⋯⟩) := fun {N} hN => Trans.trans (Trans.trans (Eq.mpr (id (congrArg (fun x => @_fvar.32561 (N + 2) = x + (-1) ^ (N + 2) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Eq.symm (@_fvar.35045 N hN)))) (Eq.mpr (id (congr (congrArg (fun x => Eq (@_fvar.32561 x)) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this)) (congrArg (HAdd.hAdd (@_fvar.32561 (N + 1))) (congr (congrArg (fun x => HMul.hMul ((-1) ^ x)) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this)) (congrArg _fvar.27161 ((fun {α} {p} val val_1 e_val => Eq.rec (motive := fun val_2 e_val => ∀ (property : p val), ⟨val, property⟩ = ⟨val_2, e_val ▸ property⟩) (fun property => Eq.refl ⟨val, property⟩) e_val) (N + 2) (N + 1 + 1) (have this := Eq.trans (Mathlib.Tactic.Abel.subst_into_addg N 2 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 2 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 2) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 2 0) (Mathlib.Tactic.Abel.termg 1 2 0) (zero_add (Mathlib.Tactic.Abel.termg 1 2 0)))) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (N + 1) 1 (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 2 1 0)) (Mathlib.Tactic.Abel.subst_into_addg N 1 (Mathlib.Tactic.Abel.termg 1 N 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 N (Mathlib.Tactic.Abel.termg 1 1 0)) (Mathlib.Tactic.Abel.term_atomg N) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N 0 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (zero_add (Mathlib.Tactic.Abel.termg 1 1 0)))) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_add_constg 1 N (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 2 1 0) (Mathlib.Tactic.Abel.term_add_termg 1 1 0 1 0 2 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)) (Eq.refl 2)) (Eq.refl 2)) (zero_add 0))))); this) (Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN))))))) (@_fvar.35045 (N + 1) (le_of_not_gt fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2))) (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2)))) (Mathlib.Tactic.Ring.mul_zero (Nat.rawCast 2)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul ((Int.negOfNat 1).rawCast + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero ((Int.negOfNat 2).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.27160) (Mathlib.Tactic.Ring.atom_pf N) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul N (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (_fvar.27160 ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 2).rawCast (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.27160 ^ Nat.rawCast 1 * Nat.rawCast 1 + (N ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf N) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_overlap (Mathlib.Meta.NormNum.IsNat.to_raw_eq (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2))) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.atom_pf _fvar.27160) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.27160 (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2) (Mathlib.Tactic.Ring.add_pf_add_gt (_fvar.27160 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (N ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.27160 (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero N (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.mul_neg (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Meta.NormNum.isNat_lt_true (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)) (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)) (Eq.refl false))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le hN)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) ((fun {α β γ} [HAdd α β γ] a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 a_4 : β), a_3 = a_4 → a + a_3 = a_2 + a_4) (fun a_2 a_3 e_a => e_a ▸ Eq.refl (a + a_2)) e_a) (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Eq.refl (@_fvar.32561 N + (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) ((-1) ^ (N + 2) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (-1 * (-1) ^ (N + 1) * @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) ((fun {α β γ} [HMul α β γ] a a_1 e_a => Eq.rec (motive := fun a_2 e_a => ∀ (a_3 a_4 : β), a_3 = a_4 → a * a_3 = a_2 * a_4) (fun a_2 a_3 e_a => e_a ▸ Eq.refl (a * a_2)) e_a) ((-1) ^ (N + 2)) (-1 * (-1) ^ (N + 1)) (Eq.mpr (id (congrArg (fun _a => (-1) ^ (N + 2) = _a) (Eq.symm (zpow_one_add₀ (Chapter7.Series.converges_of_alternating._proof_6 _fvar.35045 hN) (N + 1))))) (Chapter7.Series.converges_of_alternating._proof_5 _fvar.35045 hN)) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Eq.refl (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))))) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.32561 N)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℝ Nat.cast_one)) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_right ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.mul_zero (Int.negOfNat 1).rawCast) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.zero_mul (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_one (Int.negOfNat 1).rawCast))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_lt (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.32561 N)) (Mathlib.Tactic.Ring.mul_congr (Mathlib.Tactic.Ring.atom_pf ((-1) ^ (N + 1))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.atom_pf (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℝ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℝ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))))) (Mathlib.Tactic.Ring.add_mul (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))) (Mathlib.Tactic.Ring.mul_add (Mathlib.Tactic.Ring.mul_pf_left ((-1) ^ (N + 1)) (Nat.rawCast 1) (Mathlib.Tactic.Ring.mul_pf_right (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩) (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Int.negOfNat 1).rawCast))) (Mathlib.Tactic.Ring.mul_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))) (Mathlib.Tactic.Ring.add_pf_add_lt (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1)) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0)))) (Mathlib.Tactic.Ring.zero_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1 + (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0))) (Mathlib.Tactic.Ring.add_pf_add_zero (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))) (Mathlib.Tactic.Ring.add_pf_add_lt (@_fvar.32561 N ^ Nat.rawCast 1 * Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_zero_add (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * Nat.rawCast 1) + (((-1) ^ (N + 1)) ^ Nat.rawCast 1 * (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast) + 0))))))claim2:∀ {N : ℤ}, N ≥ _fvar.27160 → Odd N → @_fvar.32561 (N + 2) ≥ @_fvar.32561 N := fun {N} hN h' => Eq.mpr (id (Eq.trans (Eq.trans (congrArg (fun x => x ≥ @_fvar.32561 N) (Eq.trans (@_fvar.50460 N hN) (congrArg (HAdd.hAdd (@_fvar.32561 N)) (Eq.trans (congrArg (fun x => x * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) ((fun x_0 x_1 x_2 => (fun x_0 x_1 x_2 => Even.neg_one_zpow (Odd.add_one h')) x_0 x_1 x_2) ℝ CommGroupWithZero.toDivisionCommMonoid.toDivisionMonoid NonUnitalNonAssocRing.toHasDistribNeg)) (one_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)))))) ge_iff_le._simp_1) (Eq.trans (le_mul_iff_one_le_right'._simp_4 (@_fvar.32561 N)) one_le_div'._simp_4))) (@_fvar.27163 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ (of_eq_true (Eq.trans Subtype.mk_le_mk._simp_1 (Eq.trans (mul_le_mul_iff_left._simp_4 N) Nat.one_le_ofNat._simp_1))))claim3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → @_fvar.32561 (N + 2) ≤ @_fvar.32561 N := fun {N} hN h' => Eq.mpr (id (Eq.trans (Eq.trans (congrArg (fun x => x ≤ @_fvar.32561 N) (Eq.trans (@_fvar.50460 N hN) (congrArg (HAdd.hAdd (@_fvar.32561 N)) (Eq.trans (Eq.trans (congrArg (fun x => x * (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) ((fun x_0 x_1 => (fun x_0 x_1 => Odd.neg_one_zpow (Even.add_one h')) x_0 x_1) ℝ Real.instDivisionRing)) (neg_mul 1 (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))) (Eq.trans (congrArg Neg.neg (one_mul (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ - @_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))) (neg_sub (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩) (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩))))))) (mul_le_iff_le_one_right'._simp_4 (@_fvar.32561 N))) (Eq.trans tsub_le_iff_right._simp_1 (congrArg (LE.le (@_fvar.27161 ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩)) (zero_add (@_fvar.27161 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩)))))) (@_fvar.27163 ⟨N + 1, Chapter7.Series.converges_of_alternating._proof_3 _fvar.35045 hN⟩ ⟨N + 2, Chapter7.Series.converges_of_alternating._proof_4 _fvar.35045 hN⟩ (of_eq_true (Eq.trans Subtype.mk_le_mk._simp_1 (Eq.trans (mul_le_mul_iff_left._simp_4 N) Nat.one_le_ofNat._simp_1))))why1:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => sorrywhy2:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≥ @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ := fun {N} hN h' k => sorrywhy3:∀ {N : ℤ}, N ≥ _fvar.27160 → Even N → ∀ (k : ℕ), @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) := fun {N} hN h' k => sorryclaim4:∀ {N : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (k : ℕ), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 (N + 2 * ↑k + 1) ∧ @_fvar.32561 (N + 2 * ↑k + 1) ≤ @_fvar.32561 (N + 2 * ↑k) ∧ @_fvar.32561 (N + 2 * ↑k) ≤ @_fvar.32561 N := fun {N} hN h' k => ⟨ge_iff_le.mp (@_fvar.102437 N hN h' k), ⟨@_fvar.102992 N hN h' k, @_fvar.91542 N hN h' k⟩⟩why4:∀ {N n : ℤ} (hN : N ≥ _fvar.27160) (h' : Even N) (hn : n ≥ N), @_fvar.32561 N - @_fvar.27161 ⟨N + 1, ⋯⟩ ≤ @_fvar.32561 n ∧ @_fvar.32561 n ≤ @_fvar.32561 N := fun {N n} hN h' hn => sorrywhy5:∀ {ε : ℝ}, ε > 0 → ∃ N, ∀ n ≥ N, ∀ m ≥ N, |@_fvar.32561 n - @_fvar.32561 m| ≤ ε := fun {ε} hε => sorryε:ℝhε:ε > 0N:ℤhN:∀ n ≥ N, ∀ m ≥ N, |S n - S m| ≤ ε / 2n:ℤhn:n ≥ N⊢ N ≥ N All goals completed! 🐙)] All goals completed! 🐙

Приклад 7.2.13

noncomputable abbrev Series.example_7_2_13 : Series := (mk' (m:=1) (fun n ↦ (-1:ℝ)^(n:ℤ) / (n:ℤ)))
theorem declaration uses 'sorry'Series.example_7_2_13a : example_7_2_13.converges := ⊢ example_7_2_13.converges All goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_13b : ¬ example_7_2_13.absConverges := ⊢ ¬example_7_2_13.absConverges All goals completed! 🐙theorem declaration uses 'sorry'Series.example_7_2_13c : example_7_2_13.condConverges := ⊢ example_7_2_13.condConverges All goals completed! 🐙instance Series.inst_add : Add Series where add a b := { m := max a.m b.m seq n := if n ≥ max a.m b.m then a.seq n + b.seq n else 0 vanish n hn := a:Seriesb:Seriesn:ℤhn:n < max a.m b.m⊢ (if n ≥ max a.m b.m then a.seq n + b.seq n else 0) = 0 a:Seriesb:Seriesn:ℤhn:¬max a.m b.m ≤ n⊢ (if n ≥ max a.m b.m then a.seq n + b.seq n else 0) = 0; All goals completed! 🐙 }theorem Series.add_coe (a b: ℕ → ℝ) : (a:Series) + (b:Series) = (fun n ↦ a n + b n) := a:ℕ → ℝb:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } + { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ } = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ } a:ℕ → ℝb:ℕ → ℝ⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } + { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).m = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.ma:ℕ → ℝb:ℕ → ℝn:ℤ⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } + { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq n; a:ℕ → ℝb:ℕ → ℝn:ℤ⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } + { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq n a:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } + { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq na:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } + { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq n a:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } + { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq na:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } + { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n + b n) n.toNat else 0, vanish := ⋯ }.seq n All goals completed! 🐙

Твердження 7.2.14 (a) (Закони для рядів) / Вправа 7.2.5. Форма Unknown identifier `convergesTo`convergesTo може бути зручнішою для застосувань.

theorem declaration uses 'sorry'Series.convergesTo.add {s t:Series} {L M: ℝ} (hs: s.convergesTo L) (ht: t.convergesTo M) : (s + t).convergesTo (L + M) := s:Seriest:SeriesL:ℝM:ℝhs:s.convergesTo Lht:t.convergesTo M⊢ (s + t).convergesTo (L + M) All goals completed! 🐙
theorem declaration uses 'sorry'Series.add {s t:Series} (hs: s.converges) (ht: t.converges) : (s + t).converges ∧ (s+t).sum = s.sum + t.sum := s:Seriest:Serieshs:s.convergesht:t.converges⊢ (s + t).converges ∧ (s + t).sum = s.sum + t.sum All goals completed! 🐙instance Series.inst.smul : SMul ℝ Series where smul c s := { m := s.m seq n := if n ≥ s.m then c * s.seq n else 0 vanish := c:ℝs:Series⊢ ∀ n < s.m, (if n ≥ s.m then c * s.seq n else 0) = 0 All goals completed! 🐙 }theorem Series.smul_coe (a: ℕ → ℝ) (c: ℝ) : (c • a:Series) = (fun n ↦ c * a n) := a:ℕ → ℝc:ℝ⊢ c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ } a:ℕ → ℝc:ℝ⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).m = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.ma:ℕ → ℝc:ℝn:ℤ⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq n; a:ℕ → ℝc:ℝn:ℤ⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq n a:ℕ → ℝc:ℝn:ℤh:n ≥ 0⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq na:ℕ → ℝc:ℝn:ℤh:¬n ≥ 0⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq n a:ℕ → ℝc:ℝn:ℤh:n ≥ 0⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq na:ℕ → ℝc:ℝn:ℤh:¬n ≥ 0⊢ (c • { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => c * a n) n.toNat else 0, vanish := ⋯ }.seq n All goals completed! 🐙

Твердження 7.2.14 (b) (Закони для рядів) / Вправа 7.2.5. Форма Unknown identifier `convergesTo`convergesTo може бути зручнішою для застосувань.

theorem declaration uses 'sorry'Series.convergesTo.smul {s:Series} {L c: ℝ} (hs: s.convergesTo L) : (c • s).convergesTo (c * L) := s:SeriesL:ℝc:ℝhs:s.convergesTo L⊢ (c • s).convergesTo (c * L) All goals completed! 🐙
theorem declaration uses 'sorry'Series.smul {c:ℝ} {s:Series} (hs: s.converges) : (c • s).converges ∧ (c • s).sum = c * s.sum := c:ℝs:Serieshs:s.converges⊢ (c • s).converges ∧ (c • s).sum = c * s.sum All goals completed! 🐙

Відповідного API для віднімання не було в підручнику, але воно корисне у наступних розділах, тому додається тут.

instance Series.inst_sub : Sub Series where sub a b := { m := max a.m b.m seq n := if n ≥ max a.m b.m then a.seq n - b.seq n else 0 vanish := a:Seriesb:Series⊢ ∀ n < max a.m b.m, (if n ≥ max a.m b.m then a.seq n - b.seq n else 0) = 0 All goals completed! 🐙 }
theorem Series.sub_coe (a b: ℕ → ℝ) : (a:Series) - (b:Series) = (fun n ↦ a n - b n) := a:ℕ → ℝb:ℕ → ℝ⊢ { m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } - { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ } = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ } a:ℕ → ℝb:ℕ → ℝ⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } - { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).m = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.ma:ℕ → ℝb:ℕ → ℝn:ℤ⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } - { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq n; a:ℕ → ℝb:ℕ → ℝn:ℤ⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } - { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq n a:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } - { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq na:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } - { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq n a:ℕ → ℝb:ℕ → ℝn:ℤh:n ≥ 0⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } - { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq na:ℕ → ℝb:ℕ → ℝn:ℤh:¬n ≥ 0⊢ ({ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ } - { m := 0, seq := fun n => if n ≥ 0 then b n.toNat else 0, vanish := ⋯ }).seq n = { m := 0, seq := fun n => if n ≥ 0 then (fun n => a n - b n) n.toNat else 0, vanish := ⋯ }.seq n All goals completed! 🐙theorem declaration uses 'sorry'Series.convergesTo.sub {s t:Series} {L M: ℝ} (hs: s.convergesTo L) (ht: t.convergesTo M) : (s - t).convergesTo (L - M) := s:Seriest:SeriesL:ℝM:ℝhs:s.convergesTo Lht:t.convergesTo M⊢ (s - t).convergesTo (L - M) All goals completed! 🐙theorem declaration uses 'sorry'Series.sub {s t:Series} (hs: s.converges) (ht: t.converges) : (s - t).converges ∧ (s-t).sum = s.sum - t.sum := s:Seriest:Serieshs:s.convergesht:t.converges⊢ (s - t).converges ∧ (s - t).sum = s.sum - t.sum All goals completed! 🐙abbrev Series.from (s:Series) (m₁:ℤ) : Series := mk' (m := max s.m m₁) (fun n ↦ s.seq (n:ℤ))

Твердження 7.2.14 (c) (Закони для рядів) / Вправа 7.2.5

theorem declaration uses 'sorry'Series.converges_from (s:Series) (k:ℕ) : s.converges ↔ (s.from (s.m+k)).converges := s:Seriesk:ℕ⊢ s.converges ↔ (s.from (s.m + ↑k)).converges All goals completed! 🐙
theorem declaration uses 'sorry'Series.sum_from {s:Series} (k:ℕ) (h: s.converges) : s.sum = ∑ n ∈ Finset.Ico s.m (s.m+k), s.seq n + (s.from (s.m+k)).sum := s:Seriesk:ℕh:s.converges⊢ s.sum = ∑ n ∈ Finset.Ico s.m (s.m + ↑k), s.seq n + (s.from (s.m + ↑k)).sum All goals completed! 🐙

Твердження 7.2.14 (d) (Закони для рядів) / Вправа 7.2.5

theorem declaration uses 'sorry'Series.shift {s:Series} {x:ℝ} (h: s.convergesTo x) (L:ℤ) : (mk' (m := s.m + L) (fun n ↦ s.seq (n - L))).convergesTo x := s:Seriesx:ℝh:s.convergesTo xL:ℤ⊢ (mk' fun n => s.seq (↑n - L)).convergesTo x All goals completed! 🐙

Лема 7.2.15 (Телескопічний ряд) / Вправа 7.2.6

theorem declaration uses 'sorry'Series.telescope {a:ℕ → ℝ} (ha: Filter.atTop.Tendsto a (nhds 0)) : ((fun n:ℕ ↦ a (n+1) - a n):Series).convergesTo (a 0) := a:ℕ → ℝha:Filter.Tendsto a Filter.atTop (nhds 0)⊢ { m := 0, seq := fun n => if n ≥ 0 then (fun n => a (n + 1) - a n) n.toNat else 0, vanish := ⋯ }.convergesTo (a 0) All goals completed! 🐙
/- Вправа 7.2.1 -/ def declaration uses 'sorry'Series.exercise_7_2_1_convergent : Decidable ((mk' (m := 1) (fun n ↦ (-1:ℝ)^(n:ℤ))).converges ) := ⊢ Decidable (mk' fun n => (-1) ^ ↑n).converges -- Перший рядок цього доказу має бути `apply isTrue` або `apply isFalse`. All goals completed! 🐙end Chapter7