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:

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 ≥ 0⊢ Set.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 ≤ N⊢ x.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 => @_fvar.14602 (@_fvar.14605 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 => @_fvar.14602 (@_fvar.14605 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 => @_fvar.14602 (@_fvar.14605 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 => @_fvar.14602 (@_fvar.14605 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 => @_fvar.14602 (@_fvar.14605 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 => @_fvar.14602 (@_fvar.14605 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 => @_fvar.14602 (@_fvar.14605 n)n:ℤh:n ≥ 0ha:{ m := 0, seq := fun n => if n ≥ 0 then a n.toNat else 0, vanish := ⋯ }.seq ↑(f n.toNat) ≥ 0⊢ 0 ≤ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603⊢ { 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800⊢ { 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926⊢ { 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097⊢ { 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604⊢ { 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604⊢ (∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Q:ℝhQ:∀ (N : ℤ), S N ≤ Q⊢ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Q:ℝhQ:∀ (N : ℤ), S N ≤ Q⊢ Q ∈ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912⊢ { 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912⊢ { 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912⊢ Filter.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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912⊢ (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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912⊢ BddAbove (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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912⊢ (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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912⊢ T 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912Q:ℝhQ:∀ (M : ℤ), T M ≤ Q⊢ BddAbove (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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912Q:ℝhQ:∀ (M : ℤ), T M ≤ Q⊢ Q ∈ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604this:(∃ Q, ∀ (M : ℤ), T M ≤ Q) ∧ L = L'Ssum:_fvar.20577 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.20912Tsum:_fvar.20708 = { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.sum := ?_mvar.122064⊢ ∃ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0⊢ T 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:¬M ≥ 0⊢ 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 faf:ℕ → ℝ := fun n => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:¬M ≥ 0⊢ T 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0⊢ 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 faf:ℕ → ℝ := fun n => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:¬M ≥ 0⊢ T 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:¬M ≥ 0hM':_fvar.247761 < 0 := ?_mvar.247887⊢ 0 ≤ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:¬M ≥ 0hM':_fvar.247761 < 0 := ?_mvar.247887⊢ BddAbove (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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)⊢ T 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)⊢ ∀ m ∈ Y, f 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)m:ℕhm:m ∈ Y⊢ f 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)m:ℕhm:m ∈ Y⊢ f 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕhN:∀ m ∈ Y, f m ≤ N⊢ T 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕhN:∀ m ∈ Y, f m ≤ N⊢ T 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕhN:∀ m ∈ Y, f m ≤ N⊢ Set.InjOn ?m.631 ↑?m.630 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕhN:∀ m ∈ Y, f m ≤ N⊢ (f '' ↑Y).toFinset ⊆ Finset.Iic 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕhN:∀ m ∈ Y, f m ≤ Na✝¹:ℕa✝:a✝¹ ∈ (f '' ↑Y).toFinset⊢ a✝¹ ∈ Finset.Iic N; 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕhN:∀ m ∈ Y, f m ≤ Ni:ℕa✝¹:i ∈ Finset.Iic Na✝:i ∉ (f '' ↑Y).toFinset⊢ 0 ≤ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 ≥ 0⊢ 0 ≤ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕhN:∀ m ∈ Y, f m ≤ N⊢ ↑N ≥ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕhN:∀ m ∈ Y, f m ≤ 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 faf:ℕ → ℝ := fun n => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604M:ℤhM:M ≥ 0Y:Finset ℕ := Finset.Iic (Int.toNat _fvar.247761)N:ℕhN:∀ m ∈ Y, f m ≤ N⊢ BddAbove (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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508⊢ L = 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:N ≥ 0⊢ 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 faf:ℕ → ℝ := fun n => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:¬N ≥ 0⊢ 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 faf:ℕ → ℝ := fun n => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:¬N ≥ 0⊢ 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 faf:ℕ → ℝ := fun n => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:N ≥ 0⊢ 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 faf:ℕ → ℝ := fun n => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:¬N ≥ 0⊢ S 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:¬N ≥ 0hN':_fvar.469256 < 0 := ?_mvar.469382⊢ 0 ≤ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:¬N ≥ 0hN':_fvar.469256 < 0 := ?_mvar.469382⊢ BddAbove (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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)⊢ S 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)⊢ ∀ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)n:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)n:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)n:ℕhn:n ∈ Xm:ℕhm: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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)n:ℕhn:n ∈ Xm:ℕhm:f m = n⊢ m ∈ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕhM:∀ n ∈ X, ∃ m, f m = n ∧ m ≤ M⊢ S 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => if hM : M ≥ 0 then let Y := Finset.Iic M.toNat; have hN := Exists.intro ((Finset.image _fvar.14605 Y).sup id) fun m hm => Finset.le_sup (Chapter7.Series.converges_of_permute_nonneg._proof_3 _fvar.14603 _fvar.14604 _fvar.14606 _fvar.14800 _fvar.20439 _fvar.20560 _fvar.20877 M hM m hm); (fun N hN => Trans.trans (Trans.trans (Trans.trans (Trans.trans (Eq.mpr (id (congr (congrArg Eq (Eq.trans (congrArg (fun x => x.partial M) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 (@_fvar.14605 n.toNat) else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 (@_fvar.14605 n.toNat))) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14617))) (Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (if 0 ≤ x then @_fvar.14602 (@_fvar.14605 x.toNat) else 0)))) (Finset.sum_congr (Eq.refl Y) fun x a => Eq.refl (@_fvar.14602 (@_fvar.14605 x))))) (Chapter7.Series.sum_eq_sum _fvar.14617 hM)) (Eq.symm (Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (∑ n ∈ (_fvar.14605 '' ↑Y).toFinset, @_fvar.14602 n) (∑ x ∈ Finset.image (fun ⦃x₁⦄ => @_fvar.14605 x₁) Y, @_fvar.14602 x) (Finset.sum_congr (of_eq_true (Eq.trans (congrArg (fun x => x = Finset.image (fun ⦃x₁⦄ => @_fvar.14605 x₁) Y) (Eq.trans (Set.toFinset_image _fvar.14605 ↑Y) (congrArg (Finset.image _fvar.14605) (Finset.toFinset_coe Y)))) (eq_self (Finset.image _fvar.14605 Y)))) fun x a => Eq.refl (@_fvar.14602 x)) (∑ m ∈ Y, @_fvar.14617 m) (∑ x ∈ Y, @_fvar.14602 (@_fvar.14605 x)) (Eq.refl (∑ m ∈ Y, @_fvar.14617 m)))) (Finset.sum_image fun ⦃x₁⦄ a ⦃x₂⦄ a => Function.Bijective.injective _fvar.14606)))) (Finset.sum_le_sum_of_subset_of_nonneg (fun ⦃a⦄ a_1 => Eq.mpr (id Finset.mem_Iic._simp_1) (Exists.casesOn (Eq.mp (congrArg Chapter7.Series.converges ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602))) _fvar.14604) fun w h => Exists.casesOn (Eq.mp (congrArg Exists (funext fun Q => forall_congr fun N => congrArg (fun x => x.partial N ≤ Q) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602)))) _fvar.20877) fun w_1 h_1 => Exists.casesOn (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) (Eq.trans (Eq.trans (Set.toFinset_congr (congrArg (Set.image _fvar.14605) (Finset.coe_Iic M.toNat))) (Set.toFinset_image _fvar.14605 (Set.Iic M.toNat))) (congrArg (Finset.image _fvar.14605) (Set.toFinset_Iic M.toNat)))) Finset.mem_image._simp_1) (congrArg Exists (funext fun a_2 => congrArg (fun x => x ∧ @_fvar.14605 a_2 = a) (Eq.trans Finset.mem_Iic._simp_1 (Int.le_toNat._simp_1 (id (Eq.mp ge_iff_le._simp_1 hM))))))) a_1) fun w_2 h_2 => And.casesOn h_2 fun left right => right ▸ of_eq_true ((fun m a => eq_true (Eq.mp (forall_congr fun m => implies_congr (Eq.trans Finset.mem_Iic._simp_1 (Int.le_toNat._simp_1 (id (Eq.mp ge_iff_le._simp_1 hM)))) (Eq.refl (@_fvar.14605 m ≤ N))) hN m a)) w_2 left))) fun i a a => id (Eq.mp (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14602 (↑i).toNat) 0 (Eq.trans ge_iff_le._simp_1 (Nat.cast_nonneg._simp_1 i)))) ge_iff_le._simp_1) (@_fvar.14603 ↑i)))) (Eq.mpr (id (congrArg (Eq (∑ n ∈ Finset.Iic N, @_fvar.14602 n)) (Eq.trans (congrArg (fun x => x.partial ↑N) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602))) (Finset.sum_congr (Eq.refl (Finset.Icc 0 ↑N)) fun x a => Eq.refl (if 0 ≤ x then @_fvar.14602 x.toNat else 0))))) (Eq.symm (Chapter7.Series.sum_eq_sum _fvar.14602 (Nat.cast_nonneg' N))))) (le_ciSup (of_eq_true (Eq.trans (congrArg Exists (funext fun x => congrArg (fun x_1 => x ∈ setOf x_1) (funext fun x => Eq.trans (forall_congr fun ⦃a⦄ => Eq.trans (implies_congr Set.mem_range._simp_1 (Eq.refl (a ≤ x))) forall_exists_index._simp_1) forall_apply_eq_imp_iff._simp_1))) (eq_true _fvar.20877))) ↑N)) (Classical.choose hN) (Classical.choose_spec hN) else have hM' := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf M) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.atom_pf M) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul M (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (M ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero M (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge hM)))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))); Eq.mpr (id (Eq.trans (congrArg (fun x => x ≤ _fvar.20577) (Eq.trans (congrArg (fun x => x.partial M) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14617 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14617 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14617))) (Finset.sum_congr (Finset.Icc_eq_empty_of_lt hM') fun x a => Eq.refl (if 0 ≤ x then @_fvar.14617 x.toNat else 0)))) ge_iff_le._simp_1)) (Eq.mpr (eq_of_heq ((fun α self self' e'_2 a a' e'_3 a_1 => Eq.casesOn (motive := fun a_2 x => self' = a_2 → e'_2 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_2 (fun h => Eq.ndrec (motive := fun self' => ∀ (e_2 : self = self'), e_2 ≍ Eq.refl self → (a ≤ a_1) ≍ (a' ≤ a_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1)) (fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl self') (HEq.refl e'_2)) ℝ Real.instLE Real.instConditionallyCompleteLinearOrder.toSemilatticeInf.toLE (Eq.refl Real.instLE) 0 (@_fvar.19926 (-1)) (Eq.refl 0) _fvar.20577)) (le_ciSup (of_eq_true (Eq.trans (congrArg Exists (funext fun x => congrArg (fun x_1 => x ∈ setOf x_1) (funext fun x => Eq.trans (forall_congr fun ⦃a⦄ => Eq.trans (implies_congr Set.mem_range._simp_1 (Eq.refl (a ≤ x))) forall_exists_index._simp_1) forall_apply_eq_imp_iff._simp_1))) (eq_true _fvar.20877))) (-1)))hTbound:∃ Q, ∀ (M : ℤ), @_fvar.20097 M ≤ Q := Exists.intro _fvar.20577 _fvar.247770N✝:ℤhN✝:N✝ ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕhM:∀ n ∈ X, ∃ m, f m = n ∧ m ≤ Mb:ℕ → ℝN:ℤhN:N ≥ 0⊢ Set.InjOn Int.ofNat ↑?m.1144 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N✝:ℤhN✝:N✝ ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N✝:ℤhN✝:N✝ ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N✝:ℤhN✝:N✝ ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N✝:ℤhN✝:N✝ ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N✝:ℤhN✝:N✝ ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N✝:ℤhN✝:N✝ ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕ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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := ?_mvar.14799S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => @?_mvar.247769 MhTbound:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.468508N✝:ℤhN✝:N✝ ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕhM:∀ n ∈ X, ∃ m, f m = n ∧ m ≤ Mb:ℕ → ℝN:ℤhN:N ≥ 0x:ℤleft✝:0 ≤ xright✝:x ≤ N⊢ x.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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => if hM : M ≥ 0 then let Y := Finset.Iic M.toNat; have hN := Exists.intro ((Finset.image _fvar.14605 Y).sup id) fun m hm => Finset.le_sup (Chapter7.Series.converges_of_permute_nonneg._proof_3 _fvar.14603 _fvar.14604 _fvar.14606 _fvar.14800 _fvar.20439 _fvar.20560 _fvar.20877 M hM m hm); (fun N hN => Trans.trans (Trans.trans (Trans.trans (Trans.trans (Eq.mpr (id (congr (congrArg Eq (Eq.trans (congrArg (fun x => x.partial M) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 (@_fvar.14605 n.toNat) else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 (@_fvar.14605 n.toNat))) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14617))) (Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (if 0 ≤ x then @_fvar.14602 (@_fvar.14605 x.toNat) else 0)))) (Finset.sum_congr (Eq.refl Y) fun x a => Eq.refl (@_fvar.14602 (@_fvar.14605 x))))) (Chapter7.Series.sum_eq_sum _fvar.14617 hM)) (Eq.symm (Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (∑ n ∈ (_fvar.14605 '' ↑Y).toFinset, @_fvar.14602 n) (∑ x ∈ Finset.image (fun ⦃x₁⦄ => @_fvar.14605 x₁) Y, @_fvar.14602 x) (Finset.sum_congr (of_eq_true (Eq.trans (congrArg (fun x => x = Finset.image (fun ⦃x₁⦄ => @_fvar.14605 x₁) Y) (Eq.trans (Set.toFinset_image _fvar.14605 ↑Y) (congrArg (Finset.image _fvar.14605) (Finset.toFinset_coe Y)))) (eq_self (Finset.image _fvar.14605 Y)))) fun x a => Eq.refl (@_fvar.14602 x)) (∑ m ∈ Y, @_fvar.14617 m) (∑ x ∈ Y, @_fvar.14602 (@_fvar.14605 x)) (Eq.refl (∑ m ∈ Y, @_fvar.14617 m)))) (Finset.sum_image fun ⦃x₁⦄ a ⦃x₂⦄ a => Function.Bijective.injective _fvar.14606)))) (Finset.sum_le_sum_of_subset_of_nonneg (fun ⦃a⦄ a_1 => Eq.mpr (id Finset.mem_Iic._simp_1) (Exists.casesOn (Eq.mp (congrArg Chapter7.Series.converges ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602))) _fvar.14604) fun w h => Exists.casesOn (Eq.mp (congrArg Exists (funext fun Q => forall_congr fun N => congrArg (fun x => x.partial N ≤ Q) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602)))) _fvar.20877) fun w_1 h_1 => Exists.casesOn (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) (Eq.trans (Eq.trans (Set.toFinset_congr (congrArg (Set.image _fvar.14605) (Finset.coe_Iic M.toNat))) (Set.toFinset_image _fvar.14605 (Set.Iic M.toNat))) (congrArg (Finset.image _fvar.14605) (Set.toFinset_Iic M.toNat)))) Finset.mem_image._simp_1) (congrArg Exists (funext fun a_2 => congrArg (fun x => x ∧ @_fvar.14605 a_2 = a) (Eq.trans Finset.mem_Iic._simp_1 (Int.le_toNat._simp_1 (id (Eq.mp ge_iff_le._simp_1 hM))))))) a_1) fun w_2 h_2 => And.casesOn h_2 fun left right => right ▸ of_eq_true ((fun m a => eq_true (Eq.mp (forall_congr fun m => implies_congr (Eq.trans Finset.mem_Iic._simp_1 (Int.le_toNat._simp_1 (id (Eq.mp ge_iff_le._simp_1 hM)))) (Eq.refl (@_fvar.14605 m ≤ N))) hN m a)) w_2 left))) fun i a a => id (Eq.mp (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14602 (↑i).toNat) 0 (Eq.trans ge_iff_le._simp_1 (Nat.cast_nonneg._simp_1 i)))) ge_iff_le._simp_1) (@_fvar.14603 ↑i)))) (Eq.mpr (id (congrArg (Eq (∑ n ∈ Finset.Iic N, @_fvar.14602 n)) (Eq.trans (congrArg (fun x => x.partial ↑N) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602))) (Finset.sum_congr (Eq.refl (Finset.Icc 0 ↑N)) fun x a => Eq.refl (if 0 ≤ x then @_fvar.14602 x.toNat else 0))))) (Eq.symm (Chapter7.Series.sum_eq_sum _fvar.14602 (Nat.cast_nonneg' N))))) (le_ciSup (of_eq_true (Eq.trans (congrArg Exists (funext fun x => congrArg (fun x_1 => x ∈ setOf x_1) (funext fun x => Eq.trans (forall_congr fun ⦃a⦄ => Eq.trans (implies_congr Set.mem_range._simp_1 (Eq.refl (a ≤ x))) forall_exists_index._simp_1) forall_apply_eq_imp_iff._simp_1))) (eq_true _fvar.20877))) ↑N)) (Classical.choose hN) (Classical.choose_spec hN) else have hM' := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf M) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.atom_pf M) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul M (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (M ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero M (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge hM)))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))); Eq.mpr (id (Eq.trans (congrArg (fun x => x ≤ _fvar.20577) (Eq.trans (congrArg (fun x => x.partial M) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14617 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14617 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14617))) (Finset.sum_congr (Finset.Icc_eq_empty_of_lt hM') fun x a => Eq.refl (if 0 ≤ x then @_fvar.14617 x.toNat else 0)))) ge_iff_le._simp_1)) (Eq.mpr (eq_of_heq ((fun α self self' e'_2 a a' e'_3 a_1 => Eq.casesOn (motive := fun a_2 x => self' = a_2 → e'_2 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_2 (fun h => Eq.ndrec (motive := fun self' => ∀ (e_2 : self = self'), e_2 ≍ Eq.refl self → (a ≤ a_1) ≍ (a' ≤ a_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1)) (fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl self') (HEq.refl e'_2)) ℝ Real.instLE Real.instConditionallyCompleteLinearOrder.toSemilatticeInf.toLE (Eq.refl Real.instLE) 0 (@_fvar.19926 (-1)) (Eq.refl 0) _fvar.20577)) (le_ciSup (of_eq_true (Eq.trans (congrArg Exists (funext fun x => congrArg (fun x_1 => x ∈ setOf x_1) (funext fun x => Eq.trans (forall_congr fun ⦃a⦄ => Eq.trans (implies_congr Set.mem_range._simp_1 (Eq.refl (a ≤ x))) forall_exists_index._simp_1) forall_apply_eq_imp_iff._simp_1))) (eq_true _fvar.20877))) (-1)))hTbound:∃ Q, ∀ (M : ℤ), @_fvar.20097 M ≤ Q := Exists.intro _fvar.20577 _fvar.247770N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕ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 := fun b {N} hN => Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (∑ n ∈ Finset.Icc 0 N, if 0 ≤ n then b n.toNat else 0) (∑ x ∈ Finset.image Int.ofNat (Finset.Iic N.toNat), if 0 ≤ x then b x.toNat else 0) (Finset.sum_congr (Finset.ext fun x => Eq.mpr (id (congr (congrArg Iff Finset.mem_Icc._simp_1) (Eq.trans Finset.mem_image._simp_1 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ ↑a = x) Finset.mem_Iic._simp_1))))) { mp := fun h => match h with | ⟨left, right⟩ => Exists.intro x.toNat (Decidable.byContradiction fun a => Chapter7.Series.converges_of_permute_nonneg._proof_5 _fvar.469256 hN x left right a), mpr := Chapter7.Series.converges_of_permute_nonneg._proof_6 _fvar.14603 _fvar.14604 _fvar.14606 _fvar.14800 _fvar.20439 _fvar.20560 _fvar.20877 _fvar.247770 _fvar.468509 _fvar.469256 _fvar.469329 _fvar.482509 _fvar.482513 b hN x }) fun x a => Eq.refl (if 0 ≤ x then b x.toNat else 0)) (∑ n ∈ Finset.Iic N.toNat, b n) (∑ x ∈ Finset.Iic N.toNat, if 0 ≤ Int.ofNat x then b (Int.ofNat x).toNat else 0) (Finset.sum_congr (Eq.refl (Finset.Iic N.toNat)) fun x a => Eq.refl (b x)))) (Finset.sum_image (of_eq_true (Set.injOn_of_eq_iff_eq._simp_1 (↑(Finset.Iic N.toNat)) (of_eq_true (Eq.trans (forall_congr fun x => Eq.trans (forall_congr fun y => Eq.trans (congrArg (fun x_1 => x_1 ↔ x = y) Nat.cast_inj._simp_1) (iff_self (x = y))) (implies_true ℕ)) (implies_true ℕ))))))⊢ S 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => if hM : M ≥ 0 then let Y := Finset.Iic M.toNat; have hN := Exists.intro ((Finset.image _fvar.14605 Y).sup id) fun m hm => Finset.le_sup (Chapter7.Series.converges_of_permute_nonneg._proof_3 _fvar.14603 _fvar.14604 _fvar.14606 _fvar.14800 _fvar.20439 _fvar.20560 _fvar.20877 M hM m hm); (fun N hN => Trans.trans (Trans.trans (Trans.trans (Trans.trans (Eq.mpr (id (congr (congrArg Eq (Eq.trans (congrArg (fun x => x.partial M) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 (@_fvar.14605 n.toNat) else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 (@_fvar.14605 n.toNat))) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14617))) (Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (if 0 ≤ x then @_fvar.14602 (@_fvar.14605 x.toNat) else 0)))) (Finset.sum_congr (Eq.refl Y) fun x a => Eq.refl (@_fvar.14602 (@_fvar.14605 x))))) (Chapter7.Series.sum_eq_sum _fvar.14617 hM)) (Eq.symm (Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (∑ n ∈ (_fvar.14605 '' ↑Y).toFinset, @_fvar.14602 n) (∑ x ∈ Finset.image (fun ⦃x₁⦄ => @_fvar.14605 x₁) Y, @_fvar.14602 x) (Finset.sum_congr (of_eq_true (Eq.trans (congrArg (fun x => x = Finset.image (fun ⦃x₁⦄ => @_fvar.14605 x₁) Y) (Eq.trans (Set.toFinset_image _fvar.14605 ↑Y) (congrArg (Finset.image _fvar.14605) (Finset.toFinset_coe Y)))) (eq_self (Finset.image _fvar.14605 Y)))) fun x a => Eq.refl (@_fvar.14602 x)) (∑ m ∈ Y, @_fvar.14617 m) (∑ x ∈ Y, @_fvar.14602 (@_fvar.14605 x)) (Eq.refl (∑ m ∈ Y, @_fvar.14617 m)))) (Finset.sum_image fun ⦃x₁⦄ a ⦃x₂⦄ a => Function.Bijective.injective _fvar.14606)))) (Finset.sum_le_sum_of_subset_of_nonneg (fun ⦃a⦄ a_1 => Eq.mpr (id Finset.mem_Iic._simp_1) (Exists.casesOn (Eq.mp (congrArg Chapter7.Series.converges ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602))) _fvar.14604) fun w h => Exists.casesOn (Eq.mp (congrArg Exists (funext fun Q => forall_congr fun N => congrArg (fun x => x.partial N ≤ Q) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602)))) _fvar.20877) fun w_1 h_1 => Exists.casesOn (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) (Eq.trans (Eq.trans (Set.toFinset_congr (congrArg (Set.image _fvar.14605) (Finset.coe_Iic M.toNat))) (Set.toFinset_image _fvar.14605 (Set.Iic M.toNat))) (congrArg (Finset.image _fvar.14605) (Set.toFinset_Iic M.toNat)))) Finset.mem_image._simp_1) (congrArg Exists (funext fun a_2 => congrArg (fun x => x ∧ @_fvar.14605 a_2 = a) (Eq.trans Finset.mem_Iic._simp_1 (Int.le_toNat._simp_1 (id (Eq.mp ge_iff_le._simp_1 hM))))))) a_1) fun w_2 h_2 => And.casesOn h_2 fun left right => right ▸ of_eq_true ((fun m a => eq_true (Eq.mp (forall_congr fun m => implies_congr (Eq.trans Finset.mem_Iic._simp_1 (Int.le_toNat._simp_1 (id (Eq.mp ge_iff_le._simp_1 hM)))) (Eq.refl (@_fvar.14605 m ≤ N))) hN m a)) w_2 left))) fun i a a => id (Eq.mp (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14602 (↑i).toNat) 0 (Eq.trans ge_iff_le._simp_1 (Nat.cast_nonneg._simp_1 i)))) ge_iff_le._simp_1) (@_fvar.14603 ↑i)))) (Eq.mpr (id (congrArg (Eq (∑ n ∈ Finset.Iic N, @_fvar.14602 n)) (Eq.trans (congrArg (fun x => x.partial ↑N) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602))) (Finset.sum_congr (Eq.refl (Finset.Icc 0 ↑N)) fun x a => Eq.refl (if 0 ≤ x then @_fvar.14602 x.toNat else 0))))) (Eq.symm (Chapter7.Series.sum_eq_sum _fvar.14602 (Nat.cast_nonneg' N))))) (le_ciSup (of_eq_true (Eq.trans (congrArg Exists (funext fun x => congrArg (fun x_1 => x ∈ setOf x_1) (funext fun x => Eq.trans (forall_congr fun ⦃a⦄ => Eq.trans (implies_congr Set.mem_range._simp_1 (Eq.refl (a ≤ x))) forall_exists_index._simp_1) forall_apply_eq_imp_iff._simp_1))) (eq_true _fvar.20877))) ↑N)) (Classical.choose hN) (Classical.choose_spec hN) else have hM' := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf M) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.atom_pf M) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul M (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (M ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero M (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge hM)))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))); Eq.mpr (id (Eq.trans (congrArg (fun x => x ≤ _fvar.20577) (Eq.trans (congrArg (fun x => x.partial M) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14617 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14617 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14617))) (Finset.sum_congr (Finset.Icc_eq_empty_of_lt hM') fun x a => Eq.refl (if 0 ≤ x then @_fvar.14617 x.toNat else 0)))) ge_iff_le._simp_1)) (Eq.mpr (eq_of_heq ((fun α self self' e'_2 a a' e'_3 a_1 => Eq.casesOn (motive := fun a_2 x => self' = a_2 → e'_2 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_2 (fun h => Eq.ndrec (motive := fun self' => ∀ (e_2 : self = self'), e_2 ≍ Eq.refl self → (a ≤ a_1) ≍ (a' ≤ a_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1)) (fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl self') (HEq.refl e'_2)) ℝ Real.instLE Real.instConditionallyCompleteLinearOrder.toSemilatticeInf.toLE (Eq.refl Real.instLE) 0 (@_fvar.19926 (-1)) (Eq.refl 0) _fvar.20577)) (le_ciSup (of_eq_true (Eq.trans (congrArg Exists (funext fun x => congrArg (fun x_1 => x ∈ setOf x_1) (funext fun x => Eq.trans (forall_congr fun ⦃a⦄ => Eq.trans (implies_congr Set.mem_range._simp_1 (Eq.refl (a ≤ x))) forall_exists_index._simp_1) forall_apply_eq_imp_iff._simp_1))) (eq_true _fvar.20877))) (-1)))hTbound:∃ Q, ∀ (M : ℤ), @_fvar.20097 M ≤ Q := Exists.intro _fvar.20577 _fvar.247770N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕ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 := fun b {N} hN => Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (∑ n ∈ Finset.Icc 0 N, if 0 ≤ n then b n.toNat else 0) (∑ x ∈ Finset.image Int.ofNat (Finset.Iic N.toNat), if 0 ≤ x then b x.toNat else 0) (Finset.sum_congr (Finset.ext fun x => Eq.mpr (id (congr (congrArg Iff Finset.mem_Icc._simp_1) (Eq.trans Finset.mem_image._simp_1 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ ↑a = x) Finset.mem_Iic._simp_1))))) { mp := fun h => match h with | ⟨left, right⟩ => Exists.intro x.toNat (Decidable.byContradiction fun a => Chapter7.Series.converges_of_permute_nonneg._proof_5 _fvar.469256 hN x left right a), mpr := Chapter7.Series.converges_of_permute_nonneg._proof_6 _fvar.14603 _fvar.14604 _fvar.14606 _fvar.14800 _fvar.20439 _fvar.20560 _fvar.20877 _fvar.247770 _fvar.468509 _fvar.469256 _fvar.469329 _fvar.482509 _fvar.482513 b hN x }) fun x a => Eq.refl (if 0 ≤ x then b x.toNat else 0)) (∑ n ∈ Finset.Iic N.toNat, b n) (∑ x ∈ Finset.Iic N.toNat, if 0 ≤ Int.ofNat x then b (Int.ofNat x).toNat else 0) (Finset.sum_congr (Eq.refl (Finset.Iic N.toNat)) fun x a => Eq.refl (b x)))) (Finset.sum_image (of_eq_true (Set.injOn_of_eq_iff_eq._simp_1 (↑(Finset.Iic N.toNat)) (of_eq_true (Eq.trans (forall_congr fun x => Eq.trans (forall_congr fun y => Eq.trans (congrArg (fun x_1 => x_1 ↔ x = y) Nat.cast_inj._simp_1) (iff_self (x = y))) (implies_true ℕ)) (implies_true ℕ))))))⊢ ∑ 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h : n ≥ 0 then Eq.mpr (id (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_true h)))) ge_iff_le._simp_1)) (Chapter7.Series.converges_of_permute_nonneg._proof_1 _fvar.14604 _fvar.14606 n h (@_fvar.14603 ↑(@_fvar.14605 n.toNat))) else of_eq_true (Eq.trans (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_false (@_fvar.14617 n.toNat) 0 (Eq.trans ge_iff_le._simp_1 (eq_false h)))) ge_iff_le._simp_1) (le_refl._simp_1 0))S:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0, vanish := ⋯ }.partialT:ℤ → ℝ := { m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.partialhSmono:Monotone _fvar.19926 := Chapter7.Series.partial_of_nonneg _fvar.14603hTmono:Monotone _fvar.20097 := Chapter7.Series.partial_of_nonneg _fvar.14800L:ℝ := iSup _fvar.19926L':ℝ := iSup _fvar.20097hSBound:∃ Q, ∀ (N : ℤ), @_fvar.19926 N ≤ Q := (Chapter7.Series.converges_of_nonneg_iff _fvar.14603).mp _fvar.14604hTL:∀ (M : ℤ), @_fvar.20097 M ≤ _fvar.20577 := fun M => if hM : M ≥ 0 then let Y := Finset.Iic M.toNat; have hN := Exists.intro ((Finset.image _fvar.14605 Y).sup id) fun m hm => Finset.le_sup (Chapter7.Series.converges_of_permute_nonneg._proof_3 _fvar.14603 _fvar.14604 _fvar.14606 _fvar.14800 _fvar.20439 _fvar.20560 _fvar.20877 M hM m hm); (fun N hN => Trans.trans (Trans.trans (Trans.trans (Trans.trans (Eq.mpr (id (congr (congrArg Eq (Eq.trans (congrArg (fun x => x.partial M) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 (@_fvar.14605 n.toNat) else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 (@_fvar.14605 n.toNat))) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14617))) (Finset.sum_congr (Eq.refl (Finset.Icc 0 M)) fun x a => Eq.refl (if 0 ≤ x then @_fvar.14602 (@_fvar.14605 x.toNat) else 0)))) (Finset.sum_congr (Eq.refl Y) fun x a => Eq.refl (@_fvar.14602 (@_fvar.14605 x))))) (Chapter7.Series.sum_eq_sum _fvar.14617 hM)) (Eq.symm (Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (∑ n ∈ (_fvar.14605 '' ↑Y).toFinset, @_fvar.14602 n) (∑ x ∈ Finset.image (fun ⦃x₁⦄ => @_fvar.14605 x₁) Y, @_fvar.14602 x) (Finset.sum_congr (of_eq_true (Eq.trans (congrArg (fun x => x = Finset.image (fun ⦃x₁⦄ => @_fvar.14605 x₁) Y) (Eq.trans (Set.toFinset_image _fvar.14605 ↑Y) (congrArg (Finset.image _fvar.14605) (Finset.toFinset_coe Y)))) (eq_self (Finset.image _fvar.14605 Y)))) fun x a => Eq.refl (@_fvar.14602 x)) (∑ m ∈ Y, @_fvar.14617 m) (∑ x ∈ Y, @_fvar.14602 (@_fvar.14605 x)) (Eq.refl (∑ m ∈ Y, @_fvar.14617 m)))) (Finset.sum_image fun ⦃x₁⦄ a ⦃x₂⦄ a => Function.Bijective.injective _fvar.14606)))) (Finset.sum_le_sum_of_subset_of_nonneg (fun ⦃a⦄ a_1 => Eq.mpr (id Finset.mem_Iic._simp_1) (Exists.casesOn (Eq.mp (congrArg Chapter7.Series.converges ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602))) _fvar.14604) fun w h => Exists.casesOn (Eq.mp (congrArg Exists (funext fun Q => forall_congr fun N => congrArg (fun x => x.partial N ≤ Q) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602)))) _fvar.20877) fun w_1 h_1 => Exists.casesOn (Eq.mp (Eq.trans (Eq.trans (congrArg (fun x => a ∈ x) (Eq.trans (Eq.trans (Set.toFinset_congr (congrArg (Set.image _fvar.14605) (Finset.coe_Iic M.toNat))) (Set.toFinset_image _fvar.14605 (Set.Iic M.toNat))) (congrArg (Finset.image _fvar.14605) (Set.toFinset_Iic M.toNat)))) Finset.mem_image._simp_1) (congrArg Exists (funext fun a_2 => congrArg (fun x => x ∧ @_fvar.14605 a_2 = a) (Eq.trans Finset.mem_Iic._simp_1 (Int.le_toNat._simp_1 (id (Eq.mp ge_iff_le._simp_1 hM))))))) a_1) fun w_2 h_2 => And.casesOn h_2 fun left right => right ▸ of_eq_true ((fun m a => eq_true (Eq.mp (forall_congr fun m => implies_congr (Eq.trans Finset.mem_Iic._simp_1 (Int.le_toNat._simp_1 (id (Eq.mp ge_iff_le._simp_1 hM)))) (Eq.refl (@_fvar.14605 m ≤ N))) hN m a)) w_2 left))) fun i a a => id (Eq.mp (Eq.trans (congrArg (fun x => x ≥ 0) (ite_cond_eq_true (@_fvar.14602 (↑i).toNat) 0 (Eq.trans ge_iff_le._simp_1 (Nat.cast_nonneg._simp_1 i)))) ge_iff_le._simp_1) (@_fvar.14603 ↑i)))) (Eq.mpr (id (congrArg (Eq (∑ n ∈ Finset.Iic N, @_fvar.14602 n)) (Eq.trans (congrArg (fun x => x.partial ↑N) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14602 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14602 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14602 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14602))) (Finset.sum_congr (Eq.refl (Finset.Icc 0 ↑N)) fun x a => Eq.refl (if 0 ≤ x then @_fvar.14602 x.toNat else 0))))) (Eq.symm (Chapter7.Series.sum_eq_sum _fvar.14602 (Nat.cast_nonneg' N))))) (le_ciSup (of_eq_true (Eq.trans (congrArg Exists (funext fun x => congrArg (fun x_1 => x ∈ setOf x_1) (funext fun x => Eq.trans (forall_congr fun ⦃a⦄ => Eq.trans (implies_congr Set.mem_range._simp_1 (Eq.refl (a ≤ x))) forall_exists_index._simp_1) forall_apply_eq_imp_iff._simp_1))) (eq_true _fvar.20877))) ↑N)) (Classical.choose hN) (Classical.choose_spec hN) else have hM' := lt_of_not_ge fun a => Mathlib.Tactic.Linarith.lt_irrefl (Eq.mp (congrArg (fun _a => _a < 0) (Mathlib.Tactic.Ring.of_eq (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.neg_congr (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1))))) Mathlib.Tactic.Ring.neg_zero)) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf M) (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1))) (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1) (Mathlib.Tactic.Ring.add_pf_add_zero (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero (Mathlib.Tactic.Ring.add_pf_add_zero (Nat.rawCast 1 + (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.ofNat 0)))) (Mathlib.Tactic.Ring.add_pf_zero_add (M ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))) (Mathlib.Tactic.Ring.sub_congr (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))) (Mathlib.Tactic.Ring.atom_pf M) (Mathlib.Tactic.Ring.sub_pf (Mathlib.Tactic.Ring.neg_add (Mathlib.Tactic.Ring.neg_mul M (Nat.rawCast 1) (Mathlib.Tactic.Ring.neg_one_mul (Mathlib.Meta.NormNum.IsInt.to_raw_eq (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Eq.refl (Int.negOfNat 1)))))) Mathlib.Tactic.Ring.neg_zero) (Mathlib.Tactic.Ring.add_pf_zero_add (M ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))) (Mathlib.Tactic.Ring.add_pf_add_overlap_zero (Mathlib.Tactic.Ring.add_overlap_pf_zero M (Nat.rawCast 1) (Mathlib.Meta.NormNum.IsInt.to_isNat (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)) (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))) (Mathlib.Tactic.Ring.add_pf_zero_add 0))) (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0))))) (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one) (Mathlib.Tactic.Linarith.sub_nonpos_of_le (Int.add_one_le_iff.mpr (lt_of_not_ge hM)))) (Mathlib.Tactic.Linarith.sub_nonpos_of_le a))); Eq.mpr (id (Eq.trans (congrArg (fun x => x ≤ _fvar.20577) (Eq.trans (congrArg (fun x => x.partial M) ((fun m m_1 e_m => Eq.rec (motive := fun m_2 e_m => ∀ (seq seq_1 : ℤ → ℝ) (e_seq : seq = seq_1) (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m_2, seq := seq_1, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_1 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) e_m }) (fun seq seq_1 e_seq => Eq.rec (motive := fun seq_2 e_seq => ∀ (vanish : ∀ n < m, seq n = 0), { m := m, seq := seq, vanish := vanish } = { m := m, seq := seq_2, vanish := Eq.ndrec (motive := fun m => ∀ n < m, seq_2 n = 0) (Eq.ndrec (motive := fun seq => ∀ n < m, seq n = 0) vanish e_seq) (Eq.refl m) }) (fun vanish => Eq.refl { m := m, seq := seq, vanish := vanish }) e_seq) e_m) 0 0 (Eq.refl 0) (fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0) (fun n => if 0 ≤ n then @_fvar.14617 n.toNat else 0) (funext fun n => ite_congr ge_iff_le._simp_1 (fun a => Eq.refl (@_fvar.14617 n.toNat)) fun a => Eq.refl 0) (Chapter7.Series.instCoe._proof_1 _fvar.14617))) (Finset.sum_congr (Finset.Icc_eq_empty_of_lt hM') fun x a => Eq.refl (if 0 ≤ x then @_fvar.14617 x.toNat else 0)))) ge_iff_le._simp_1)) (Eq.mpr (eq_of_heq ((fun α self self' e'_2 a a' e'_3 a_1 => Eq.casesOn (motive := fun a_2 x => self' = a_2 → e'_2 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_2 (fun h => Eq.ndrec (motive := fun self' => ∀ (e_2 : self = self'), e_2 ≍ Eq.refl self → (a ≤ a_1) ≍ (a' ≤ a_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_3 ≍ x → (a ≤ a_1) ≍ (a' ≤ a_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a = a'), e_3 ≍ Eq.refl a → (a ≤ a_1) ≍ (a' ≤ a_1)) (fun e_3 h => HEq.refl (a ≤ a_1)) (Eq.symm h) e'_3) (Eq.refl a') (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl self') (HEq.refl e'_2)) ℝ Real.instLE Real.instConditionallyCompleteLinearOrder.toSemilatticeInf.toLE (Eq.refl Real.instLE) 0 (@_fvar.19926 (-1)) (Eq.refl 0) _fvar.20577)) (le_ciSup (of_eq_true (Eq.trans (congrArg Exists (funext fun x => congrArg (fun x_1 => x ∈ setOf x_1) (funext fun x => Eq.trans (forall_congr fun ⦃a⦄ => Eq.trans (implies_congr Set.mem_range._simp_1 (Eq.refl (a ≤ x))) forall_exists_index._simp_1) forall_apply_eq_imp_iff._simp_1))) (eq_true _fvar.20877))) (-1)))hTbound:∃ Q, ∀ (M : ℤ), @_fvar.20097 M ≤ Q := Exists.intro _fvar.20577 _fvar.247770N:ℤhN:N ≥ 0X:Finset ℕ := Finset.Iic (Int.toNat _fvar.469256)M:ℕ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 := fun b {N} hN => Eq.mpr (eq_of_heq ((fun α a a' e'_2 a_1 a'_1 e'_3 => Eq.casesOn (motive := fun a_2 x => a' = a_2 → e'_2 ≍ x → (a = a_1) ≍ (a' = a'_1)) e'_2 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_2 : a = a'), e_2 ≍ Eq.refl a → (a = a_1) ≍ (a' = a'_1)) (fun e_2 h => Eq.casesOn (motive := fun a_2 x => a'_1 = a_2 → e'_3 ≍ x → (a = a_1) ≍ (a = a'_1)) e'_3 (fun h => Eq.ndrec (motive := fun a' => ∀ (e_3 : a_1 = a'), e_3 ≍ Eq.refl a_1 → (a = a_1) ≍ (a = a')) (fun e_3 h => HEq.refl (a = a_1)) (Eq.symm h) e'_3) (Eq.refl a'_1) (HEq.refl e'_3)) (Eq.symm h) e'_2) (Eq.refl a') (HEq.refl e'_2)) ℝ (∑ n ∈ Finset.Icc 0 N, if 0 ≤ n then b n.toNat else 0) (∑ x ∈ Finset.image Int.ofNat (Finset.Iic N.toNat), if 0 ≤ x then b x.toNat else 0) (Finset.sum_congr (Finset.ext fun x => Eq.mpr (id (congr (congrArg Iff Finset.mem_Icc._simp_1) (Eq.trans Finset.mem_image._simp_1 (congrArg Exists (funext fun a => congrArg (fun x_1 => x_1 ∧ ↑a = x) Finset.mem_Iic._simp_1))))) { mp := fun h => match h with | ⟨left, right⟩ => Exists.intro x.toNat (Decidable.byContradiction fun a => Chapter7.Series.converges_of_permute_nonneg._proof_5 _fvar.469256 hN x left right a), mpr := Chapter7.Series.converges_of_permute_nonneg._proof_6 _fvar.14603 _fvar.14604 _fvar.14606 _fvar.14800 _fvar.20439 _fvar.20560 _fvar.20877 _fvar.247770 _fvar.468509 _fvar.469256 _fvar.469329 _fvar.482509 _fvar.482513 b hN x }) fun x a => Eq.refl (if 0 ≤ x then b x.toNat else 0)) (∑ n ∈ Finset.Iic N.toNat, b n) (∑ x ∈ Finset.Iic N.toNat, if 0 ≤ Int.ofNat x then b (Int.ofNat x).toNat else 0) (Finset.sum_congr (Eq.refl (Finset.Iic N.toNat)) fun x a => Eq.refl (b x)))) (Finset.sum_image (of_eq_true (Set.injOn_of_eq_iff_eq._simp_1 (↑(Finset.Iic N.toNat)) (of_eq_true (Eq.trans (forall_congr fun x => Eq.trans (forall_congr fun y => Eq.trans (congrArg (fun x_1 => x_1 ↔ x = y) Nat.cast_inj._simp_1) (iff_self (x = y))) (implies_true ℕ)) (implies_true ℕ))))))⊢ X = 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 => @_fvar.14602 (@_fvar.14605 n)haf:{ m := 0, seq := fun n => if n ≥ 0 then @_fvar.14617 n.toNat else 0, vanish := ⋯ }.nonneg := fun n => if h