Analysis
7.1. Finite series

Imports

import Mathlib.Tactic

set_option doc.verso.suggestions false

Analysis I, Section 7.1: Finite 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.

Technical note: it is convenient in Lean to extend finite sequences (usually by zero) to be functions on the entire integers.

Main constructions and results of this section:

-- This makes available the convenient notation `∑ n ∈ A, f n` to denote summation of `f n` for
-- `n` ranging over a finite set `A`.
open BigOperators

API for summation over finite sets (encoded using Mathlib's Finset type), using the Finset.sum method and the ∑ n ∈ A, f n notation.
Fubini's theorem for finite series

We do not attempt to replicate the full API for Finset.sum here, but in subsequent sections we shall make liberal use of this API.

              -- This is a technical device to avoid Mathlib's insistence on decidable equality for finite sets.
open Classicalnamespace Finset-- We use `Finset.Icc` to describe finite intervals in the integers. `Finset.mem_Icc` is the
-- standard Mathlib tool for checking membership in such intervals.
Finset.mem_Icc.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b x : α} : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b#check mem_Icc

Definition 7.1.1

theorem sum_of_empty {n m:ℤ} (h: n < m) (a: ℤ → ℝ) : ∑ i ∈ Icc m n, a i = 0 := byn:ℤm:ℤh:n < ma:ℤ → ℝ⊢ ∑ i ∈ Icc m n, a i = 0
  rw [sum_eq_zero]n:ℤm:ℤh:n < ma:ℤ → ℝ⊢ ∀ x ∈ Icc m n, a x = 0; intro _n:ℤm:ℤh:n < ma:ℤ → ℝx✝:ℤ⊢ x✝ ∈ Icc m n → a x✝ = 0; rw [mem_Icc]n:ℤm:ℤh:n < ma:ℤ → ℝx✝:ℤ⊢ m ≤ x✝ ∧ x✝ ≤ n → a x✝ = 0; grindAll goals completed! 🐙

Definition 7.1.1. This is similar to Mathlib's Finset.sum_Icc_succ_top except that the latter involves summation over the natural numbers rather than integers.

theorem sum_of_nonempty {n m:ℤ} (h: n ≥ m-1) (a: ℤ → ℝ) :
    ∑ i ∈ Icc m (n+1), a i = ∑ i ∈ Icc m n, a i + a (n+1) := byn:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ ∑ i ∈ Icc m (n + 1), a i = ∑ i ∈ Icc m n, a i + a (n + 1)
  rw [add_comm _ (a (n+1))]n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ ∑ i ∈ Icc m (n + 1), a i = a (n + 1) + ∑ i ∈ Icc m n, a i
  convert sum_insert _h.e'_2.hn:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ Icc m (n + 1) = insert (n + 1) (Icc m n)convert_7n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ DecidableEq ℤconvert_8n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ n + 1 ∉ Icc m n
  .h.e'_2.hn:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ Icc m (n + 1) = insert (n + 1) (Icc m n) exth.e'_2.h.hn:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝa✝:ℤ⊢ a✝ ∈ Icc m (n + 1) ↔ a✝ ∈ insert (n + 1) (Icc m n); simph.e'_2.h.hn:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝa✝:ℤ⊢ m ≤ a✝ ∧ a✝ ≤ n + 1 ↔ a✝ = n + 1 ∨ m ≤ a✝ ∧ a✝ ≤ n; omegaAll goals completed! 🐙
  .convert_7n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ DecidableEq ℤ infer_instanceAll goals completed! 🐙
  simpAll goals completed! 🐙

              declaration uses `sorry`example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m (m-2), a i = 0 := bya:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m (m - 2), a i = 0 sorryAll goals completed! 🐙declaration uses `sorry`example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m (m-1), a i = 0 := bya:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m (m - 1), a i = 0 sorryAll goals completed! 🐙declaration uses `sorry`example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m m, a i = a m := bya:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m m, a i = a m sorryAll goals completed! 🐙declaration uses `sorry`example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m (m+1), a i = a m + a (m+1) := bya:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m (m + 1), a i = a m + a (m + 1) sorryAll goals completed! 🐙declaration uses `sorry`example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m (m+2), a i = a m + a (m+1) + a (m+2) := bya:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m (m + 2), a i = a m + a (m + 1) + a (m + 2) sorryAll goals completed! 🐙/-- Remark 7.1.3 -/
example (a: ℤ → ℝ) (m n:ℤ) : ∑ i ∈ Icc m n, a i = ∑ j ∈ Icc m n, a j := rfl

Lemma 7.1.4(a) / Exercise 7.1.1

theorem declaration uses `sorry`concat_finite_series {m n p:ℤ} (hmn: m ≤ n+1) (hpn : n ≤ p) (a: ℤ → ℝ) :
  ∑ i ∈ Icc m n, a i + ∑ i ∈ Icc (n+1) p, a i = ∑ i ∈ Icc m p, a i := bym:ℤn:ℤp:ℤhmn:m ≤ n + 1hpn:n ≤ pa:ℤ → ℝ⊢ ∑ i ∈ Icc m n, a i + ∑ i ∈ Icc (n + 1) p, a i = ∑ i ∈ Icc m p, a i sorryAll goals completed! 🐙

Lemma 7.1.4(b) / Exercise 7.1.1

theorem declaration uses `sorry`shift_finite_series {m n k:ℤ} (a: ℤ → ℝ) :
  ∑ i ∈ Icc m n, a i = ∑ i ∈ Icc (m+k) (n+k), a (i-k) := bym:ℤn:ℤk:ℤa:ℤ → ℝ⊢ ∑ i ∈ Icc m n, a i = ∑ i ∈ Icc (m + k) (n + k), a (i - k) sorryAll goals completed! 🐙

Lemma 7.1.4(c) / Exercise 7.1.1

theorem declaration uses `sorry`finite_series_add {m n:ℤ} (a b: ℤ → ℝ) :
  ∑ i ∈ Icc m n, (a i + b i) = ∑ i ∈ Icc m n, a i + ∑ i ∈ Icc m n, b i := bym:ℤn:ℤa:ℤ → ℝb:ℤ → ℝ⊢ ∑ i ∈ Icc m n, (a i + b i) = ∑ i ∈ Icc m n, a i + ∑ i ∈ Icc m n, b i sorryAll goals completed! 🐙

Lemma 7.1.4(d) / Exercise 7.1.1

