Analysis I, Section 7.3: Sums of non-negative numbers

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

namespace Chapter7open Realabbrev Series.nonneg (s: Series) : Prop := n, s.seq n 0abbrev declaration uses 'sorry'Series.partial_of_nonneg {s: Series} (h: s.nonneg) : Monotone s.partial := s:Seriesh:s.nonnegMonotone s.partial All goals completed! 🐙

Proposition 7.3.1

theorem Series.converges_of_nonneg_iff {s: Series} (h: s.nonneg) : s.converges M, N, s.partial N M := s:Seriesh:s.nonnegs.converges M, (N : ), s.partial N M -- This broadly follows the argument in the text, though for one direction I choose to use Mathlib routines rather than Chapter6 results. s:Seriesh:s.nonnegs.converges M, (N : ), s.partial N Ms:Seriesh:s.nonneg(∃ M, (N : ), s.partial N M) s.converges s:Seriesh:s.nonnegs.converges M, (N : ), s.partial N M s:Seriesh:s.nonneghconv:s.converges M, (N : ), s.partial N M set S : Chapter6.Sequence := s.m, s.partial, s:Seriesh:s.nonneghconv:s.converges n < s.m, s.partial n = 0 s:Seriesh:s.nonneghconv:s.convergesn:hn:n < s.ms.partial n = 0; All goals completed! 🐙 have : S.IsBounded := s:Seriesh:s.nonnegs.converges M, (N : ), s.partial N M s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)S.Convergent s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) L, Filter.Tendsto S.seq Filter.atTop (nhds L) All goals completed! 🐙 s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hpos:M 0hM:S.BoundedBy M M, (N : ), s.partial N M s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hpos:M 0hM:S.BoundedBy M (N : ), s.partial N M; s:Seriesh:s.nonneghconv:s.convergesS:Chapter6.Sequence := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hpos:M 0hM✝:S.BoundedBy MN:hM:|S.seq N| Ms.partial N M All goals completed! 🐙 s:Seriesh:s.nonneghbound: M, (N : ), s.partial N Ms.converges s:Seriesh:s.nonneghbound: M, (N : ), s.partial N Mhinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTops.convergess:Seriesh:s.nonneghbound: M, (N : ), s.partial N Mhfin: l, Filter.Tendsto s.partial Filter.atTop (nhds l)s.converges s:Seriesh:s.nonneghbound: M, (N : ), s.partial N Mhinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTops.converges s:Seriesh:s.nonneghinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTopM:hM: (N : ), s.partial N Ms.converges s:Seriesh:s.nonneghinfin:Filter.Tendsto s.partial Filter.atTop Filter.atTopM:hM: (N : ), s.partial N MN:hN:M < s.partial Ns.converges All goals completed! 🐙 All goals completed! 🐙
theorem Series.sum_of_nonneg_lt {s: Series} (h: s.nonneg) {M:} (hM: N, s.partial N M) : s.sum M := s:Seriesh:s.nonnegM:hM: (N : ), s.partial N Ms.sum M have : M, N, s.partial N M := s:Seriesh:s.nonnegM:hM: (N : ), s.partial N Ms.sum M All goals completed! 🐙 s:Seriesh:s.nonnegM:hM: (N : ), s.partial N Mthis:s.convergess.sum M; s:Seriesh:s.nonnegM:hM: (N : ), s.partial N Mthis:s.convergesExists.choose M s:Seriesh:s.nonnegM:hM: (N : ), s.partial N Mthis:s.convergeshconv:?_mvar.6536 := Exists.choose_spec _fvar.5634Exists.choose M; s:Seriesh:s.nonnegM:hM: (N : ), s.partial N Mthis:s.convergeshconv:Filter.Tendsto (Chapter7.Series.partial _fvar.5571) Filter.atTop (nhds (Exists.choose _fvar.5634)) := Exists.choose_spec _fvar.5634Exists.choose M; All goals completed! 🐙theorem Series.partial_le_sum_of_nonneg {s: Series} (hnon: s.nonneg) (hconv: s.converges) (N : ) : s.partial N s.sum := s:Serieshnon:s.nonneghconv:s.convergesN:s.partial N s.sum s:Serieshnon:s.nonneghconv:s.convergesN:Filter.Tendsto s.partial Filter.atTop (nhds s.sum) s:Serieshnon:s.nonneghconv:s.convergesN:Filter.Tendsto s.partial Filter.atTop (nhds (Exists.choose )); All goals completed! 🐙

Some useful nonnegativity lemmas for later applications.

theorem Series.partial_nonneg {s: Series} (hnon: s.nonneg) (N : ) : 0 s.partial N := s:Serieshnon:s.nonnegN:0 s.partial N s:Serieshnon:s.nonnegN:0 n Finset.Icc s.m N, s.seq n; s:Serieshnon:s.nonnegN: i Finset.Icc s.m N, 0 s.seq i; All goals completed! 🐙
theorem Series.sum_of_nonneg {s:Series} (hnon: s.nonneg) : 0 s.sum := s:Serieshnon:s.nonneg0 s.sum s:Serieshnon:s.nonnegh:s.converges0 s.sums:Serieshnon:s.nonnegh:¬s.converges0 s.sum s:Serieshnon:s.nonnegh:s.converges0 s.sums:Serieshnon:s.nonnegh:¬s.converges0 s.sum All goals completed! 🐙 All goals completed! 🐙

Corollary 7.3.2 (Comparison test) / Exercise 7.3.1

theorem declaration uses 'sorry'Series.converges_of_le {s t: Series} (hm: s.m = t.m) (hcomp: n s.m, |s.seq n| t.seq n) (hconv : t.converges) : s.absConverges |s.sum| s.abs.sum s.abs.sum t.sum := s:Seriest:Serieshm:s.m = t.mhcomp: n s.m, |s.seq n| t.seq nhconv:t.convergess.absConverges |s.sum| s.abs.sum s.abs.sum t.sum All goals completed! 🐙
theorem declaration uses 'sorry'Series.diverges_of_ge {s t: Series} (hm: s.m = t.m) (hcomp: n s.m, |s.seq n| t.seq n) (hdiv: ¬ s.absConverges) : t.diverges := s:Seriest:Serieshm:s.m = t.mhcomp: n s.m, |s.seq n| t.seq nhdiv:¬s.absConvergest.diverges All goals completed! 🐙

Lemma 7.3.3 (Geometric series) / Exercise 7.3.2

