Imports
import Mathlib.Tactic import Analysis.Section_7_3

Analysis I, Section 7.4: Rearrangement of series

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:

  • Rearrangement of non-negative or absolutely convergent series.

namespace Chapter7theorem Series.sum_eq_sum (b: ) {N:} (hN: N 0) : n .Icc 0 N, (if 0 n then b n.toNat else 0) = n .Iic N.toNat, b n := b: N:hN:N 0(∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n convert Finset.sum_image (g := Int.ofNat) (b: N:hN:N 0Set.InjOn Int.ofNat ?m.42 All goals completed! 🐙) b: N:hN:N 0x:x Finset.Icc 0 N x Finset.image Int.ofNat (Finset.Iic N.toNat); b: N:hN:N 0x:0 x x N a N.toNat, a = x; b: N:hN:N 0x:0 x x N a N.toNat, a = xb: N:hN:N 0x:(∃ a N.toNat, a = x) 0 x x N b: N:hN:N 0x:0 x x N a N.toNat, a = x b: N:hN:N 0x:left✝:0 xright✝:x N a N.toNat, a = x; b: N:hN:N 0x:left✝:0 xright✝:x Nx.toNat N.toNat x.toNat = x; All goals completed! 🐙 All goals completed! 🐙

Proposition 7.4.1

theorem Series.converges_of_permute_nonneg {a: } (ha: (a:Series).nonneg) (hconv: (a:Series).converges) {f: } (hf: Function.Bijective f) : (fun n a (f n) : Series).converges (a:Series).sum = (fun n a (f n) : Series).sum := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum -- This proof is written to follow the structure of the original text. 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n){ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum have haf : (af:Series).nonneg := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)n:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.seq 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)n:h:n 0{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.seq n 0a: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)n:h:¬n 0{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.seq 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)n:h:n 0{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.seq n 0a: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)n:h:¬n 0{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.seq n 0 All goals completed! 🐙 a: hconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)n:h:n 0ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.seq (f n.toNat) 00 a (f n.toNat); All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partial{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone S{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone T{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup S{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup T{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Q{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.suma: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Q(∃ Q, (M : ), T M Q) L = L' 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum have Ssum : L = (a:Series).sum := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = L; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesTo L; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Filter.Tendsto { m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.partial Filter.atTop (nhds (iSup S)) 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'(Set.range S).Nonemptya: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'BddAbove (Set.range S) 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'(Set.range S).Nonempty 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'S 0 Set.range S; All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup Tthis:(∃ Q, (M : ), T M Q) L = L'Q:hQ: (N : ), S N QBddAbove (Set.range S); 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup Tthis:(∃ Q, (M : ), T M Q) L = L'Q:hQ: (N : ), S N QQ upperBounds (Set.range S); All goals completed! 🐙 have Tsum : L' = (af:Series).sum := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum = L'; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L'; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumFilter.Tendsto { m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial Filter.atTop (nhds (iSup T)) 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum(Set.range T).Nonemptya: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumBddAbove (Set.range T) 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum(Set.range T).Nonempty 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumT 0 Set.range T; All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumQ:hQ: (M : ), T M QBddAbove (Set.range T); 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumQ:hQ: (M : ), T M QQ upperBounds (Set.range T); All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N Qthis:(∃ Q, (M : ), T M Q) L = L'Ssum:L = { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumTsum:L' = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum M, (N : ), { m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial N M All goals completed! 🐙 have hTL (M:) : T M L := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0T M La: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0T M L 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0T M La: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0T M L 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0T M L have hM' : M < 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0hM':M < 00 L 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:¬M 0hM':M < 0BddAbove (Set.range S) All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatT M L have hN : N, m Y, f m N := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNat m Y, f m (Finset.image f Y).sup id; intro m 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatm:hm:m Yf m (Finset.image f Y).sup id 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatm:hm:m Yf m Finset.image f Y; All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NT M L calc _ = m Y, af m := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NT M = m Y, af m 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(∑ n Finset.Icc 0 M, if 0 n then a (f n.toNat) else 0) = n Y, a (f n); All goals completed! 🐙 _ = n f '' Y, a n := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N m Y, af m = n (f '' Y).toFinset, a n 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N n (f '' Y).toFinset, a n = m Y, af m; convert Finset.sum_image (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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NSet.InjOn ?m.439 ?m.438 All goals completed! 🐙); All goals completed! 🐙 _ n .Iic N, a n := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N n (f '' Y).toFinset, a n n Finset.Iic N, a n 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(f '' Y).toFinset Finset.Iic Na: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N i Finset.Iic N, i (f '' Y).toFinset 0 a i 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(f '' Y).toFinset Finset.Iic N intro _ 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Na✝¹:a✝:a✝¹ (f '' Y).toFinseta✝¹ Finset.Iic N; All goals completed! 🐙 intro i 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Ni:a✝:i Finset.Iic Ni (f '' Y).toFinset 0 a i 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Ni:a✝¹:i Finset.Iic Na✝:i (f '' Y).toFinset0 a i; a: hconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m Ni:a✝¹:i Finset.Iic Na✝:i (f '' Y).toFinsetha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.seq i 00 a i; All goals completed! 🐙 _ = S N := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N n Finset.Iic N, a n = S N 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N n Finset.Iic N, a n = n Finset.Icc 0 N, if 0 n then a n.toNat else 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m N(∑ n Finset.Icc 0 N, if 0 n then a n.toNat else 0) = n Finset.Iic N, a n; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NN 0; All goals completed! 🐙 _ L := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NS N L 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QM:hM:M 0Y:Finset := Finset.Iic M.toNatN:hN: m Y, f m NBddAbove (Set.range S); All goals completed! 🐙 have hTbound : Q, M, T M Q := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QL = L' have hSL' (N:) : S N L' := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N 0S N L'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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:¬N 0S N L' 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:¬N 0S N L'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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N 0S N L' 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:¬N 0S N L' have hN' : 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:¬N 0hN':N < 00 L' 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:¬N 0hN':N < 0BddAbove (Set.range T) All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N 0X:Finset := Finset.Iic N.toNatS N L' have hM : M, n X, m, f m = n m M := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N 0X:Finset := Finset.Iic N.toNat n X, m, f m = n m (X.preimage f ).sup id intro n 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N 0X:Finset := Finset.Iic N.toNatn:hn:n X m, f m = n m (X.preimage f ).sup id; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N 0X:Finset := Finset.Iic N.toNatn:hn:n Xm:hm:f m = n m, f m = n m (X.preimage f ).sup id 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N 0X:Finset := Finset.Iic N.toNatn:hn:n Xm:hm:f m = nm (X.preimage f ).sup id 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N 0X:Finset := Finset.Iic N.toNatn:hn:n Xm:hm:f m = nm X.preimage f All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m MS N L' have sum_eq_sum (b: ) {N:} (hN: N 0) : n .Icc 0 N, (if 0 n then b n.toNat else 0) = n .Iic N.toNat, b n := 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 := }.convergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.converges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum convert Finset.sum_image (g := Int.ofNat) (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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN✝:hN✝:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0Set.InjOn Int.ofNat ?m.926 All goals completed! 🐙) 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN✝:hN✝:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:x Finset.Icc 0 N x Finset.image Int.ofNat (Finset.Iic N.toNat); 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN✝:hN✝:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:0 x x N a N.toNat, a = x; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN✝:hN✝:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:0 x x N a N.toNat, a = xa: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN✝:hN✝:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:(∃ a N.toNat, a = x) 0 x x N 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN✝:hN✝:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:0 x x N a N.toNat, a = x 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN✝:hN✝:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:left✝:0 xright✝:x N a N.toNat, a = x; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN✝:hN✝:N 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Mb: N:hN:N 0x:left✝:0 xright✝:x Nx.toNat N.toNat x.toNat = x; All goals completed! 🐙 All goals completed! 🐙 calc _ = n X, a n := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nS N = n X, a n All goals completed! 🐙 _ = n ((Finset.Iic M).filter (f · X)).image f, a n := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n n X, a n = n Finset.image f ({x Finset.Iic M | f x X}), a n 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nX = Finset.image f ({x Finset.Iic M | f x X}); 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b na✝:a✝ X a✝ Finset.image f ({x Finset.Iic M | f x X}); 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b na✝:a✝ X a, (a M f a X) f a = a✝; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b na✝:a✝ X a, (a M f a X) f a = a✝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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b na✝:(∃ a, (a M f a X) f a = a✝) a✝ X 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b na✝:a✝ X a, (a M f a X) f a = a✝ 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b na✝:h:a✝ X a, (a M f a X) f a = a✝; 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nm:hm':m Mh:f m X a, (a M f a X) f a = f m; All goals completed! 🐙 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nw✝:left✝:w✝ Mright✝:f w✝ Xf w✝ X; All goals completed! 🐙 _ m .Iic M, af m := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n n Finset.image f ({x Finset.Iic M | f x X}), a n m Finset.Iic M, af m 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n x Finset.Iic M with f x X, a (f x) m Finset.Iic M, af m 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n{x Finset.Iic M | f x X} Finset.Iic Ma: 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n i Finset.Iic M, i {x Finset.Iic M | f x X} 0 a (f i) 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n{x Finset.Iic M | f x X} Finset.Iic M All goals completed! 🐙 intro i 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b ni:a✝:i Finset.Iic Mi {x Finset.Iic M | f x X} 0 a (f i) 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b ni:a✝¹:i Finset.Iic Ma✝:i {x Finset.Iic M | f x X}0 a (f i); 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)S: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b ni:a✝¹:i Finset.Iic Ma✝:i {x Finset.Iic M | f x X}haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.seq i 00 a (f i); All goals completed! 🐙 _ = T M := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n m Finset.Iic M, af m = T M 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n n Finset.Iic M, a (f n) = n Finset.Icc 0 M, if 0 n then a (f n.toNat) else 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b n(∑ n Finset.Icc 0 M, if 0 n then a (f n.toNat) else 0) = n Finset.Iic M, a (f n); 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nM 0; All goals completed! 🐙 _ L' := 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nT M L' 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 := }.convergesf: hf:Function.Bijective faf: := fun n a (f n)haf:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.nonnegS: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partialT: := { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partialhSmono:Monotone ShTmono:Monotone TL: := iSup SL': := iSup ThSBound: Q, (N : ), S N QhTL: (M : ), T M LhTbound: Q, (M : ), T M QN:hN:N✝ 0X:Finset := Finset.Iic N.toNatM:hM: n X, m, f m = n m Msum_eq_sum: (b : ) {N : }, N 0 (∑ n Finset.Icc 0 N, if 0 n then b n.toNat else 0) = n Finset.Iic N.toNat, b nBddAbove (Set.range T); All goals completed! 🐙 All goals completed! 🐙

Example 7.4.2

theorem declaration uses `sorry`Series.zeta_2_converges : (fun n: 1/(n+1:)^2 : Series).converges := { m := 0, seq := fun n if n 0 then (fun n 1 / (n + 1) ^ 2) n.toNat else 0, vanish := }.converges All goals completed! 🐙
theorem declaration uses `sorry`Series.permuted_zeta_2_converges : (fun n: if Even n then 1/(n+2:)^2 else 1/(n:)^2 : Series).converges := { m := 0, seq := fun n if n 0 then (fun n if Even n then 1 / (n + 2) ^ 2 else 1 / n ^ 2) n.toNat else 0, vanish := }.converges All goals completed! 🐙theorem declaration uses `sorry`Series.permuted_zeta_2_eq_zeta_2 : (fun n: if Even n then 1/(n+2:)^2 else 1/(n:)^2 : Series).sum = (fun n: 1/(n+1:)^2 : Series).sum := { m := 0, seq := fun n if n 0 then (fun n if Even n then 1 / (n + 2) ^ 2 else 1 / n ^ 2) n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n 1 / (n + 1) ^ 2) n.toNat else 0, vanish := }.sum All goals completed! 🐙

Proposition 7.4.3 (Rearrangement of series)

theorem declaration uses `sorry`Series.absConverges_of_permute {a: } (ha : (a:Series).absConverges) {f: } (hf: Function.Bijective f) : (fun n a (f n):Series).absConverges (a:Series).sum = (fun n a (f n) : Series).sum := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum -- This proof is written to follow the structure of the original text. a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sum{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ 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 (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ 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 (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum have habs : (fun n |a (f n)| : Series).converges L = (fun n |a (f n)| : Series).sum := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ 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 := }.abs = { m := 0, seq := fun n if n 0 then |a n.toNat| else 0, vanish := }a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ 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 (fun n |a n|) n.toNat else 0, vanish := }.nonnega: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ 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 (fun n |a n|) n.toNat else 0, vanish := }.converges a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ 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 := }.abs = { m := 0, seq := fun n if n 0 then |a n.toNat| else 0, vanish := } a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.converges(fun n if 0 n then |if 0 n then a n.toNat else 0| else 0) = fun n if 0 n then |a n.toNat| else 0; a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0; a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h✝:n 0(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h✝:¬n 0(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h✝:n 0(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h✝:¬n 0(if 0 n then |if 0 n then a n.toNat else 0| else 0) = if 0 n then |a n.toNat| else 0 All goals completed! 🐙 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ 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 (fun n |a n|) n.toNat else 0, vanish := }.nonneg a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:{ m := 0, seq := fun n if n 0 then (fun n |a n|) n.toNat else 0, vanish := }.seq n 0; a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h:n 0{ m := 0, seq := fun n if n 0 then (fun n |a n|) n.toNat else 0, vanish := }.seq n 0a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h:¬n 0{ m := 0, seq := fun n if n 0 then (fun n |a n|) n.toNat else 0, vanish := }.seq n 0 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h:n 0{ m := 0, seq := fun n if n 0 then (fun n |a n|) n.toNat else 0, vanish := }.seq n 0a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h:¬n 0{ m := 0, seq := fun n if n 0 then (fun n |a n|) n.toNat else 0, vanish := }.seq n 0 All goals completed! 🐙 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:(if n 0 then (fun n |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0; a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h✝:n 0(if n 0 then (fun n |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h✝:¬n 0(if n 0 then (fun n |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h✝:n 0(if n 0 then (fun n |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesn:h✝:¬n 0(if n 0 then (fun n |a n|) n.toNat else 0) = if h : n { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.seq n|) n, h else 0 All goals completed! 🐙 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges L' = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n){ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.absConverges L' = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)this:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L'{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.absConverges L' = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.suma: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n){ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L' a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)this:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L'{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.absConverges L' = { m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.sum a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)this:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L'{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.abs.converges a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)this:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:(if h : n { m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n |a (f n)|) n.toNat else 0; a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)this:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:h✝:n 0(if h : n { m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n |a (f n)|) n.toNat else 0a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)this:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:h✝:¬n 0(if h : n { m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n |a (f n)|) n.toNat else 0 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)this:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:h✝:n 0(if h : n { m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n |a (f n)|) n.toNat else 0a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)this:{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.convergesTo L'n:h✝:¬n 0(if h : n { m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.m then (fun n |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.seq n|) n, h else 0) = if n 0 then (fun n |a (f n)|) n.toNat else 0 All goals completed! 🐙 a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n) (ε : ), 0 < ε a, (b : ), a b |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε intro ε a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.convergesf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < ε a, (b : ), a b |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε a: ha: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < ε a, (b : ), a b |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:hN₁:N₁ { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.mha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2 a, (b : ), a b |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε; a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁ a, (b : ), a b |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε have : N N₁, |(a:Series).partial N - L'| < ε/2 := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁hconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergesTo { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum N N₁, |{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁hconv: (ε : ), 0 < ε a_2, (b : ), a_2 b |{ m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.sum| < ε N N₁, |{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁hconv: (ε : ), 0 < ε a_2, (b : ), a_2 b |{ m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.sum| < εN:hN: (b : ), N b |{ m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.sum| < ε / 2 N N₁, |{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2 use max N N₁, (a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁hconv: (ε : ), 0 < ε a_2, (b : ), a_2 b |{ m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.sum| < εN:hN: (b : ), N b |{ m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.sum| < ε / 2max N N₁ N₁ All goals completed! 🐙); a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁hconv: (ε : ), 0 < ε a_2, (b : ), a_2 b |{ m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.sum| < εN:hN: (b : ), N b |{ m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.partial b - { m := 0, seq := fun n if 0 n then a n.toNat else 0, vanish := }.sum| < ε / 2N max N N₁; All goals completed! 🐙 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2 a, (b : ), a b |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε have hNpos : N 0 := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun f a, (b : ), a b |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε have : M, n N.toNat, finv n M := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun f n N.toNat, finv n (Finset.image finv (Finset.Iic N.toNat)).sup id intro n a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fn:hn:n N.toNatfinv n (Finset.image finv (Finset.Iic N.toNat)).sup id a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fn:hn:n N.toNat(if h : x, f x = n then h.choose else Classical.arbitrary ) Finset.image finv (Finset.Iic N.toNat); a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fn:hn:n N.toNat a N.toNat, finv a = if h : x, f x = n then h.choose else Classical.arbitrary ; a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fn:hn:n N.toNatfinv n = if h : x, f x = n then h.choose else Classical.arbitrary ; All goals completed! 🐙 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n M a, (b : ), a b |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε; a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n M (b : ), M b |{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial b - L'| < ε; intro M' a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'|{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial M' - L'| < ε have hM'_pos : M' 0 := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 have why : (Finset.Iic M'.toNat).image f .Iic N.toNat := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat|{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial M' - L'| < ε have claim : m .Iic M'.toNat, a (f m) = n .Iic N.toNat, a n + n X, a n := calc _ = n (Finset.Iic M'.toNat).image f , a n := a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat m Finset.Iic M'.toNat, a (f m) = n Finset.image f (Finset.Iic M'.toNat), a n a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat n Finset.image f (Finset.Iic M'.toNat), a n = m Finset.Iic M'.toNat, a (f m); a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatSet.InjOn f (Finset.Iic M'.toNat); All goals completed! 🐙 _ = _ := a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat n Finset.image f (Finset.Iic M'.toNat), a n = n Finset.Iic N.toNat, a n + n X, a n a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatFinset.image f (Finset.Iic M'.toNat) = Finset.Iic N.toNat Xa: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatDecidableEq a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatDisjoint (Finset.Iic N.toNat) X a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatFinset.image f (Finset.Iic M'.toNat) = Finset.Iic N.toNat X All goals completed! 🐙 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatDecidableEq All goals completed! 🐙 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNat a : ⦄, a X a Finset.Iic N.toNat; intro n a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatn:hn:n Xn Finset.Iic N.toNat; a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatn:hn:n Finset.image f (Finset.Iic M'.toNat) n Finset.Iic N.toNatn Finset.Iic N.toNat; All goals completed! 🐙 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds X|{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial M' - L'| < ε a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNat|{ m := 0, seq := fun n if 0 n then af n.toNat else 0, vanish := }.partial M' - L'| < ε have why2 : X Finset.Icc (N.toNat+1) q := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙 have claim2 : | n X, a n| ε/2 := calc _ n X, |a n| := X.abs_sum_le_sum_abs a _ n .Icc (N.toNat+1) q, |a n| := a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n X, |a n| n Finset.Icc (N.toNat + 1) q, |a n| a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q i Finset.Icc (N.toNat + 1) q, i X 0 |a i|; All goals completed! 🐙 _ ε/2 := a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n Finset.Icc (N.toNat + 1) q, |a n| ε / 2 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n Finset.Icc (N.toNat + 1) q, |a n| = | n Finset.Icc (N.toNat + 1) q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n|a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qN.toNat + 1 N₁a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qq N₁ a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n Finset.Icc (N.toNat + 1) q, |a n| = | n Finset.Icc (N.toNat + 1) q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n|a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qN.toNat + 1 N₁a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qq N₁ try All goals completed! 🐙 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n Finset.Icc (N.toNat + 1) q, |a n| = | x Finset.Icc (N + 1) q, if 0 x then |if 0 x then a x.toNat else 0| else 0|; a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q n Finset.Icc (N.toNat + 1) q, |a n| = x Finset.Icc (N + 1) q, if 0 x then |if 0 x then a x.toNat else 0| else 0; a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) q(∑ x Finset.Icc (N + 1) q, if 0 x then |if 0 x then a x.toNat else 0| else 0) = n Finset.Icc (N.toNat + 1) q, |a n| convert Finset.sum_image (g := fun (n:) (n:)) (a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qSet.InjOn (fun n n) ?m.1624 All goals completed! 🐙) using 2 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:x Finset.Icc (N + 1) q x Finset.image (fun n n) (Finset.Icc (N.toNat + 1) q); a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:N < x x q a, (N.toNat < a a q) a = x; a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:N < x x q a, (N.toNat < a a q) a = xa: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:(∃ a, (N.toNat < a a q) a = x) N < x x q a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:N < x x q a, (N.toNat < a a q) a = x a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:left✝:N < xright✝:x q a, (N.toNat < a a q) a = x; a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qx:left✝:N < xright✝:x q(N.toNat < x.toNat x.toNat q) x.toNat = x; All goals completed! 🐙 All goals completed! 🐙 calc _ |(af:Series).partial M' - (a:Series).partial N| + |(a:Series).partial N - L'| := abs_sub_le _ _ _ _ < |(af:Series).partial M' - (a:Series).partial N| + ε/2 := a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2|{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N| + |{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < |{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N| + ε / 2 All goals completed! 🐙 _ ε/2 + ε/2 := a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2|{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N| + ε / 2 ε / 2 + ε / 2 a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2|{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N| ε / 2; a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2{ m := 0, seq := fun n if n 0 then af n.toNat else 0, vanish := }.partial M' - { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N = n X, a n a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2 n Finset.Iic M'.toNat, af n - n Finset.Iic N.toNat, a n = n X, a n; All goals completed! 🐙 _ = ε := a: ha✝: ε > 0, N { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.m, p N, q N, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| εf: hf:Function.Bijective fL: := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.sumhconv:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.convergeshabs:{ m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.converges L = { m := 0, seq := fun n if n 0 then (fun n |a (f n)|) n.toNat else 0, vanish := }.sumL': := { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sumaf: := fun n a (f n)ε::0 < εN₁:ha: p N₁, q N₁, | n Finset.Icc p q, { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.abs.seq n| ε / 2hN₁:0 N₁N:hN:N N₁hN2:|{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.partial N - L'| < ε / 2hNpos:N 0finv: := Function.invFun fM:hM: n N.toNat, finv n MM':hM':M M'hM'_pos:M' 0why:Finset.image f (Finset.Iic M'.toNat) Finset.Iic N.toNatX:Finset := Finset.image f (Finset.Iic M'.toNat) \ Finset.Iic N.toNatclaim: m Finset.Iic M'.toNat, a (f m) = n Finset.Iic N.toNat, a n + n X, a nq':hq:q' upperBounds Xq: := max q' N.toNatwhy2:X Finset.Icc (N.toNat + 1) qclaim2:| n X, a n| ε / 2ε / 2 + ε / 2 = ε All goals completed! 🐙

Example 7.4.4

noncomputable abbrev Series.a_7_4_4 : := fun n (-1:)^n / (n+2)
theorem declaration uses `sorry`Series.ex_7_4_4_conv : (a_7_4_4 : Series).converges := { m := 0, seq := fun n if n 0 then a_7_4_4 n.toNat else 0, vanish := }.converges All goals completed! 🐙theorem declaration uses `sorry`Series.ex_7_4_4_sum : (a_7_4_4 : Series).sum > 0 := { m := 0, seq := fun n if n 0 then a_7_4_4 n.toNat else 0, vanish := }.sum > 0 All goals completed! 🐙abbrev Series.f_7_4_4 : := fun n if n % 3 = 0 then 2 * (n/3) else 4 * (n/3) + 2 * (n % 3) - 1theorem declaration uses `sorry`Series.f_7_4_4_bij : Function.Bijective f_7_4_4 := Function.Bijective f_7_4_4 All goals completed! 🐙theorem declaration uses `sorry`Series.ex_7_4_4'_conv : (fun n a_7_4_4 (f_7_4_4 n) :Series).converges := { m := 0, seq := fun n if n 0 then (fun n a_7_4_4 (f_7_4_4 n)) n.toNat else 0, vanish := }.converges All goals completed! 🐙theorem declaration uses `sorry`Series.ex_7_4_4'_sum : (fun n a_7_4_4 (f_7_4_4 n) :Series).sum < 0 := { m := 0, seq := fun n if n 0 then (fun n a_7_4_4 (f_7_4_4 n)) n.toNat else 0, vanish := }.sum < 0 All goals completed! 🐙

Exercise 7.4.1

theorem declaration uses `sorry`Series.absConverges_of_subseries {a: } (ha: (a:Series).absConverges) {f: } (hf: StrictMono f) : (fun n a (f n):Series).absConverges := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:StrictMono f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges All goals completed! 🐙

Exercise 7.4.2 : reprove Proposition 7.4.3 using Proposition 7.41, Proposition 7.2.14, and expressing a n as the difference of a n + |a n| and |a n|.

theorem declaration uses `sorry`Series.absConverges_of_permute' {a: } (ha : (a:Series).absConverges) {f: } (hf: Function.Bijective f) : (fun n a (f n):Series).absConverges (a:Series).sum = (fun n a (f n):Series).sum := a: ha:{ m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.absConvergesf: hf:Function.Bijective f{ m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.absConverges { m := 0, seq := fun n if n 0 then a n.toNat else 0, vanish := }.sum = { m := 0, seq := fun n if n 0 then (fun n a (f n)) n.toNat else 0, vanish := }.sum All goals completed! 🐙
end Chapter7