theorem declaration uses `sorry`finite_series_const_mul {m n:ℤ} (a: ℤ → ℝ) (c:ℝ) :
  ∑ i ∈ Icc m n, c * a i = c * ∑ i ∈ Icc m n, a i := bym:ℤn:ℤa:ℤ → ℝc:ℝ⊢ ∑ i ∈ Icc m n, c * a i = c * ∑ i ∈ Icc m n, a i sorryAll goals completed! 🐙

Lemma 7.1.4(e) / Exercise 7.1.1

theorem declaration uses `sorry`abs_finite_series_le {m n:ℤ} (a: ℤ → ℝ) :
  |∑ i ∈ Icc m n, a i| ≤ ∑ i ∈ Icc m n, |a i| := bym:ℤn:ℤa:ℤ → ℝ⊢ |∑ i ∈ Icc m n, a i| ≤ ∑ i ∈ Icc m n, |a i| sorryAll goals completed! 🐙

Lemma 7.1.4(f) / Exercise 7.1.1

theorem declaration uses `sorry`finite_series_of_le {m n:ℤ}  {a b: ℤ → ℝ} (h: ∀ i, m ≤ i → i ≤ n → a i ≤ b i) :
  ∑ i ∈ Icc m n, a i ≤ ∑ i ∈ Icc m n, b i := bym:ℤn:ℤa:ℤ → ℝb:ℤ → ℝh:∀ (i : ℤ), m ≤ i → i ≤ n → a i ≤ b i⊢ ∑ i ∈ Icc m n, a i ≤ ∑ i ∈ Icc m n, b i sorryAll goals completed! 🐙