theorem declaration uses 'sorry'Series.converges_geom {x: } (hx: |x| < 1) : (fun n x ^ n : Series).convergesTo (1 / (1 - x)) := x:hx:|x| < 1{ m := 0, seq := fun n => if n 0 then (fun n => x ^ n) n.toNat else 0, vanish := }.convergesTo (1 / (1 - x)) All goals completed! 🐙
theorem declaration uses 'sorry'Series.absConverges_geom {x: } (hx: |x| < 1) : (fun n x ^ n : Series).absConverges := x:hx:|x| < 1{ m := 0, seq := fun n => if n 0 then (fun n => x ^ n) n.toNat else 0, vanish := }.absConverges All goals completed! 🐙theorem declaration uses 'sorry'Series.diverges_geom {x: } (hx: |x| 1) : (fun n x ^ n : Series).diverges := x:hx:|x| 1{ m := 0, seq := fun n => if n 0 then (fun n => x ^ n) n.toNat else 0, vanish := }.diverges All goals completed! 🐙theorem declaration uses 'sorry'Series.converges_geom_iff (x: ) : (fun n x ^ n : Series).converges |x| < 1 := x:{ m := 0, seq := fun n => if n 0 then (fun n => x ^ n) n.toNat else 0, vanish := }.converges |x| < 1 All goals completed! 🐙

Proposition 7.3.4 (Cauchy criterion)