Finset.sum_congr.{u_1, u_4} {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M}
  (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g#check sum_congr

Finset.sum_congr.{u_1, u_4} {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M}
  (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g

Proposition 7.1.8.

set_option maxHeartbeats 210000 in

theorem declaration uses `sorry`finite_series_of_rearrange {n:ℕ} {X':Type*} (X: Finset X') (hcard: X.card = n)
  (f: X' → ℝ) (g h: Icc (1:ℤ) n → X) (hg: Function.Bijective g) (hh: Function.Bijective h) :
    ∑ i ∈ Icc (1:ℤ) n, (if hi:i ∈ Icc (1:ℤ) n then f (g ⟨ i, hi ⟩) else 0)
    = ∑ i ∈ Icc (1:ℤ) n, (if hi: i ∈ Icc (1:ℤ) n then f (h ⟨ i, hi ⟩) else 0) := byn:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:↥(Icc 1 ↑n) → ↥Xh:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ghh:Function.Bijective h⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0
  -- This proof is written to broadly follow the structure of the original text.
  revert X nX':Type u_1f:X' → ℝ⊢ ∀ {n : ℕ} (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0; intro nX':Type u_1f:X' → ℝn:ℕ⊢ ∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0
  induction' n with n hnzeroX':Type u_1f:X' → ℝ⊢ ∀ (X : Finset X'),
  #X = 0 →
    ∀ (g h : ↥(Icc 1 ↑0) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑0, if hi : i ∈ Icc 1 ↑0 then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑0, if hi : i ∈ Icc 1 ↑0 then f ↑(h ⟨i, hi⟩) else 0succX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0⊢ ∀ (X : Finset X'),
  #X = n + 1 →
    ∀ (g h : ↥(Icc 1 ↑(n + 1)) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(h ⟨i, hi⟩) else 0
  .zeroX':Type u_1f:X' → ℝ⊢ ∀ (X : Finset X'),
  #X = 0 →
    ∀ (g h : ↥(Icc 1 ↑0) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑0, if hi : i ∈ Icc 1 ↑0 then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑0, if hi : i ∈ Icc 1 ↑0 then f ↑(h ⟨i, hi⟩) else 0 simpAll goals completed! 🐙
  intro X hXsuccX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1⊢ ∀ (g h : ↥(Icc 1 ↑(n + 1)) → ↥X),
  Function.Bijective g →
    Function.Bijective h →
      (∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(g ⟨i, hi⟩) else 0) =
        ∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(h ⟨i, hi⟩) else 0 gsuccX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥X⊢ ∀ (h : ↥(Icc 1 ↑(n + 1)) → ↥X),
  Function.Bijective g →
    Function.Bijective h →
      (∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(g ⟨i, hi⟩) else 0) =
        ∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(h ⟨i, hi⟩) else 0 hsuccX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥X⊢ Function.Bijective g →
  Function.Bijective h →
    (∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(g ⟨i, hi⟩) else 0) =
      ∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(h ⟨i, hi⟩) else 0 hgsuccX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective g⊢ Function.Bijective h →
  (∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(g ⟨i, hi⟩) else 0) =
    ∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(h ⟨i, hi⟩) else 0 hhsuccX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective h⊢ (∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(g ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑(n + 1), if hi : i ∈ Icc 1 ↑(n + 1) then f ↑(h ⟨i, hi⟩) else 0
  -- A technical step: we extend g, h to the entire integers using a slightly artificial map π
  set π : ℤ → Icc (1:ℤ) (n+1) :=
    fun i ↦ if hi: i ∈ Icc (1:ℤ) (n+1) then ⟨ i, hi ⟩ else ⟨ 1, byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hi:ℤhi:i ∉ Icc 1 (↑n + 1)⊢ 1 ∈ Icc 1 (↑n + 1) simpAll goals completed! 🐙 ⟩
  have hπ (g : Icc (1:ℤ) (n+1) → X) :
      ∑ i ∈ Icc (1:ℤ) (n+1), (if hi:i ∈ Icc (1:ℤ) (n+1) then f (g ⟨ i, hi ⟩) else 0)
      = ∑ i ∈ Icc (1:ℤ) (n+1), f (g (π i)) := byn:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:↥(Icc 1 ↑n) → ↥Xh:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ghh:Function.Bijective h⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0
    apply sum_congr rfl _X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g✝:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩g:↥(Icc 1 (↑n + 1)) → ↥X⊢ ∀ x ∈ Icc 1 (↑n + 1), (if hi : x ∈ Icc 1 (↑n + 1) then f ↑(g ⟨x, hi⟩) else 0) = f ↑(g (π x))
    intro i hiX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g✝:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩g:↥(Icc 1 (↑n + 1)) → ↥Xi:ℤhi:i ∈ Icc 1 (↑n + 1)⊢ (if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = f ↑(g (π i)); simp [hi, π, -mem_Icc]All goals completed! 🐙
  simp [-mem_Icc, hπ]succX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))⊢ ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i)) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i))
  rw [sum_of_nonempty (by linarith) _]succX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑(g (π (↑n + 1))) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i))
  set x := g (π (n+1))succX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i))
  have ⟨⟨j, hj'⟩, hj⟩ := hh.surjective xsuccX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = x⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i))
  simp at hj'succX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj'✝:j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj':1 ≤ j ∧ j ≤ ↑n + 1⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)); obtain ⟨ hj1, hj2 ⟩ := hj'succX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i))
  set h' : ℤ → X := fun i ↦ if (i:ℤ) < j then h (π i) else h (π (i+1))succX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i))
  have : ∑ i ∈ Icc (1:ℤ) (n + 1), f (h (π i)) = ∑ i ∈ Icc (1:ℤ) n, f (h' i) + f x := calc
    _ = ∑ i ∈ Icc (1:ℤ) j, f (h (π i)) + ∑ i ∈ Icc (j+1:ℤ) (n + 1), f (h (π i)) := byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 j, f ↑(h (π i)) + ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i))
      symmX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 j, f ↑(h (π i)) + ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)); apply concat_finite_serieshmnX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ 1 ≤ j + 1hpnX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j ≤ ↑n + 1 <;>hmnX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ 1 ≤ j + 1hpnX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j ≤ ↑n + 1 linarithAll goals completed! 🐙
    _ = ∑ i ∈ Icc (1:ℤ) (j-1), f (h (π i)) + f ( h (π j) )
        + ∑ i ∈ Icc (j+1:ℤ) (n + 1), f (h (π i)) := byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 j, f ↑(h (π i)) + ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) =
  ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) + ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i))
      congre_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 j, f ↑(h (π i)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)); convert sum_of_nonempty _ _h.e'_2.h.h.e'_5X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j = j - 1 + 1h.e'_3.h.e'_6.h.e'_1.h.e'_3.h.e'_1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ π j = π (j - 1 + 1)e_a.convert_3X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j - 1 ≥ 1 - 1 <;>h.e'_2.h.h.e'_5X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j = j - 1 + 1h.e'_3.h.e'_6.h.e'_1.h.e'_3.h.e'_1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ π j = π (j - 1 + 1)e_a.convert_3X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j - 1 ≥ 1 - 1 simp [hj1]All goals completed! 🐙
    _ = ∑ i ∈ Icc (1:ℤ) (j-1), f (h (π i)) + f x + ∑ i ∈ Icc (j:ℤ) n, f (h (π (i+1))) := byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) + ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) =
  ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑x + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1)))
      congr 1e_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑xe_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1)))
      .e_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑x simp [←hj, π,hj1, hj2]All goals completed! 🐙
      symme_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) = ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)); convert shift_finite_series _h.e'_3.a.h.e'_1.h.e'_3.h.e'_1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))x✝:ℤa✝:x✝ ∈ Icc (j + 1) (↑n + 1)⊢ π x✝ = π (x✝ - 1 + 1); simpAll goals completed! 🐙
    _ = ∑ i ∈ Icc (1:ℤ) (j-1), f (h (π i)) + ∑ i ∈ Icc (j:ℤ) n, f (h (π (i+1))) + f x := byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑x + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) =
  ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) + f ↑x abelAll goals completed! 🐙
    _ = ∑ i ∈ Icc (1:ℤ) (j-1), f (h' i) + ∑ i ∈ Icc (j:ℤ) n, f (h' i) + f x := byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) + f ↑x =
  ∑ i ∈ Icc 1 (j - 1), f ↑(h' i) + ∑ i ∈ Icc j ↑n, f ↑(h' i) + f ↑x
      congr 2e_a.e_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h' i)e_a.e_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) = ∑ i ∈ Icc j ↑n, f ↑(h' i)
      all_goals apply sum_congr rfl _X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∀ x ∈ Icc j ↑n, f ↑(h (π (x + 1))) = f ↑(h' x); intro i hiX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))i:ℤhi:i ∈ Icc j ↑n⊢ f ↑(h (π (i + 1))) = f ↑(h' i); simp [h'] at *X':Type u_1f:X' → ℝn:ℕX:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))i:ℤhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Multiset.map g (Icc 1 ↑n).val.attach = X.val.attach →
        Multiset.map h (Icc 1 ↑n).val.attach = X.val.attach →
          (∑ x ∈ Icc 1 ↑n, if h : 1 ≤ x ∧ x ≤ ↑n then f ↑(g ⟨x, ⋯⟩) else 0) =
            ∑ x ∈ Icc 1 ↑n, if h_1 : 1 ≤ x ∧ x ≤ ↑n then f ↑(h ⟨x, ⋯⟩) else 0hg:Multiset.map g (Icc 1 (↑n + 1)).val.attach = X.val.attachhh:Multiset.map h (Icc 1 (↑n + 1)).val.attach = X.val.attachhπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ x ∈ Icc 1 (↑n + 1), if h : 1 ≤ x ∧ x ≤ ↑n + 1 then f ↑(g ⟨x, ⋯⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))hi:j ≤ i ∧ i ≤ ↑n⊢ f ↑(h (π (i + 1))) = f ↑(if i < j then h (π i) else h (π (i + 1)))
      .X':Type u_1f:X' → ℝn:ℕX:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))i:ℤhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Multiset.map g (Icc 1 ↑n).val.attach = X.val.attach →
        Multiset.map h (Icc 1 ↑n).val.attach = X.val.attach →
          (∑ x ∈ Icc 1 ↑n, if h : 1 ≤ x ∧ x ≤ ↑n then f ↑(g ⟨x, ⋯⟩) else 0) =
            ∑ x ∈ Icc 1 ↑n, if h_1 : 1 ≤ x ∧ x ≤ ↑n then f ↑(h ⟨x, ⋯⟩) else 0hg:Multiset.map g (Icc 1 (↑n + 1)).val.attach = X.val.attachhh:Multiset.map h (Icc 1 (↑n + 1)).val.attach = X.val.attachhπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ x ∈ Icc 1 (↑n + 1), if h : 1 ≤ x ∧ x ≤ ↑n + 1 then f ↑(g ⟨x, ⋯⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))hi:1 ≤ i ∧ i < j⊢ f ↑(h (π i)) = f ↑(if i < j then h (π i) else h (π (i + 1))) simp [show i < j by linarith]All goals completed! 🐙
      simp [show ¬ i < j by linarith]All goals completed! 🐙
    _ = _ := byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h' i) + ∑ i ∈ Icc j ↑n, f ↑(h' i) + f ↑x = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑x congre_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h' i) + ∑ i ∈ Icc j ↑n, f ↑(h' i) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i); convert concat_finite_series _ _ _h.e'_2.h.e'_6.h.h.e'_4X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j = j - 1 + 1e_a.convert_4X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ 1 ≤ j - 1 + 1e_a.convert_5X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j - 1 ≤ ↑n <;>h.e'_2.h.e'_6.h.h.e'_4X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j = j - 1 + 1e_a.convert_4X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ 1 ≤ j - 1 + 1e_a.convert_5X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))⊢ j - 1 ≤ ↑n linarithAll goals completed! 🐙
  rw [this]succX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑x⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑x
  congr 1succ.e_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑x⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i)
  have g_ne_x {i:ℤ} (hi : i ∈ Icc (1:ℤ) n) : g (π i) ≠ x := byn:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:↥(Icc 1 ↑n) → ↥Xh:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ghh:Function.Bijective h⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0
    simp at hiX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xi:ℤhi:1 ≤ i ∧ i ≤ ↑n⊢ g (π i) ≠ x
    simp [x, hg.injective.eq_iff, π, hi.1, show i ≤ n+1 by linarith]X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xi:ℤhi:1 ≤ i ∧ i ≤ ↑n⊢ ¬i = ↑n + 1
    linarithAll goals completed! 🐙
  have h'_ne_x {i:ℤ} (hi : i ∈ Icc (1:ℤ) n) : h' i ≠ x := byn:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:↥(Icc 1 ↑n) → ↥Xh:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ghh:Function.Bijective h⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0
    simp at hiX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑n⊢ h' i ≠ x
    have hi' : 0 ≤ i := byn:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:↥(Icc 1 ↑n) → ↥Xh:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ghh:Function.Bijective h⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0 linarithAll goals completed! 🐙
    have hi'' : i ≤ n+1 := byn:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:↥(Icc 1 ↑n) → ↥Xh:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ghh:Function.Bijective h⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0 linarithAll goals completed! 🐙
    by_cases hlt: i < jposX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:i < j⊢ h' i ≠ xnegX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:¬i < j⊢ h' i ≠ x <;>posX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:i < j⊢ h' i ≠ xnegX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:¬i < j⊢ h' i ≠ x by_contra! heqnegX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:¬i < jheq:h' i = x⊢ False
    all_goals simp [h', hlt, ←hj, hh.injective.eq_iff, ←Subtype.val_inj,
                    π, hi.1, hi.2, hi',hi''] at heqnegX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:¬i < jheq:i + 1 = j⊢ False
    .posX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:i < jheq:i = j⊢ False linarithAll goals completed! 🐙
    contrapose! hltnegX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1heq:i + 1 = jhlt:True⊢ i < j; linarithAll goals completed! 🐙
  set gtil : Icc (1:ℤ) n → X.erase x :=
    fun i ↦ ⟨ (g (π i)).val, byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xi:↥(Icc 1 ↑n)⊢ ↑(g (π ↑i)) ∈ X.erase ↑x simp [mem_erase, g_ne_x]All goals completed! 🐙 ⟩
  set htil : Icc (1:ℤ) n → X.erase x :=
    fun i ↦ ⟨ (h' i).val, byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩i:↥(Icc 1 ↑n)⊢ ↑(h' ↑i) ∈ X.erase ↑x simp [mem_erase, h'_ne_x]All goals completed! 🐙 ⟩
  set ftil : X.erase x → ℝ := fun y ↦ f y.valsucc.e_aX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑y⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i)
  have why : Function.Bijective gtil := byn:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:↥(Icc 1 ↑n) → ↥Xh:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ghh:Function.Bijective h⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0 sorryAll goals completed! 🐙
  have why2 : Function.Bijective htil := byn:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:↥(Icc 1 ↑n) → ↥Xh:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ghh:Function.Bijective h⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0 sorryAll goals completed! 🐙
  calc
    _ = ∑ i ∈ Icc (1:ℤ) n, if hi: i ∈ Icc (1:ℤ) n then ftil (gtil ⟨ i, hi ⟩ ) else 0 := byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) = ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then ftil (gtil ⟨i, hi⟩) else 0
      apply sum_congr rflX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ ∀ x ∈ Icc 1 ↑n, f ↑(g (π x)) = if hi : x ∈ Icc 1 ↑n then ftil (gtil ⟨x, hi⟩) else 0; grindAll goals completed! 🐙
    _ = ∑ i ∈ Icc (1:ℤ) n, if hi: i ∈ Icc (1:ℤ) n then ftil (htil ⟨ i, hi ⟩ ) else 0 := byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then ftil (gtil ⟨i, hi⟩) else 0) =
  ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then ftil (htil ⟨i, hi⟩) else 0
      convert hn _ _ gtil htil why why2X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ #(X.erase ↑x) = n
      rw [Finset.card_erase_of_mem _, hX]X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ n + 1 - 1 = nX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ ↑x ∈ X <;>X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ n + 1 - 1 = nX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ ↑x ∈ X simpAll goals completed! 🐙
    _ = _ := byX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then ftil (htil ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) apply sum_congr rflX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'),
  #X = n →
    ∀ (g h : ↥(Icc 1 ↑n) → ↥X),
      Function.Bijective g →
        Function.Bijective h →
          (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) =
            ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(h ⟨i, hi⟩) else 0X:Finset X'hX:#X = n + 1g:↥(Icc 1 ↑(n + 1)) → ↥Xh:↥(Icc 1 ↑(n + 1)) → ↥Xhg:Function.Bijective ghh:Function.Bijective hπ:ℤ → ↥(Icc 1 (↑n + 1)) := fun i ↦ if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : ↥(Icc 1 (↑n + 1)) → ↥X),
  (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:↥X := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → ↥X := fun i ↦ if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(g (π ↑i)), ⋯⟩htil:↥(Icc 1 ↑n) → ↥(X.erase ↑x) := fun i ↦ ⟨↑(h' ↑i), ⋯⟩ftil:↥(X.erase ↑x) → ℝ := fun y ↦ f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ ∀ x ∈ Icc 1 ↑n, (if hi : x ∈ Icc 1 ↑n then ftil (htil ⟨x, hi⟩) else 0) = f ↑(h' x); grindAll goals completed! 🐙

This fact ensures that Definition 7.1.6 would be well-defined even if we did not appeal to the existing Finset.sum method.

theorem exist_bijection {n:ℕ} {Y:Type*} (X: Finset Y) (hcard: X.card = n) :
    ∃ g: Icc (1:ℤ) n → X, Function.Bijective g := byn:ℕY:Type u_1X:Finset Yhcard:#X = n⊢ ∃ g, Function.Bijective g
  have := Finset.equivOfCardEq (show (Icc (1:ℤ) n).card = X.card byn:ℕY:Type u_1X:Finset Yhcard:#X = n⊢ ∃ g, Function.Bijective g simp [hcard]All goals completed! 🐙)
  exact ⟨ this, this.bijective ⟩All goals completed! 🐙

Definition 7.1.6

theorem finite_series_eq {n:ℕ} {Y:Type*} (X: Finset Y) (f: Y → ℝ) (g: Icc (1:ℤ) n → X)
  (hg: Function.Bijective g) :
    ∑ i ∈ X, f i = ∑ i ∈ Icc (1:ℤ) n, (if hi:i ∈ Icc (1:ℤ) n then f (g ⟨ i, hi ⟩) else 0) := byn:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective g⊢ ∑ i ∈ X, f i = ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0
  symmn:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective g⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ X, f i
  convert sum_bij (t:=X) (fun i hi ↦ g ⟨ i, hi ⟩ ) _ _ _ _convert_5n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective g⊢ ∀ (a : ℤ) (ha : a ∈ Icc 1 ↑n), (fun i hi ↦ ↑(g ⟨i, hi⟩)) a ha ∈ Xconvert_6n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective g⊢ ∀ (a₁ : ℤ) (ha₁ : a₁ ∈ Icc 1 ↑n) (a₂ : ℤ) (ha₂ : a₂ ∈ Icc 1 ↑n),
  (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₁ ha₁ = (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₂ ha₂ → a₁ = a₂convert_7n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective g⊢ ∀ b ∈ X, ∃ a, ∃ (ha : a ∈ Icc 1 ↑n), (fun i hi ↦ ↑(g ⟨i, hi⟩)) a ha = bconvert_8n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective g⊢ ∀ (a : ℤ) (ha : a ∈ Icc 1 ↑n), (if hi : a ∈ Icc 1 ↑n then f ↑(g ⟨a, hi⟩) else 0) = f ((fun i hi ↦ ↑(g ⟨i, hi⟩)) a ha)
  .convert_5n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective g⊢ ∀ (a : ℤ) (ha : a ∈ Icc 1 ↑n), (fun i hi ↦ ↑(g ⟨i, hi⟩)) a ha ∈ X aesopAll goals completed! 🐙
  .convert_6n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective g⊢ ∀ (a₁ : ℤ) (ha₁ : a₁ ∈ Icc 1 ↑n) (a₂ : ℤ) (ha₂ : a₂ ∈ Icc 1 ↑n),
  (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₁ ha₁ = (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₂ ha₂ → a₁ = a₂ intro _ _convert_6n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ga₁✝:ℤha₁✝:a₁✝ ∈ Icc 1 ↑n⊢ ∀ (a₂ : ℤ) (ha₂ : a₂ ∈ Icc 1 ↑n), (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₁✝ ha₁✝ = (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₂ ha₂ → a₁✝ = a₂ _convert_6n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ga₁✝:ℤha₁✝:a₁✝ ∈ Icc 1 ↑na₂✝:ℤ⊢ ∀ (ha₂ : a₂✝ ∈ Icc 1 ↑n), (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₁✝ ha₁✝ = (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₂✝ ha₂ → a₁✝ = a₂✝ _convert_6n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ga₁✝:ℤha₁✝:a₁✝ ∈ Icc 1 ↑na₂✝:ℤha₂✝:a₂✝ ∈ Icc 1 ↑n⊢ (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₁✝ ha₁✝ = (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₂✝ ha₂✝ → a₁✝ = a₂✝ hconvert_6n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ga₁✝:ℤha₁✝:a₁✝ ∈ Icc 1 ↑na₂✝:ℤha₂✝:a₂✝ ∈ Icc 1 ↑nh:(fun i hi ↦ ↑(g ⟨i, hi⟩)) a₁✝ ha₁✝ = (fun i hi ↦ ↑(g ⟨i, hi⟩)) a₂✝ ha₂✝⊢ a₁✝ = a₂✝; simpa [Subtype.val_inj, hg.injective.eq_iff] using hAll goals completed! 🐙
  .convert_7n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective g⊢ ∀ b ∈ X, ∃ a, ∃ (ha : a ∈ Icc 1 ↑n), (fun i hi ↦ ↑(g ⟨i, hi⟩)) a ha = b intro b hbconvert_7n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective gb:Yhb:b ∈ X⊢ ∃ a, ∃ (ha : a ∈ Icc 1 ↑n), (fun i hi ↦ ↑(g ⟨i, hi⟩)) a ha = b; have := hg.surjective ⟨ b, hb ⟩convert_7n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective gb:Yhb:b ∈ Xthis:∃ a, g a = ⟨b, hb⟩⊢ ∃ a, ∃ (ha : a ∈ Icc 1 ↑n), (fun i hi ↦ ↑(g ⟨i, hi⟩)) a ha = b; grindAll goals completed! 🐙
  introsconvert_8n:ℕY:Type u_1X:Finset Yf:Y → ℝg:↥(Icc 1 ↑n) → ↥Xhg:Function.Bijective ga✝:ℤha✝:a✝ ∈ Icc 1 ↑n⊢ (if hi : a✝ ∈ Icc 1 ↑n then f ↑(g ⟨a✝, hi⟩) else 0) = f ((fun i hi ↦ ↑(g ⟨i, hi⟩)) a✝ ha✝); simp_allAll goals completed! 🐙

Proposition 7.1.11(a) / Exercise 7.1.2

theorem declaration uses `sorry`finite_series_of_empty {X':Type*} (f: X' → ℝ) : ∑ i ∈ ∅, f i = 0 := byX':Type u_1f:X' → ℝ⊢ ∑ i ∈ ∅, f i = 0 sorryAll goals completed! 🐙

Proposition 7.1.11(b) / Exercise 7.1.2

theorem declaration uses `sorry`finite_series_of_singleton {X':Type*} (f: X' → ℝ) (x₀:X') : ∑ i ∈ {x₀}, f i = f x₀ := byX':Type u_1f:X' → ℝx₀:X'⊢ ∑ i ∈ {x₀}, f i = f x₀
  sorryAll goals completed! 🐙

A technical lemma relating a sum over a finset with a sum over a fintype. Combines well with tools such as map_finite_series below.

theorem finite_series_of_fintype {X':Type*} (f: X' → ℝ) (X: Finset X') :
    ∑ x ∈ X, f x = ∑ x:X, f x.val := (sum_coe_sort X f).symm

Proposition 7.1.11(c) / Exercise 7.1.2

theorem declaration uses `sorry`map_finite_series {X:Type*} [Fintype X] [Fintype Y] (f: X → ℝ) {g:Y → X}
  (hg: Function.Bijective g) :
    ∑ x, f x = ∑ y, f (g y) := byY:Type u_2X:Type u_1inst✝¹:Fintype Xinst✝:Fintype Yf:X → ℝg:Y → Xhg:Function.Bijective g⊢ ∑ x, f x = ∑ y, f (g y) sorryAll goals completed! 🐙

Proposition 7.1.11(e) / Exercise 7.1.2

-- Proposition 7.1.11(d) is `rfl` in our formalism and is therefore omitted.

theorem declaration uses `sorry`finite_series_of_disjoint_union {Z:Type*} {X Y: Finset Z} (hdisj: Disjoint X Y) (f: Z → ℝ) :
    ∑ z ∈ X ∪ Y, f z = ∑ z ∈ X, f z + ∑ z ∈ Y, f z := byZ:Type u_1X:Finset ZY:Finset Zhdisj:Disjoint X Yf:Z → ℝ⊢ ∑ z ∈ X ∪ Y, f z = ∑ z ∈ X, f z + ∑ z ∈ Y, f z sorryAll goals completed! 🐙

Proposition 7.1.11(f) / Exercise 7.1.2

theorem declaration uses `sorry`finite_series_of_add {X':Type*} (f g: X' → ℝ) (X: Finset X') :
    ∑ x ∈ X, (f + g) x = ∑ x ∈ X, f x + ∑ x ∈ X, g x := byX':Type u_1f:X' → ℝg:X' → ℝX:Finset X'⊢ ∑ x ∈ X, (f + g) x = ∑ x ∈ X, f x + ∑ x ∈ X, g x sorryAll goals completed! 🐙

Proposition 7.1.11(g) / Exercise 7.1.2

theorem declaration uses `sorry`finite_series_of_const_mul {X':Type*} (f: X' → ℝ) (X: Finset X') (c:ℝ) :
    ∑ x ∈ X, c * f x = c * ∑ x ∈ X, f x := byX':Type u_1f:X' → ℝX:Finset X'c:ℝ⊢ ∑ x ∈ X, c * f x = c * ∑ x ∈ X, f x sorryAll goals completed! 🐙

Proposition 7.1.11(h) / Exercise 7.1.2

theorem declaration uses `sorry`finite_series_of_le' {X':Type*} (f g: X' → ℝ) (X: Finset X') (h: ∀ x ∈ X, f x ≤ g x) :
    ∑ x ∈ X, f x ≤ ∑ x ∈ X, g x := byX':Type u_1f:X' → ℝg:X' → ℝX:Finset X'h:∀ x ∈ X, f x ≤ g x⊢ ∑ x ∈ X, f x ≤ ∑ x ∈ X, g x sorryAll goals completed! 🐙

Proposition 7.1.11(i) / Exercise 7.1.2

theorem declaration uses `sorry`abs_finite_series_le' {X':Type*} (f: X' → ℝ) (X: Finset X') :
    |∑ x ∈ X, f x| ≤ ∑ x ∈ X, |f x| := byX':Type u_1f:X' → ℝX:Finset X'⊢ |∑ x ∈ X, f x| ≤ ∑ x ∈ X, |f x| sorryAll goals completed! 🐙

Lemma 7.1.13 -

theorem declaration uses `sorry`finite_series_of_finite_series {XX YY:Type*} (X: Finset XX) (Y: Finset YY)
  (f: XX × YY → ℝ) :
    ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z := byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z
  generalize h: X.card = nXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝn:ℕh:#X = n⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z
  revert XXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕ⊢ ∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z; induction' n with n hnzeroXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝ⊢ ∀ (X : Finset XX), #X = 0 → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zsuccXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z⊢ ∀ (X : Finset XX), #X = n + 1 → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z
  .zeroXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝ⊢ ∀ (X : Finset XX), #X = 0 → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z sorryAll goals completed! 🐙
  intro X hXsuccXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z
  have hnon : X.Nonempty := byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z grind [card_ne_zero]All goals completed! 🐙
  choose x₀ hx₀ using hnon.exists_memsuccXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ X⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z
  set X' := X.erase x₀succXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z
  have hcard : X'.card = n := byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z simp [X', card_erase_of_mem hx₀, hX]All goals completed! 🐙
  have hunion : X = X' ∪ {x₀} := byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z ext xhXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nx:XX⊢ x ∈ X ↔ x ∈ X' ∪ {x₀}; by_cases x = x₀posXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nx:XXh✝:x = x₀⊢ x ∈ X ↔ x ∈ X' ∪ {x₀}negXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nx:XXh✝:¬x = x₀⊢ x ∈ X ↔ x ∈ X' ∪ {x₀} <;>posXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nx:XXh✝:x = x₀⊢ x ∈ X ↔ x ∈ X' ∪ {x₀}negXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nx:XXh✝:¬x = x₀⊢ x ∈ X ↔ x ∈ X' ∪ {x₀} grindAll goals completed! 🐙
  have hdisj : Disjoint X' {x₀} := byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z simp [X']All goals completed! 🐙
  calc
    _ = ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ x ∈ {x₀}, ∑ y ∈ Y, f (x, y) := byXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ x ∈ {x₀}, ∑ y ∈ Y, f (x, y)
      convert finite_series_of_disjoint_union hdisj _All goals completed! 🐙
    _ = ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ y ∈ Y, f (x₀, y) := byXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ x ∈ {x₀}, ∑ y ∈ Y, f (x, y) = ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ y ∈ Y, f (x₀, y)
      rw [finite_series_of_singleton]All goals completed! 🐙
    _ = ∑ z ∈ X'.product Y, f z + ∑ y ∈ Y, f (x₀, y) := byXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ y ∈ Y, f (x₀, y) = ∑ z ∈ X'.product Y, f z + ∑ y ∈ Y, f (x₀, y) rw [hn X' hcard]All goals completed! 🐙
    _ = ∑ z ∈ X'.product Y, f z + ∑ z ∈ .product {x₀} Y, f z := byXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ z ∈ X'.product Y, f z + ∑ y ∈ Y, f (x₀, y) = ∑ z ∈ X'.product Y, f z + ∑ z ∈ {x₀}.product Y, f z
      congr 1e_aXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ y ∈ Y, f (x₀, y) = ∑ z ∈ {x₀}.product Y, f z
      rw [finite_series_of_fintype, finite_series_of_fintype f]e_aXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ x, f (x₀, ↑x) = ∑ x, f ↑x
      set π : Finset.product {x₀} Y → Y :=
        fun z ↦ ⟨ z.val.2, byXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}z:↥({x₀}.product Y)⊢ (↑z).2 ∈ Y obtain ⟨ z, hz ⟩ := zXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}z:XX × YYhz:z ∈ {x₀}.product Y⊢ (↑⟨z, hz⟩).2 ∈ Y; simp at hz ⊢XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}z:XX × YYhz:∃ a ∈ Y, (x₀, a) = z⊢ z.2 ∈ Y; grindAll goals completed! 🐙 ⟩
      have hπ : Function.Bijective π := byXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ z ∈ X'.product Y, f z + ∑ y ∈ Y, f (x₀, y) = ∑ z ∈ X'.product Y, f z + ∑ z ∈ {x₀}.product Y, f z
        constructorleftXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩⊢ Function.Injective πrightXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩⊢ Function.Surjective π
        .leftXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩⊢ Function.Injective π intro ⟨ ⟨ x, y ⟩, hz ⟩ ⟨ ⟨ x', y' ⟩, hz' ⟩leftXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩x:XXy:YYhz:(x, y) ∈ {x₀}.product Yx':XXy':YYhz':(x', y') ∈ {x₀}.product Y⊢ π ⟨(x, y), hz⟩ = π ⟨(x', y'), hz'⟩ → ⟨(x, y), hz⟩ = ⟨(x', y'), hz'⟩ hzz'leftXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩x:XXy:YYhz:(x, y) ∈ {x₀}.product Yx':XXy':YYhz':(x', y') ∈ {x₀}.product Yhzz':π ⟨(x, y), hz⟩ = π ⟨(x', y'), hz'⟩⊢ ⟨(x, y), hz⟩ = ⟨(x', y'), hz'⟩; simp [π] at hz hz' hzz' ⊢leftXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩x:XXy:YYx':XXy':YYhz:y ∈ Y ∧ x₀ = xhz':y' ∈ Y ∧ x₀ = x'hzz':y = y'⊢ x = x' ∧ y = y'; grindAll goals completed! 🐙
        intro ⟨ y, hy ⟩rightXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩y:YYhy:y ∈ Y⊢ ∃ a, π a = ⟨y, hy⟩; use ⟨ (x₀, y), byXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩y:YYhy:y ∈ Y⊢ (x₀, y) ∈ {x₀}.product Y simp [hy]All goals completed! 🐙 ⟩
      convert map_finite_series _ hπ with zh.e'_3.a.h.e'_1.h.e'_3XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩hπ:Function.Bijective πz:↥({x₀}.product Y)a✝:z ∈ univ⊢ z.1.1 = x₀
      obtain ⟨⟨x, y⟩, hz ⟩ := zh.e'_3.a.h.e'_1.h.e'_3XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩hπ:Function.Bijective πx:XXy:YYhz:(x, y) ∈ {x₀}.product Ya✝:⟨(x, y), hz⟩ ∈ univ⊢ ⟨(x, y), hz⟩.1.1 = x₀
      simp at hz ⊢h.e'_3.a.h.e'_1.h.e'_3XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:↥({x₀}.product Y) → ↥Y := fun z ↦ ⟨(↑z).2, ⋯⟩hπ:Function.Bijective πx:XXy:YYhz✝:(x, y) ∈ {x₀}.product Ya✝:⟨(x, y), hz⟩ ∈ univhz:y ∈ Y ∧ x₀ = x⊢ x = x₀; grindAll goals completed! 🐙
    _ = _ := byXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ z ∈ X'.product Y, f z + ∑ z ∈ {x₀}.product Y, f z = ∑ z ∈ X.product Y, f z
      symmXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ z ∈ X.product Y, f z = ∑ z ∈ X'.product Y, f z + ∑ z ∈ {x₀}.product Y, f z; convert finite_series_of_disjoint_union _ _h.e'_2.hXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ X.product Y = X'.product Y ∪ {x₀}.product Yconvert_4XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ Disjoint (X'.product Y) ({x₀}.product Y)
      .h.e'_2.hXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ X.product Y = X'.product Y ∪ {x₀}.product Y sorryAll goals completed! 🐙
      sorryAll goals completed! 🐙

Corollary 7.1.14 (Fubini's theorem for finite series)

theorem finite_series_refl {XX YY:Type*} (X: Finset XX) (Y: Finset YY) (f: XX × YY → ℝ) :
    ∑ z ∈ X.product Y, f z = ∑ z ∈ Y.product X, f (z.2, z.1) := byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ z ∈ X.product Y, f z = ∑ z ∈ Y.product X, f (z.2, z.1)
  set h : Y.product X → X.product Y :=
    fun z ↦ ⟨ (z.val.2, z.val.1), byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝz:↥(Y.product X)⊢ ((↑z).2, (↑z).1) ∈ X.product Y obtain ⟨ z, hz ⟩ := zXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝz:YY × XXhz:z ∈ Y.product X⊢ ((↑⟨z, hz⟩).2, (↑⟨z, hz⟩).1) ∈ X.product Y; simp at hz ⊢XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝz:YY × XXhz:z.1 ∈ Y ∧ z.2 ∈ X⊢ z.2 ∈ X ∧ z.1 ∈ Y; tautoAll goals completed! 🐙 ⟩
  have hh : Function.Bijective h := byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ z ∈ X.product Y, f z = ∑ z ∈ Y.product X, f (z.2, z.1)
    constructorleftXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩⊢ Function.Injective hrightXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩⊢ Function.Surjective h
    .leftXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩⊢ Function.Injective h intro ⟨ ⟨ _, _ ⟩, _ ⟩ ⟨ ⟨ _, _ ⟩, _ ⟩leftXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩fst✝¹:YYsnd✝¹:XXproperty✝¹:(fst✝¹, snd✝¹) ∈ Y.product Xfst✝:YYsnd✝:XXproperty✝:(fst✝, snd✝) ∈ Y.product X⊢ h ⟨(fst✝¹, snd✝¹), property✝¹⟩ = h ⟨(fst✝, snd✝), property✝⟩ → ⟨(fst✝¹, snd✝¹), property✝¹⟩ = ⟨(fst✝, snd✝), property✝⟩ _leftXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩fst✝¹:YYsnd✝¹:XXproperty✝¹:(fst✝¹, snd✝¹) ∈ Y.product Xfst✝:YYsnd✝:XXproperty✝:(fst✝, snd✝) ∈ Y.product Xa✝:h ⟨(fst✝¹, snd✝¹), property✝¹⟩ = h ⟨(fst✝, snd✝), property✝⟩⊢ ⟨(fst✝¹, snd✝¹), property✝¹⟩ = ⟨(fst✝, snd✝), property✝⟩
      simp_all [h]All goals completed! 🐙
    intro ⟨ z, hz ⟩rightXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩z:XX × YYhz:z ∈ X.product Y⊢ ∃ a, h a = ⟨z, hz⟩; simp at hzrightXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩z:XX × YYhz✝:z ∈ X.product Yhz:z.1 ∈ X ∧ z.2 ∈ Y⊢ ∃ a, h a = ⟨z, hz⟩
    use ⟨ (z.2, z.1), byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩z:XX × YYhz✝:z ∈ X.product Yhz:z.1 ∈ X ∧ z.2 ∈ Y⊢ (z.2, z.1) ∈ Y.product X simp [hz]All goals completed! 🐙 ⟩
  rw [finite_series_of_fintype]XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩hh:Function.Bijective h⊢ ∑ x, f ↑x = ∑ z ∈ Y.product X, f (z.2, z.1)
  nth_rewrite 2 [finite_series_of_fintype]XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:↥(Y.product X) → ↥(X.product Y) := fun z ↦ ⟨((↑z).2, (↑z).1), ⋯⟩hh:Function.Bijective h⊢ ∑ x, f ↑x = ∑ x, f ((↑x).2, (↑x).1)
  convert map_finite_series _ hh with zAll goals completed! 🐙

theorem finite_series_comm {XX YY:Type*} (X: Finset XX) (Y: Finset YY) (f: XX × YY → ℝ) :
    ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ y ∈ Y, ∑ x ∈ X, f (x, y) := byXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ y ∈ Y, ∑ x ∈ X, f (x, y)
  rw [finite_series_of_finite_series, finite_series_refl,
      finite_series_of_finite_series _ _ (fun z ↦ f (z.2, z.1))]All goals completed! 🐙

-- Exercise 7.1.3 : develop as many analogues as you can of the above theory for finite products
-- instead of finite sums.

Nat.factorial_zero : Nat.factorial 0 = 1#check Nat.factorial_zero

Nat.factorial_succ (n : ℕ) : (n + 1).factorial = (n + 1) * n.factorial#check Nat.factorial_succ

Nat.factorial_succ (n : ℕ) : (n + 1).factorial = (n + 1) * n.factorial

Exercise 7.1.4. Note: there may be some technicalities passing back and forth between natural numbers and integers. Look into the tactics zify, norm_cast, and omega

theorem declaration uses `sorry`binomial_theorem (x y:ℝ) (n:ℕ) :
    (x + y)^n
    = ∑ j ∈ Icc (0:ℤ) n,
    n.factorial / (j.toNat.factorial * (n-j).toNat.factorial) * x^j * y^(n - j) := byx:ℝy:ℝn:ℕ⊢ (x + y) ^ n = ∑ j ∈ Icc 0 ↑n, ↑n.factorial / (↑j.toNat.factorial * ↑(↑n - j).toNat.factorial) * x ^ j * y ^ (↑n - j)
  sorryAll goals completed! 🐙

Exercise 7.1.5

theorem declaration uses `sorry`lim_of_finite_series {X:Type*} [Fintype X] (a: X → ℕ → ℝ) (L : X → ℝ)
  (h: ∀ x, Filter.atTop.Tendsto (a x) (nhds (L x))) :
    Filter.atTop.Tendsto (fun n ↦ ∑ x, a x n) (nhds (∑ x, L x)) := byX:Type u_1inst✝:Fintype Xa:X → ℕ → ℝL:X → ℝh:∀ (x : X), Filter.Tendsto (a x) Filter.atTop (nhds (L x))⊢ Filter.Tendsto (fun n ↦ ∑ x, a x n) Filter.atTop (nhds (∑ x, L x))
  sorryAll goals completed! 🐙

Exercise 7.1.6

theorem declaration uses `sorry`sum_union_disjoint {n : ℕ} {S : Type*} [Fintype S]
    (E : Fin n → Finset S)
    (disj : ∀ i j : Fin n, i ≠ j → Disjoint (E i) (E j))
    (cover : ∀ s : S, ∃ i, s ∈ E i)
    (f : S → ℝ) :
    ∑ s, f s = ∑ i, ∑ s ∈ E i, f s := byn:ℕS:Type u_1inst✝:Fintype SE:Fin n → Finset Sdisj:∀ (i j : Fin n), i ≠ j → Disjoint (E i) (E j)cover:∀ (s : S), ∃ i, s ∈ E if:S → ℝ⊢ ∑ s, f s = ∑ i, ∑ s ∈ E i, f s
  sorryAll goals completed! 🐙

aᵢ Exercise 7.1.7. Uses Fin m (so aᵢ < m) instead of the book's aᵢ ≤ m; the bound is baked into the type, and < replaces ≤ to match the 0-indexed shift.

theorem declaration uses `sorry`sum_finite_col_row_counts {n m : ℕ} (a : Fin n → Fin m) :
    ∑ i, (a i : ℕ) = ∑ j : Fin m, {i : Fin n | j < a i}.toFinset.card := byn:ℕm:ℕa:Fin n → Fin m⊢ ∑ i, ↑(a i) = ∑ j, #{i | j < a i}.toFinset
  sorryAll goals completed! 🐙

end Finset