theorem Series.cauchy_criterion {s:Series} (hm: s.m = 1) (hs:s.nonneg) (hmono: n 1, s.seq (n+1) s.seq n) : s.converges (fun k 2^k * s.seq (2^k): Series).converges := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq ns.converges { m := 0, seq := fun n => if n 0 then (fun k => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := }.converges -- This proof is written to follow the structure of the original text. s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)s.converges t.converges have ht: t.nonneg := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq ns.converges { m := 0, seq := fun n => if n 0 then (fun k => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := }.converges s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)n:t.seq n 0; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)n:h:n 0t.seq n 0s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)n:h:¬n 0t.seq n 0 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)n:h:n 0t.seq n 0s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)n:h:¬n 0t.seq n 0 All goals completed! 🐙; All goals completed! 🐙 have hmono' : n 1, m n, s.seq m s.seq n := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq ns.converges { m := 0, seq := fun n => if n 0 then (fun k => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := }.converges s:Serieshm✝:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395n:hn:n 1m:hm:m ns.seq m s.seq n; s:Serieshm✝:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395n:hn:n 1k:hm:n + k ns.seq (n + k) s.seq n; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395n:hn:n 1k:s.seq (n + k) s.seq n s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395n:hn:n 1s.seq (n + 0) s.seq ns:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395n:hn:n 1k:hk:s.seq (n + k) s.seq ns.seq (n + (k + 1)) s.seq n; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395n:hn:n 1k:hk:s.seq (n + k) s.seq ns.seq (n + (k + 1)) s.seq n convert (hmono (n+k) (s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)n:hn:n 1k:hk:s.seq (n + k) s.seq nn + k 1 All goals completed! 🐙)).trans hk using 2; All goals completed! 🐙 have htm : t.m = 0 := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq ns.converges { m := 0, seq := fun n => if n 0 then (fun k => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := }.converges All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029(∃ M, (N : ), s.partial N M) M, (N : ), t.partial N M s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391(∃ M, (N : ), S N M) M, (N : ), t.partial N M s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328(∃ M, (N : ), S N M) M, (N : ), T N M have Lemma_7_3_6 (K:) : S (2^(K+1) - 1) T K T K 2 * S (2^K) := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq ns.converges { m := 0, seq := fun n => if n 0 then (fun k => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := }.converges s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328S (2 ^ (0 + 1) - 1) T 0 T 0 2 * S (2 ^ 0)s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:hK:S (2 ^ (K + 1) - 1) T K T K 2 * S (2 ^ K)S (2 ^ (K + 1 + 1) - 1) T (K + 1) T (K + 1) 2 * S (2 ^ (K + 1)) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328S (2 ^ (0 + 1) - 1) T 0 T 0 2 * S (2 ^ 0) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328s.seq 1 2 * s.seq 1; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:hK:S (2 ^ (K + 1) - 1) T K T K 2 * S (2 ^ K)h2K:1 2 ^ KS (2 ^ (K + 1 + 1) - 1) T (K + 1) T (K + 1) 2 * S (2 ^ (K + 1)); s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:hK:S (2 ^ (K + 1) - 1) T K T K 2 * S (2 ^ K)h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)S (2 ^ (K + 1 + 1) - 1) T (K + 1) T (K + 1) 2 * S (2 ^ (K + 1)) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)S (2 ^ (K + 1 + 1) - 1) T (K + 1) T (K + 1) 2 * S (2 ^ (K + 1)) have claim1 : T (K + 1) = T K + 2^(K+1) * s.seq (2^(K+1)) := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq ns.converges { m := 0, seq := fun n => if n 0 then (fun k => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := }.converges s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)K t.m - 1; All goals completed! 🐙 have claim2a : S (2^(K+1)) S (2^K) + 2^K * s.seq (2^(K+1)) := calc _ = S (2^K) + n .Ioc (2^K) (2^(K+1)), s.seq n := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)S (2 ^ (K + 1)) = S (2 ^ K) + n Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq n have : Disjoint (Finset.Icc s.m (2^K)) (Finset.Ioc (2^K) (2^(K+1))) := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)S (2 ^ (K + 1)) = S (2 ^ K) + n Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq n s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330) a Finset.Icc s.m (2 ^ K), b Finset.Ioc (2 ^ K) (2 ^ (K + 1)), a b; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)x:hx:x Finset.Icc s.m (2 ^ K)y:hy:y Finset.Ioc (2 ^ K) (2 ^ (K + 1))x y; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)x:y:hx:s.m x x 2 ^ Khy:2 ^ K < y y 2 ^ (K + 1)x y; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039Finset.Icc s.m (2 ^ (K + 1)) = Finset.Icc s.m (2 ^ K) Finset.Ioc (2 ^ K) (2 ^ (K + 1)) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:x Finset.Icc s.m (2 ^ (K + 1)) x Finset.Icc s.m (2 ^ K) Finset.Ioc (2 ^ K) (2 ^ (K + 1)); s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:s.m x x 2 ^ (K + 1) s.m x x 2 ^ K 2 ^ K < x x 2 ^ (K + 1); s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:s.m x x 2 ^ (K + 1) s.m x x 2 ^ K 2 ^ K < x x 2 ^ (K + 1)s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:s.m x x 2 ^ K 2 ^ K < x x 2 ^ (K + 1) s.m x x 2 ^ (K + 1) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:s.m x x 2 ^ (K + 1) s.m x x 2 ^ K 2 ^ K < x x 2 ^ (K + 1) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:h1:s.m xh2:x 2 ^ (K + 1)s.m x x 2 ^ K 2 ^ K < x x 2 ^ (K + 1); All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:h1:s.m xh2:x 2 ^ Ks.m x x 2 ^ (K + 1)s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:h1:2 ^ K < xh2:x 2 ^ (K + 1)s.m x x 2 ^ (K + 1) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:h1:s.m xh2:x 2 ^ Ks.m x x 2 ^ (K + 1) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:h1:s.m xh2:x 2 ^ Kx 2 * 2 ^ K; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.118039x:h1:2 ^ K < xh2:x 2 ^ (K + 1)1 x; All goals completed! 🐙 _ S (2^K) + n .Ioc ((2:)^K) (2^(K+1)), s.seq (2^(K+1)) := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)S (2 ^ K) + n Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq n S (2 ^ K) + n Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq (2 ^ (K + 1)) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)n:hn:n Finset.Ioc (2 ^ K) (2 ^ (K + 1))s.seq (2 ^ (K + 1)) s.seq n; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)n:hn:2 ^ K < n n 2 ^ (K + 1)s.seq (2 ^ (K + 1)) s.seq n; exact hmono' _ (s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)n:hn:2 ^ K < n n 2 ^ (K + 1)n 1 All goals completed! 🐙) _ hn.2 _ = _ := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)S (2 ^ K) + n Finset.Ioc (2 ^ K) (2 ^ (K + 1)), s.seq (2 ^ (K + 1)) = S (2 ^ K) + 2 ^ K * s.seq (2 ^ (K + 1)) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)(2 * 2 ^ K - 2 ^ K).toNat = 2 ^ K s.seq (2 * 2 ^ K) = 0; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)(2 * 2 ^ K - 2 ^ K).toNat = 2 ^ K; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)(2 ^ K).toNat = 2 ^ K; All goals completed! 🐙 have claim2 : 2 * S (2^(K+1)) 2 * S (2^K) + 2^(K+1) * s.seq (2^(K+1)) := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq ns.converges { m := 0, seq := fun n => if n 0 then (fun k => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := }.converges s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.109886claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.116563 ?_mvar.117032) ?_mvar.1171962 * S (2 ^ (K + 1)) 2 * S (2 ^ K) + 2 * 2 ^ K * s.seq (2 ^ (K + 1)); All goals completed! 🐙 have claim3 : S (2^(K+1+1) - 1) S (2^(K+1)-1) + 2^(K+1) * s.seq (2^(K+1)) := calc _ = S (2^(K+1)-1) + n .Icc (2^(K+1)) (2^(K+1+1)-1), s.seq n := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)S (2 ^ (K + 1 + 1) - 1) = S (2 ^ (K + 1) - 1) + n Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq n have : Disjoint (Finset.Icc s.m (2^(K+1)-1)) (Finset.Icc (2^(K+1)) (2^(K+1+1)-1)) := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)S (2 ^ (K + 1 + 1) - 1) = S (2 ^ (K + 1) - 1) + n Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq n s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) a Finset.Icc s.m (2 ^ (K + 1) - 1), b Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), a b; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)x:hx:x Finset.Icc s.m (2 ^ (K + 1) - 1)y:hy:y Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1)x y; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)x:y:hx:s.m x x 2 ^ (K + 1) - 1hy:2 ^ (K + 1) y y 2 ^ (K + 1 + 1) - 1x y; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930Finset.Icc s.m (2 ^ (K + 1 + 1) - 1) = Finset.Icc s.m (2 ^ (K + 1) - 1) Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:a✝ Finset.Icc s.m (2 ^ (K + 1 + 1) - 1) a✝ Finset.Icc s.m (2 ^ (K + 1) - 1) Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1); s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:s.m a✝ a✝ 2 ^ (K + 1 + 1) - 1 s.m a✝ a✝ 2 ^ (K + 1) - 1 2 ^ (K + 1) a✝ a✝ 2 ^ (K + 1 + 1) - 1; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:s.m a✝ a✝ 2 ^ (K + 1 + 1) - 1 s.m a✝ a✝ 2 ^ (K + 1) - 1 2 ^ (K + 1) a✝ a✝ 2 ^ (K + 1 + 1) - 1s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:s.m a✝ a✝ 2 ^ (K + 1) - 1 2 ^ (K + 1) a✝ a✝ 2 ^ (K + 1 + 1) - 1 s.m a✝ a✝ 2 ^ (K + 1 + 1) - 1 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:s.m a✝ a✝ 2 ^ (K + 1 + 1) - 1 s.m a✝ a✝ 2 ^ (K + 1) - 1 2 ^ (K + 1) a✝ a✝ 2 ^ (K + 1 + 1) - 1 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:h1:s.m a✝h2:a✝ 2 ^ (K + 1 + 1) - 1s.m a✝ a✝ 2 ^ (K + 1) - 1 2 ^ (K + 1) a✝ a✝ 2 ^ (K + 1 + 1) - 1; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:h1:s.m a✝h2:a✝ 2 ^ (K + 1 + 1) - 1a✝ 2 ^ (K + 1) - 1 2 ^ (K + 1) a✝; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:h1:s.m a✝h2:a✝ 2 ^ (K + 1) - 1s.m a✝ a✝ 2 ^ (K + 1 + 1) - 1s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:h1:2 ^ (K + 1) a✝h2:a✝ 2 ^ (K + 1 + 1) - 1s.m a✝ a✝ 2 ^ (K + 1 + 1) - 1 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:h1:s.m a✝h2:a✝ 2 ^ (K + 1) - 1s.m a✝ a✝ 2 ^ (K + 1 + 1) - 1 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:h1:s.m a✝h2:a✝ 2 ^ (K + 1) - 1a✝ 2 * 2 ^ (K + 1) - 1; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.188930a✝:h1:2 ^ (K + 1) a✝h2:a✝ 2 ^ (K + 1 + 1) - 11 a✝; All goals completed! 🐙 _ S (2^(K+1)-1) + n .Icc ((2:)^(K+1)) (2^(K+1+1)-1), s.seq (2^(K+1)) := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)S (2 ^ (K + 1) - 1) + n Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq n S (2 ^ (K + 1) - 1) + n Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq (2 ^ (K + 1)) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)n:hn:n Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1)s.seq n s.seq (2 ^ (K + 1)); s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)n:hn:2 ^ (K + 1) n n 2 ^ (K + 1 + 1) - 1s.seq n s.seq (2 ^ (K + 1)); s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)n:hn:2 ^ (K + 1) n n 2 ^ (K + 1 + 1) - 12 ^ (K + 1) 1; All goals completed! 🐙 _ = _ := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)S (2 ^ (K + 1) - 1) + n Finset.Icc (2 ^ (K + 1)) (2 ^ (K + 1 + 1) - 1), s.seq (2 ^ (K + 1)) = S (2 ^ (K + 1) - 1) + 2 ^ (K + 1) * s.seq (2 ^ (K + 1)) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)(2 * (2 * 2 ^ K) - 2 * 2 ^ K).toNat = 2 * 2 ^ K s.seq (2 * 2 ^ K) = 0; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)(2 * (2 * 2 ^ K) - 2 * 2 ^ K).toNat = 2 * 2 ^ K; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Chapter7.Series.partial_succ _fvar.22328 (Chapter7.Series.cauchy_criterion._proof_6 _fvar.21394 _fvar.22396 _fvar.30283 _fvar.40030 _fvar.40871 _fvar.108353 _fvar.109321 _fvar.109326 _fvar.109330)claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)(2 ^ K * 2).toNat = 2 ^ K * 2; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.109886claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.116563 ?_mvar.117032) ?_mvar.117196claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.178245claim3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.186554 ?_mvar.187315) ?_mvar.187746S (2 ^ (K + 1 + 1) - 1) T (K + 1) T (K + 1) 2 * S (2 ^ (K + 1)); s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.109886claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.116563 ?_mvar.117032) ?_mvar.117196claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.178245claim3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.186554 ?_mvar.187315) ?_mvar.187746S (2 ^ (K + 1 + 1) - 1) T (K + 1)s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.109886claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.116563 ?_mvar.117032) ?_mvar.117196claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.178245claim3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.186554 ?_mvar.187315) ?_mvar.187746T (K + 1) 2 * S (2 ^ (K + 1)) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.109886claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.116563 ?_mvar.117032) ?_mvar.117196claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.178245claim3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.186554 ?_mvar.187315) ?_mvar.187746S (2 ^ (K + 1 + 1) - 1) T (K + 1)s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328K:h2K:1 2 ^ Kh2K':1 2 ^ (K + 1)hK1:S (2 ^ (K + 1) - 1) T KhK2:T K 2 * S (2 ^ K)claim1:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.109886claim2a:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.116563 ?_mvar.117032) ?_mvar.117196claim2:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.178245claim3:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := Trans.trans (Trans.trans ?_mvar.186554 ?_mvar.187315) ?_mvar.187746T (K + 1) 2 * S (2 ^ (K + 1)) All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 K(∃ M, (N : ), S N M) M, (N : ), T N Ms:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 K(∃ M, (N : ), T N M) M, (N : ), S N M s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 K(∃ M, (N : ), S N M) M, (N : ), T N M s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N M M, (N : ), T N M; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N M (N : ), T N 2 * M; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N MN:T N 2 * M; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N MN:hN:N < 0T N 2 * Ms:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N MN:hN:0 NT N 2 * M s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N MN:hN:N < 0T N 2 * M s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N MN:hN:N < 00 M; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N MN:hN:N < 00 = S 0; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N MN:hN:0 NT N.toNat 2 * M; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), S N MN:hN:0 N2 * S (2 ^ N.toNat) 2 * M; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), T N M M, (N : ), S N M; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), T N M (N : ), S N M; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), T N MK':S K' M; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), T N MK':hK':K' < 1S K' Ms:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), T N MK':hK':1 K'S K' M s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), T N MK':hK':K' < 1S K' M s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), T N MK':hK':K' < 10 M; All goals completed! 🐙 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNatS K' M; have hK : K' = K + 1 := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq ns.converges { m := 0, seq := fun n => if n 0 then (fun k => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := }.converges s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := ?_mvar.22395hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.30282htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.40029S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := fun K => @?_mvar.40851 KM:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNatK' = K' - 1 + 1; All goals completed! 🐙 calc _ S (2 ^ (K+1) - 1) := s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNathK:_fvar.266718 = _fvar.270222 + 1 := Eq.mpr (id (congrArg (fun _a => _fvar.266718 = _a + 1) (Int.toNat_of_nonneg (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.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.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.266718 (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 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 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 (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (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_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ 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_zero (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_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.266718 (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 (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.266773)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) (Eq.trans (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (_fvar.266718 - 1) 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.unfold_sub _fvar.266718 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.subst_into_addg _fvar.266718 (-1) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Mathlib.Tactic.Abel.subst_into_negg 1 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_neg 1 1 0 (-1) 0 (Eq.refl (-1)) neg_zero)) (Mathlib.Tactic.Abel.term_add_constg 1 _fvar.266718 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 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) 0 (Eq.trans (Mathlib.Tactic.Abel.term_add_termg (-1) 1 0 1 0 0 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.negOfNat 1))) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.ofNat 0)))) (Eq.refl 0)) (zero_add 0)) (Mathlib.Tactic.Abel.zero_termg 1 0))))))S K' S (2 ^ (K + 1) - 1) s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNathK:_fvar.266718 = _fvar.270222 + 1 := Eq.mpr (id (congrArg (fun _a => _fvar.266718 = _a + 1) (Int.toNat_of_nonneg (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.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.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.266718 (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 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 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 (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (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_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ 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_zero (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_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.266718 (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 (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.266773)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) (Eq.trans (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (_fvar.266718 - 1) 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.unfold_sub _fvar.266718 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.subst_into_addg _fvar.266718 (-1) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Mathlib.Tactic.Abel.subst_into_negg 1 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_neg 1 1 0 (-1) 0 (Eq.refl (-1)) neg_zero)) (Mathlib.Tactic.Abel.term_add_constg 1 _fvar.266718 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 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) 0 (Eq.trans (Mathlib.Tactic.Abel.term_add_termg (-1) 1 0 1 0 0 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.negOfNat 1))) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.ofNat 0)))) (Eq.refl 0)) (zero_add 0)) (Mathlib.Tactic.Abel.zero_termg 1 0))))))K' 2 ^ (K + 1) - 1; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNathK:_fvar.266718 = _fvar.270222 + 1 := Eq.mpr (id (congrArg (fun _a => _fvar.266718 = _a + 1) (Int.toNat_of_nonneg (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.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.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.266718 (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 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 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 (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (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_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ 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_zero (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_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.266718 (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 (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.266773)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) (Eq.trans (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (_fvar.266718 - 1) 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.unfold_sub _fvar.266718 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.subst_into_addg _fvar.266718 (-1) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Mathlib.Tactic.Abel.subst_into_negg 1 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_neg 1 1 0 (-1) 0 (Eq.refl (-1)) neg_zero)) (Mathlib.Tactic.Abel.term_add_constg 1 _fvar.266718 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 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) 0 (Eq.trans (Mathlib.Tactic.Abel.term_add_termg (-1) 1 0 1 0 0 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.negOfNat 1))) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.ofNat 0)))) (Eq.refl 0)) (zero_add 0)) (Mathlib.Tactic.Abel.zero_termg 1 0))))))K + 1 2 ^ (K + 1) - 1 s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNathK:_fvar.266718 = _fvar.270222 + 1 := Eq.mpr (id (congrArg (fun _a => _fvar.266718 = _a + 1) (Int.toNat_of_nonneg (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.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.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.266718 (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 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 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 (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (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_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ 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_zero (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_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.266718 (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 (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.266773)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) (Eq.trans (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (_fvar.266718 - 1) 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.unfold_sub _fvar.266718 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.subst_into_addg _fvar.266718 (-1) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Mathlib.Tactic.Abel.subst_into_negg 1 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_neg 1 1 0 (-1) 0 (Eq.refl (-1)) neg_zero)) (Mathlib.Tactic.Abel.term_add_constg 1 _fvar.266718 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 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) 0 (Eq.trans (Mathlib.Tactic.Abel.term_add_termg (-1) 1 0 1 0 0 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.negOfNat 1))) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.ofNat 0)))) (Eq.refl 0)) (zero_add 0)) (Mathlib.Tactic.Abel.zero_termg 1 0))))))n:n + 1 2 ^ (n + 1) - 1; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNathK:_fvar.266718 = _fvar.270222 + 1 := Eq.mpr (id (congrArg (fun _a => _fvar.266718 = _a + 1) (Int.toNat_of_nonneg (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.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.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.266718 (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 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 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 (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (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_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ 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_zero (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_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.266718 (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 (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.266773)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) (Eq.trans (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (_fvar.266718 - 1) 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.unfold_sub _fvar.266718 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.subst_into_addg _fvar.266718 (-1) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Mathlib.Tactic.Abel.subst_into_negg 1 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_neg 1 1 0 (-1) 0 (Eq.refl (-1)) neg_zero)) (Mathlib.Tactic.Abel.term_add_constg 1 _fvar.266718 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 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) 0 (Eq.trans (Mathlib.Tactic.Abel.term_add_termg (-1) 1 0 1 0 0 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.negOfNat 1))) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.ofNat 0)))) (Eq.refl 0)) (zero_add 0)) (Mathlib.Tactic.Abel.zero_termg 1 0))))))0 + 1 2 ^ (0 + 1) - 1s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNathK:_fvar.266718 = _fvar.270222 + 1 := Eq.mpr (id (congrArg (fun _a => _fvar.266718 = _a + 1) (Int.toNat_of_nonneg (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.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.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.266718 (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 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 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 (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (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_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ 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_zero (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_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.266718 (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 (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.266773)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) (Eq.trans (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (_fvar.266718 - 1) 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.unfold_sub _fvar.266718 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.subst_into_addg _fvar.266718 (-1) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Mathlib.Tactic.Abel.subst_into_negg 1 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_neg 1 1 0 (-1) 0 (Eq.refl (-1)) neg_zero)) (Mathlib.Tactic.Abel.term_add_constg 1 _fvar.266718 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 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) 0 (Eq.trans (Mathlib.Tactic.Abel.term_add_termg (-1) 1 0 1 0 0 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.negOfNat 1))) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.ofNat 0)))) (Eq.refl 0)) (zero_add 0)) (Mathlib.Tactic.Abel.zero_termg 1 0))))))n:hn:n + 1 2 ^ (n + 1) - 1(n + 1) + 1 2 ^ (n + 1 + 1) - 1; s:Serieshm:s.m = 1hs:s.nonneghmono: n 1, s.seq (n + 1) s.seq nt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)hmono':failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328Lemma_7_3_6: (K : ), @_fvar.40146 (2 ^ (K + 1) - 1) @_fvar.40274 K @_fvar.40274 K 2 * @_fvar.40146 (2 ^ K) := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)M:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNathK:_fvar.266718 = _fvar.270222 + 1 := Eq.mpr (id (congrArg (fun _a => _fvar.266718 = _a + 1) (Int.toNat_of_nonneg (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.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.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.266718 (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 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 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 (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (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_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ 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_zero (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_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.266718 (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 (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.266773)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) (Eq.trans (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (_fvar.266718 - 1) 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.unfold_sub _fvar.266718 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.subst_into_addg _fvar.266718 (-1) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Mathlib.Tactic.Abel.subst_into_negg 1 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_neg 1 1 0 (-1) 0 (Eq.refl (-1)) neg_zero)) (Mathlib.Tactic.Abel.term_add_constg 1 _fvar.266718 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 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) 0 (Eq.trans (Mathlib.Tactic.Abel.term_add_termg (-1) 1 0 1 0 0 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.negOfNat 1))) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.ofNat 0)))) (Eq.refl 0)) (zero_add 0)) (Mathlib.Tactic.Abel.zero_termg 1 0))))))n:hn:n + 1 2 ^ (n + 1) - 1(n + 1) + 1 2 ^ (n + 1 + 1) - 1 s:Serieshm:s.m = 1hs:s.nonnegt:Chapter7.Series := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)ht:Chapter7.Series.nonneg _fvar.22328 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)htm:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := of_eq_true (eq_self 0)S: := Chapter7.Series.partial _fvar.21391T: := Chapter7.Series.partial _fvar.22328M:hM: (N : ), T N MK':hK':1 K'K: := (_fvar.266718 - 1).toNathK:_fvar.266718 = _fvar.270222 + 1 := Eq.mpr (id (congrArg (fun _a => _fvar.266718 = _a + 1) (Int.toNat_of_nonneg (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.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.sub_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul _fvar.266718 (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 1) (Mathlib.Tactic.Ring.add_pf_zero_add (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 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 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 (_fvar.266718 ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.atom_pf _fvar.266718) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Mathlib.Tactic.Ring.sub_pf (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_pf_add_gt (Int.negOfNat 1).rawCast (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ 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_zero (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_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (_fvar.266718 ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero _fvar.266718 (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 (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le _fvar.266773)) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr a)))))))) (Eq.trans (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Eq.symm (Mathlib.Tactic.Abel.subst_into_addg (_fvar.266718 - 1) 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.unfold_sub _fvar.266718 1 (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.subst_into_addg _fvar.266718 (-1) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0)) (Mathlib.Tactic.Abel.term_atomg _fvar.266718) (Mathlib.Tactic.Abel.subst_into_negg 1 (Mathlib.Tactic.Abel.termg 1 1 0) (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.term_atomg 1) (Mathlib.Tactic.Abel.term_neg 1 1 0 (-1) 0 (Eq.refl (-1)) neg_zero)) (Mathlib.Tactic.Abel.term_add_constg 1 _fvar.266718 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 _fvar.266718 (Mathlib.Tactic.Abel.termg (-1) 1 0) (Mathlib.Tactic.Abel.termg 1 1 0) 0 (Eq.trans (Mathlib.Tactic.Abel.term_add_termg (-1) 1 0 1 0 0 0 (Mathlib.Meta.NormNum.IsNat.to_eq (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.isInt_neg (Eq.refl Neg.neg) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.negOfNat 1))) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.isNat_ofNat (Eq.refl 1))) (Eq.refl (Int.ofNat 0)))) (Eq.refl 0)) (zero_add 0)) (Mathlib.Tactic.Abel.zero_termg 1 0))))))n:hmono: (n : ), 1 n s.seq (n + 1) s.seq nhmono': (n : ), 1 n (m : ), n m s.seq m s.seq nLemma_7_3_6: (K : ), S (2 ^ K * 2 - 1) T K T K 2 * S (2 ^ K)hn:n + 1 2 ^ n * 2 - 1n + 1 + 1 2 ^ n * 2 * 2 - 1; All goals completed! 🐙 _ T K := (Lemma_7_3_6 K).1 _ M := hM K

Corollary 7.3.7

theorem Series.converges_qseries (q: ) (hq: q > 0) : (mk' (m := 1) fun n 1 / (n:) ^ q : Series).converges (q>1) := q:hq:q > 0(mk' fun n => 1 / n ^ q).converges q > 1 -- This proof is written to follow the structure of the original text. q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140s.converges q > 1 have hs : s.nonneg := q:hq:q > 0(mk' fun n => 1 / n ^ q).converges q > 1 q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140n:s.seq n 0; q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140n:0 if 1 n then (n ^ q)⁻¹ else 0; q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140n:h:1 n0 if 1 n then (n ^ q)⁻¹ else 0q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140n:h:¬1 n0 if 1 n then (n ^ q)⁻¹ else 0 q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140n:h:1 n0 if 1 n then (n ^ q)⁻¹ else 0q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140n:h:¬1 n0 if 1 n then (n ^ q)⁻¹ else 0 All goals completed! 🐙; All goals completed! 🐙 have hmono : n 1, s.seq (n+1) s.seq n := q:hq:q > 0(mk' fun n => 1 / n ^ q).converges q > 1 q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1s.seq (n + 1) s.seq n have hn1 : n 0 := q:hq:q > 0(mk' fun n => 1 / n ^ q).converges q > 1 All goals completed! 🐙 have hn3 : n.toNat > 0 := q:hq:q > 0(mk' fun n => 1 / n ^ q).converges q > 1 All goals completed! 🐙 q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1hn1:_fvar.304325 0 := ?_mvar.304364hn3:Int.toNat _fvar.304325 > 0 := ?_mvar.305025((n + 1) ^ q)⁻¹ (n ^ q)⁻¹ q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1hn1:_fvar.304325 0 := ?_mvar.304364hn3:Int.toNat _fvar.304325 > 0 := ?_mvar.3050250 < n ^ qq:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1hn1:_fvar.304325 0 := ?_mvar.304364hn3:Int.toNat _fvar.304325 > 0 := ?_mvar.3050250 nq:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1hn1:_fvar.304325 0 := ?_mvar.304364hn3:Int.toNat _fvar.304325 > 0 := ?_mvar.305025n n + 1q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1hn1:_fvar.304325 0 := ?_mvar.304364hn3:Int.toNat _fvar.304325 > 0 := ?_mvar.3050250 q q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1hn1:_fvar.304325 0 := ?_mvar.304364hn3:Int.toNat _fvar.304325 > 0 := ?_mvar.3050250 < n ^ qq:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1hn1:_fvar.304325 0 := ?_mvar.304364hn3:Int.toNat _fvar.304325 > 0 := ?_mvar.3050250 nq:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1hn1:_fvar.304325 0 := ?_mvar.304364hn3:Int.toNat _fvar.304325 > 0 := ?_mvar.305025n n + 1q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209n:hn:n 1hn1:_fvar.304325 0 := ?_mvar.304364hn3:Int.toNat _fvar.304325 > 0 := ?_mvar.3050250 q try All goals completed! 🐙 All goals completed! 🐙 q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316{ m := 0, seq := fun n => if n 0 then (fun k => 2 ^ k * s.seq (2 ^ k)) n.toNat else 0, vanish := }.converges q > 1 have (n:) : 2^n * s.seq (2^n) = (2^(1-q))^n := q:hq:q > 0(mk' fun n => 1 / n ^ q).converges q > 1 have : 1 (2:)^n := q:hq:q > 0(mk' fun n => 1 / n ^ q).converges q > 1 q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:1 2 ^ n; All goals completed! 🐙 q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:this:1 2 ^ _fvar.316959 := ?_mvar.3174512 ^ n * ((2 ^ n) ^ q)⁻¹ = (2 ^ (1 - q)) ^ n q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:this:1 2 ^ _fvar.316959 := ?_mvar.317451(2 ^ n) ^ (-q + 1) = (2 ^ n) ^ (1 - q)q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:this:1 2 ^ _fvar.316959 := ?_mvar.3174510 2q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:this:1 2 ^ _fvar.316959 := ?_mvar.3174512 ^ n 0q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:this:1 2 ^ _fvar.316959 := ?_mvar.3174510 2 ^ n q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:this:1 2 ^ _fvar.316959 := ?_mvar.317451(2 ^ n) ^ (-q + 1) = (2 ^ n) ^ (1 - q)q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:this:1 2 ^ _fvar.316959 := ?_mvar.3174510 2q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:this:1 2 ^ _fvar.316959 := ?_mvar.3174512 ^ n 0q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316n:this:1 2 ^ _fvar.316959 := ?_mvar.3174510 2 ^ n (try All goals completed! 🐙); All goals completed! 🐙 q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := fun n => @?_mvar.317365 n|2 ^ (1 - q)| < 1 1 < q q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := fun n => @?_mvar.317365 n1 < 2 1 - q < 0 2 < 1 0 < 1 - q 1 < qq:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := fun n => @?_mvar.317365 n0 < 2q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := fun n => @?_mvar.317365 n0 2 ^ (1 - q) q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := fun n => @?_mvar.317365 n1 < 2 1 - q < 0 2 < 1 0 < 1 - q 1 < qq:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := fun n => @?_mvar.317365 n0 < 2q:hq:q > 0s:Chapter7.Series := Chapter7.Series.mk' fun n => 1 / n ^ _fvar.296140hs:Chapter7.Series.nonneg _fvar.297160 := ?_mvar.297209hmono:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.304316this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := fun n => @?_mvar.317365 n0 2 ^ (1 - q) try All goals completed! 🐙 All goals completed! 🐙

Remark 7.3.8

theorem Series.zeta_eq {q:} (hq: q > 1) : (mk' (m := 1) fun n 1 / (n:) ^ q : Series).sum = riemannZeta q := q:hq:q > 1(mk' fun n => 1 / n ^ q).sum = riemannZeta q -- `riemannZeta` is defined over the complex numbers, so some preliminary work is needed to specialize to the reals. q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028(mk' fun n => 1 / n ^ q).sum = riemannZeta q have hL : L = riemannZeta q := q:hq:q > 1(mk' fun n => 1 / n ^ q).sum = riemannZeta q q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028L = ∑' (n : ), 1 / (n + 1) ^ q q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028n:1 / (n + 1) ^ q = (1 / (n + 1) ^ q) All goals completed! 🐙 q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259(mk' fun n => 1 / n ^ q).sum = L q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259(mk' fun n => 1 / n ^ q).sum = L; q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259(mk' fun n => 1 / n ^ q).convergesTo L have : Summable (fun (n : ) 1 / (n+1:) ^ q) := q:hq:q > 1(mk' fun n => 1 / n ^ q).sum = riemannZeta q q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259n:n + 1 = |n + 1| q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259n:0 n + 1; All goals completed! 🐙 have tail (a: ) (L:) : Filter.atTop.Tendsto a (nhds L) Filter.atTop.Tendsto (fun n: a n) (nhds L) := q:hq:q > 1(mk' fun n => 1 / n ^ q).sum = riemannZeta q q:hq:q > 1L✝: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240a: L:Filter.atTop = Filter.map (fun n => n) Filter.atTop All goals completed! 🐙 q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a LFilter.Tendsto (mk' fun n => 1 / n ^ q).partial Filter.atTop (nhds L) q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a LFilter.Tendsto (fun n => (mk' fun n => 1 / n ^ q).partial n) Filter.atTop (nhds L) q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:(mk' fun n => 1 / n ^ q).partial n = i Finset.range n, 1 / (i + 1) ^ q q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:(∑ x Finset.Icc 1 n, if 1 x then (x ^ q)⁻¹ else 0) = x Finset.range n, ((x + 1) ^ q)⁻¹ set e : := { toFun n := n+1 inj' _ _ _ := q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := Eq.mpr (id (congrArg (fun _a => _fvar.334370 = _a) (zeta_eq_tsum_one_div_nat_add_one_cpow (Eq.mpr (id (Eq.trans (congrArg (fun x => x < (↑_fvar.334028).re) (Eq.symm Nat.cast_one)) (congrArg (fun x => x < _fvar.334028) Nat.cast_one))) _fvar.334029)))) (Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 e'_2 x (a = a_1) (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => (e_2 : a = a'), e_2 Eq.refl a (a = a_1) (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 e'_3 x (a = a_1) (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => (e_3 : a_1 = a'), e_3 Eq.refl a_1 (a = a_1) (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) (↑_fvar.334370) (↑(∑' (a : ), 1 / (a + 1) ^ _fvar.334028)) (Eq.refl _fvar.334370) (∑' (n : ), 1 / (n + 1) ^ _fvar.334028) (∑' (a : ), (1 / (a + 1) ^ _fvar.334028)) (eq_of_heq ((fun α inst inst_1 β f f' e'_5 => Eq.casesOn (motive := fun a x => f' = a e'_5 x tsum f tsum f') e'_5 (fun h => Eq.ndrec (motive := fun f' => (e_5 : f = f'), e_5 Eq.refl f tsum f tsum f') (fun e_5 h => HEq.refl (tsum f)) (Eq.symm h) e'_5) (Eq.refl f') (HEq.refl e'_5)) NormedAddCommGroup.toENormedAddCommMonoid.toAddCommMonoid PseudoMetricSpace.toUniformSpace.toTopologicalSpace (fun n => 1 / (n + 1) ^ _fvar.334028) (fun a => (1 / (a + 1) ^ _fvar.334028)) (funext fun n => of_eq_true (Eq.trans (congr (congrArg Eq (one_div ((n + 1) ^ _fvar.334028))) (Eq.trans (Eq.trans (congrArg Complex.ofReal (one_div ((n + 1) ^ _fvar.334028))) (Complex.ofReal_inv ((n + 1) ^ _fvar.334028))) (congrArg Inv.inv (Eq.trans ((fun x_0 => (fun x_0 => Complex.ofReal_cpow (le_of_lt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n) (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl (Nat.ble 1 1))))) x_0) x_0) _fvar.334028) (congrArg (fun x => x ^ _fvar.334028) (Complex.ofReal_add (↑n) 1)))))) (eq_self ((n + 1) ^ _fvar.334028)⁻¹))))))) (Complex.ofReal_tsum fun n => 1 / (n + 1) ^ _fvar.334028))this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := Eq.mpr (eq_of_heq ((fun α β inst inst_1 f f' e'_5 => Eq.casesOn (motive := fun a x => f' = a e'_5 x Summable f Summable f') e'_5 (fun h => Eq.ndrec (motive := fun f' => (e_5 : f = f'), e_5 Eq.refl f Summable f Summable f') (fun e_5 h => HEq.refl (Summable f)) (Eq.symm h) e'_5) (Eq.refl f') (HEq.refl e'_5)) Real.instAddCommMonoid PseudoMetricSpace.toUniformSpace.toTopologicalSpace (fun n => 1 / (n + 1) ^ _fvar.334028) (fun n => 1 / |n + 1| ^ _fvar.334028) (funext fun n => eq_of_heq ((fun α β γ self a a_1 a' e'_6 => Eq.casesOn (motive := fun a_2 x => a' = a_2 e'_6 x a / a_1 a / a') e'_6 (fun h => Eq.ndrec (motive := fun a' => (e_6 : a_1 = a'), e_6 Eq.refl a_1 a / a_1 a / a') (fun e_6 h => HEq.refl (a / a_1)) (Eq.symm h) e'_6) (Eq.refl a') (HEq.refl e'_6)) instHDiv 1 ((n + 1) ^ _fvar.334028) (|n + 1| ^ _fvar.334028) (eq_of_heq ((fun α β γ self a a' e'_5 a_1 => Eq.casesOn (motive := fun a_2 x => a' = a_2 e'_5 x a ^ a_1 a' ^ a_1) e'_5 (fun h => Eq.ndrec (motive := fun a' => (e_5 : a = a'), e_5 Eq.refl a a ^ a_1 a' ^ a_1) (fun e_5 h => HEq.refl (a ^ a_1)) (Eq.symm h) e'_5) (Eq.refl a') (HEq.refl e'_5)) instHPow (n + 1) |n + 1| (Eq.mpr (id (congrArg (fun _a => n + 1 = _a) (abs_of_nonneg (le_of_lt (Right.add_pos_of_nonneg_of_pos (Nat.cast_nonneg' n) (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one) (Eq.refl (Nat.ble 1 1)))))))) (Eq.refl (n + 1))) _fvar.334028)))))) ((Real.summable_one_div_nat_add_rpow 1 _fvar.334028).mpr _fvar.334029)tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => Eq.mpr (eq_of_heq ((fun a a' e'_1 b b' e'_2 => Eq.casesOn (motive := fun a_1 x => a' = a_1 e'_1 x (a b) (a' b')) e'_1 (fun h => Eq.ndrec (motive := fun a' => (e_1 : a = a'), e_1 Eq.refl a (a b) (a' b')) (fun e_1 h => Eq.casesOn (motive := fun a_1 x => b' = a_1 e'_2 x (a b) (a b')) e'_2 (fun h => Eq.ndrec (motive := fun b' => (e_2 : b = b'), e_2 Eq.refl b (a b) (a b')) (fun e_2 h => HEq.refl (a b)) (Eq.symm h) e'_2) (Eq.refl b') (HEq.refl e'_2)) (Eq.symm h) e'_1) (Eq.refl a') (HEq.refl e'_1)) (Filter.Tendsto a Filter.atTop (nhds L)) (Filter.Tendsto a (Filter.map (fun n => n) Filter.atTop) (nhds L)) (eq_of_heq ((fun α β f f' e'_3 l₁ l₁' e'_4 l₂ l₂' e'_5 => Eq.casesOn (motive := fun a x => f' = a e'_3 x Filter.Tendsto f l₁ l₂ Filter.Tendsto f' l₁' l₂') e'_3 (fun h => Eq.ndrec (motive := fun f' => (e_3 : f = f'), e_3 Eq.refl f Filter.Tendsto f l₁ l₂ Filter.Tendsto f' l₁' l₂') (fun e_3 h => Eq.casesOn (motive := fun a x => l₁' = a e'_4 x Filter.Tendsto f l₁ l₂ Filter.Tendsto f l₁' l₂') e'_4 (fun h => Eq.ndrec (motive := fun l₁' => (e_4 : l₁ = l₁'), e_4 Eq.refl l₁ Filter.Tendsto f l₁ l₂ Filter.Tendsto f l₁' l₂') (fun e_4 h => Eq.casesOn (motive := fun a x => l₂' = a e'_5 x Filter.Tendsto f l₁ l₂ Filter.Tendsto f l₁ l₂') e'_5 (fun h => Eq.ndrec (motive := fun l₂' => (e_5 : l₂ = l₂'), e_5 Eq.refl l₂ Filter.Tendsto f l₁ l₂ Filter.Tendsto f l₁ l₂') (fun e_5 h => HEq.refl (Filter.Tendsto f l₁ l₂)) (Eq.symm h) e'_5) (Eq.refl l₂') (HEq.refl e'_5)) (Eq.symm h) e'_4) (Eq.refl l₁') (HEq.refl e'_4)) (Eq.symm h) e'_3) (Eq.refl f') (HEq.refl e'_3)) a a (Eq.refl a) Filter.atTop (Filter.map (fun n => n) Filter.atTop) (of_eq_true (Eq.trans (congrArg (Eq Filter.atTop) Nat.map_cast_int_atTop) (eq_self Filter.atTop))) (nhds L) (nhds L) (Eq.refl (nhds L)))) (Filter.Tendsto (fun n => a n) Filter.atTop (nhds L)) (Filter.Tendsto (a fun n => n) Filter.atTop (nhds L)) (eq_of_heq ((fun α β f f' e'_3 l₁ l₁' e'_4 l₂ => Eq.casesOn (motive := fun a x => f' = a e'_3 x Filter.Tendsto f l₁ l₂ Filter.Tendsto f' l₁' l₂) e'_3 (fun h => Eq.ndrec (motive := fun f' => (e_3 : f = f'), e_3 Eq.refl f Filter.Tendsto f l₁ l₂ Filter.Tendsto f' l₁' l₂) (fun e_3 h => Eq.casesOn (motive := fun a x => l₁' = a e'_4 x Filter.Tendsto f l₁ l₂ Filter.Tendsto f l₁' l₂) e'_4 (fun h => Eq.ndrec (motive := fun l₁' => (e_4 : l₁ = l₁'), e_4 Eq.refl l₁ Filter.Tendsto f l₁ l₂ Filter.Tendsto f l₁' l₂) (fun e_4 h => HEq.refl (Filter.Tendsto f l₁ l₂)) (Eq.symm h) e'_4) (Eq.refl l₁') (HEq.refl e'_4)) (Eq.symm h) e'_3) (Eq.refl f') (HEq.refl e'_3)) (fun n => a n) (a fun n => n) (funext fun x => Eq.refl (a x)) Filter.atTop Filter.atTop (Eq.refl Filter.atTop) (nhds L))))) Filter.tendsto_map'_iffn:x✝²:x✝¹:x✝:(fun n => n + 1) x✝² = (fun n => n + 1) x✝¹x✝² = x✝¹ All goals completed! 🐙 } q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }Finset.Icc 1 n = Finset.map e (Finset.range n)q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }m:hm:m Finset.range n((m + 1) ^ q)⁻¹ = if 1 e m then ((e m) ^ q)⁻¹ else 0 q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }Finset.Icc 1 n = Finset.map e (Finset.range n) q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }x:x Finset.Icc 1 n x Finset.map e (Finset.range n); q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }x:1 x x n a < n, a + 1 = x; q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }x:1 x x n a < n, a + 1 = xq:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }x:(∃ a < n, a + 1 = x) 1 x x n q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }x:1 x x n a < n, a + 1 = x q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }x:left✝:1 xright✝:x n a < n, a + 1 = x; q:hq:q > 1L: := ∑' (n : ), 1 / (n + 1) ^ _fvar.334028hL:_fvar.334370 = riemannZeta _fvar.334028 := ?_mvar.335259this:Summable fun n => 1 / (n + 1) ^ _fvar.334028 := ?_mvar.340240tail: (a : ) (L : ), Filter.Tendsto a Filter.atTop (nhds L) Filter.Tendsto (fun n => a n) Filter.atTop (nhds L) := fun a L => @?_mvar.343975 a Ln:e: := { toFun := fun n => n + 1, inj' := }x:left✝:1 xright✝:x n(x - 1).toNat < n (x - 1).toNat + 1 = x; All goals completed! 🐙 All goals completed! 🐙 All goals completed! 🐙
theorem Series.Basel_problem : (mk' (m := 1) fun n 1 / (n:) ^ 2 : Series).sum = Real.pi ^ 2 / 6 := (mk' fun n => 1 / n ^ 2).sum = π ^ 2 / 6 have := zeta_eq (show 2 > 1 (mk' fun n => 1 / n ^ 2).sum = π ^ 2 / 6 All goals completed! 🐙) this:(mk' fun n => (n ^ 2)⁻¹).sum = π ^ 2 / 6(mk' fun n => 1 / n ^ 2).sum = π ^ 2 / 6 All goals completed! 🐙

Exercise 7.3.3

theorem declaration uses 'sorry'Series.nonneg_sum_zero {a: } (ha: (a:Series).nonneg) (hconv: (a:Series).converges) : (a:Series).sum = 0 n, a n = 0 := a: ha:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.nonneghconv:{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.converges{ m := 0, seq := fun n => if n 0 then a n.toNat else 0, vanish := }.sum = 0 (n : ), a n = 0 All goals completed! 🐙
end Chapter7