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

We do not attempt to replicate the full API for Finset.sum.{u_1, u_3} {ι : Type u_1} {M : Type u_3} [AddCommMonoid M] (s : Finset ι) (f : ι → M) : MFinset.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
Finset.mem_Icc.{u_1} {α : Type u_1} [Preorder α] [LocallyFiniteOrder α] {a b x : α} : x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b

Definition 7.1.1

theorem sum_of_empty {n m:ℤ} (h: n < m) (a: ℤ → ℝ) : ∑ i ∈ Icc m n, a i = 0 := n:ℤm:ℤh:n < ma:ℤ → ℝ⊢ ∑ i ∈ Icc m n, a i = 0 n:ℤm:ℤh:n < ma:ℤ → ℝ⊢ ∀ x ∈ Icc m n, a x = 0; n:ℤm:ℤh:n < ma:ℤ → ℝx✝:ℤ⊢ x✝ ∈ Icc m n → a x✝ = 0; n:ℤm:ℤh:n < ma:ℤ → ℝx✝:ℤ⊢ m ≤ x✝ ∧ x✝ ≤ n → a x✝ = 0; All goals completed! 🐙

Definition 7.1.1. This is similar to Mathlib's Finset.sum_Icc_succ_top.{u_3} {M : Type u_3} [AddCommMonoid M] {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) : ∑ k ∈ Icc a (b + 1), f k = ∑ k ∈ Icc a b, f k + f (b + 1)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) := n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ ∑ i ∈ Icc m (n + 1), a i = ∑ i ∈ Icc m n, a i + 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 n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ Icc m (n + 1) = insert (n + 1) (Icc m n)n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ DecidableEq ℤn:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ n + 1 ∉ Icc m n n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ Icc m (n + 1) = insert (n + 1) (Icc m n) n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝa✝:ℤ⊢ a✝ ∈ Icc m (n + 1) ↔ a✝ ∈ insert (n + 1) (Icc m n); n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝa✝:ℤ⊢ m ≤ a✝ ∧ a✝ ≤ n + 1 ↔ a✝ = n + 1 ∨ m ≤ a✝ ∧ a✝ ≤ n; All goals completed! 🐙 n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝ⊢ DecidableEq ℤ All goals completed! 🐙 All goals completed! 🐙
declaration uses 'sorry'example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m (m-2), a i = 0 := a:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m (m - 2), a i = 0 All goals completed! 🐙declaration uses 'sorry'example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m (m-1), a i = 0 := a:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m (m - 1), a i = 0 All goals completed! 🐙declaration uses 'sorry'example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m m, a i = a m := a:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m m, a i = a m All goals completed! 🐙declaration uses 'sorry'example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m (m+1), a i = a m + a (m+1) := a:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m (m + 1), a i = a m + a (m + 1) All goals completed! 🐙declaration uses 'sorry'example (a: ℤ → ℝ) (m:ℤ) : ∑ i ∈ Icc m (m+2), a i = a m + a (m+1) + a (m+2) := a:ℤ → ℝm:ℤ⊢ ∑ i ∈ Icc m (m + 2), a i = a m + a (m + 1) + a (m + 2) All 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 := m:ℤ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 All 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) := m:ℤn:ℤk:ℤa:ℤ → ℝ⊢ ∑ i ∈ Icc m n, a i = ∑ i ∈ Icc (m + k) (n + k), a (i - k) All 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 := m:ℤn:ℤa:ℤ → ℝb:ℤ → ℝ⊢ ∑ i ∈ Icc m n, (a i + b i) = ∑ i ∈ Icc m n, a i + ∑ i ∈ Icc m n, b i All 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 := m:ℤn:ℤa:ℤ → ℝc:ℝ⊢ ∑ i ∈ Icc m n, c * a i = c * ∑ i ∈ Icc m n, a i All goals completed! 🐙

Lemma 7.1.4(e) / Exercise 7.1.1

theorem declaration uses 'sorry'abs_finite_series_le {m n:ℤ} (a: ℤ → ℝ) (c:ℝ) : |∑ i ∈ Icc m n, a i| ≤ ∑ i ∈ Icc m n, |a i| := m:ℤn:ℤa:ℤ → ℝc:ℝ⊢ |∑ i ∈ Icc m n, a i| ≤ ∑ i ∈ Icc m n, |a i| All 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 := 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 All 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

Proposition 7.1.8.

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) := n:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg: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. X':Type u_1f:X' → ℝ⊢ ∀ {n : ℕ} (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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':Type u_1f:X' → ℝn:ℕ⊢ ∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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':Type u_1f:X' → ℝ⊢ ∀ (X : Finset X'), #X = 0 → ∀ (g h : { x // x ∈ Icc 1 ↑0 } → { x // x ∈ 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 0X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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 : { x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ 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 X':Type u_1f:X' → ℝ⊢ ∀ (X : Finset X'), #X = 0 → ∀ (g h : { x // x ∈ Icc 1 ↑0 } → { x // x ∈ 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 All goals completed! 🐙 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg: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, X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hi:ℤhi:i ∉ Icc 1 (↑n + 1)⊢ 1 ∈ Icc 1 (↑n + 1) All 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)) := n:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg: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 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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✝:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective g✝hh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩g:{ x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }⊢ ∀ x ∈ Icc 1 (↑n + 1), (if hi : x ∈ Icc 1 (↑n + 1) then f ↑(g ⟨x, hi⟩) else 0) = f ↑(g (π x)) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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✝:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective g✝hh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩g:{ x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }i:ℤhi:i ∈ Icc 1 (↑n + 1)⊢ (if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = f ↑(g (π i)); All goals completed! 🐙 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 g⊢ ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i)) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 g⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑(g (π (↑n + 1))) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 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)) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 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)); X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 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)) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (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)) := X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (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)) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (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)); X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ 1 ≤ j + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j ≤ ↑n + 1 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ 1 ≤ j + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j ≤ ↑n + 1 All goals completed! 🐙 _ = ∑ i ∈ Icc (1:ℤ) (j-1), f (h (π i)) + f (h (π j) ) + ∑ i ∈ Icc (j+1:ℤ) (n + 1), f (h (π i)) := X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (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)) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ ∑ i ∈ Icc 1 j, f ↑(h (π i)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)); X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j = j - 1 + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j = j - 1 + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j - 1 ≥ 1 - 1 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j = j - 1 + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j = j - 1 + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j - 1 ≥ 1 - 1 All goals completed! 🐙 _ = ∑ i ∈ Icc (1:ℤ) (j-1), f (h (π i)) + f x + ∑ i ∈ Icc (j:ℤ) n, f (h (π (i+1))) := X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (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))) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑xX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑x All goals completed! 🐙 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) = ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)); X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))x✝:ℤa✝:x✝ ∈ Icc (j + 1) (↑n + 1)⊢ x✝ = x✝ - 1 + 1; All goals completed! 🐙 _ = ∑ i ∈ Icc (1:ℤ) (j-1), f (h (π i)) + ∑ i ∈ Icc (j:ℤ) n, f (h (π (i+1))) + f x := X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (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 All goals completed! 🐙 _ = ∑ i ∈ Icc (1:ℤ) (j-1), f (h' i) + ∑ i ∈ Icc (j:ℤ) n, f (h' i) + f x := X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (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 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h' i)X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) = ∑ i ∈ Icc j ↑n, f ↑(h' i) all_goals X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ ∀ x ∈ Icc j ↑n, f ↑(h (π (x + 1))) = f ↑(h' x); X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))i:ℤhi:i ∈ Icc j ↑n⊢ f ↑(h (π (i + 1))) = f ↑(h' i); X':Type u_1f:X' → ℝn:ℕX:Finset X'hX:#X = n + 1g:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }π:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))i:ℤhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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 : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }π:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))i:ℤhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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 : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ 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 - 1⊢ f ↑(h (π i)) = f ↑(if i < j then h (π i) else h (π (i + 1))) All goals completed! 🐙 All goals completed! 🐙 _ = _ := X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (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 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h' i) + ∑ i ∈ Icc j ↑n, f ↑(h' i) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i); X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j = j - 1 + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ 1 ≤ j - 1 + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j - 1 ≤ ↑n X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j = j - 1 + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ 1 ≤ j - 1 + 1X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => Finset.sum_congr rfl fun i hi => of_eq_true (Eq.trans (congr (congrArg Eq (dite_cond_eq_true (eq_true hi))) (congrArg (fun x => @_fvar.21838 ↑(g x)) (dite_cond_eq_true (eq_true hi)))) (eq_self (@_fvar.21838 ↑(g ⟨i, of_eq_true (eq_true hi)⟩))))x:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))⊢ j - 1 ≤ ↑n All goals completed! 🐙 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑x X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453⊢ ∑ 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 := n:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg: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 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453i:ℤhi:1 ≤ i ∧ i ≤ ↑n⊢ g (π i) ≠ x X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453i:ℤhi:1 ≤ i ∧ i ≤ ↑n⊢ ¬i = ↑n + 1 All goals completed! 🐙 have h'_ne_x {i:ℤ} (hi : i ∈ Icc (1:ℤ) n) : h' i ≠ x := n:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg: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 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453g_ne_x:∀ {i : ℤ}, i ∈ Finset.Icc 1 ↑_fvar.21871 → @_fvar.35788 (@_fvar.39754 i) ≠ _fvar.50426 := fun {i} hi => @?_mvar.658108 i hii:ℤhi:1 ≤ i ∧ i ≤ ↑n⊢ h' i ≠ x have hi' : 0 ≤ i := n:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg: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 All goals completed! 🐙 have hi'' : i ≤ n+1 := n:ℕX':Type u_1X:Finset X'hcard:#X = nf:X' → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg: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 All goals completed! 🐙 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453g_ne_x:∀ {i : ℤ}, i ∈ Finset.Icc 1 ↑_fvar.21871 → @_fvar.35788 (@_fvar.39754 i) ≠ _fvar.50426 := fun {i} hi => @?_mvar.658108 i hii:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ _fvar.678801 := ?_mvar.681208hi'':_fvar.678801 ≤ ↑_fvar.21871 + 1 := ?_mvar.686500hlt:i < j⊢ h' i ≠ xX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453g_ne_x:∀ {i : ℤ}, i ∈ Finset.Icc 1 ↑_fvar.21871 → @_fvar.35788 (@_fvar.39754 i) ≠ _fvar.50426 := fun {i} hi => @?_mvar.658108 i hii:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ _fvar.678801 := ?_mvar.681208hi'':_fvar.678801 ≤ ↑_fvar.21871 + 1 := ?_mvar.686500hlt:¬i < j⊢ h' i ≠ x X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453g_ne_x:∀ {i : ℤ}, i ∈ Finset.Icc 1 ↑_fvar.21871 → @_fvar.35788 (@_fvar.39754 i) ≠ _fvar.50426 := fun {i} hi => @?_mvar.658108 i hii:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ _fvar.678801 := ?_mvar.681208hi'':_fvar.678801 ≤ ↑_fvar.21871 + 1 := ?_mvar.686500hlt:i < j⊢ h' i ≠ xX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453g_ne_x:∀ {i : ℤ}, i ∈ Finset.Icc 1 ↑_fvar.21871 → @_fvar.35788 (@_fvar.39754 i) ≠ _fvar.50426 := fun {i} hi => @?_mvar.658108 i hii:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ _fvar.678801 := ?_mvar.681208hi'':_fvar.678801 ≤ ↑_fvar.21871 + 1 := ?_mvar.686500hlt:¬i < j⊢ h' i ≠ x X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453g_ne_x:∀ {i : ℤ}, i ∈ Finset.Icc 1 ↑_fvar.21871 → @_fvar.35788 (@_fvar.39754 i) ≠ _fvar.50426 := fun {i} hi => @?_mvar.658108 i hii:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ _fvar.678801 := ?_mvar.681208hi'':_fvar.678801 ≤ ↑_fvar.21871 + 1 := ?_mvar.686500hlt:¬i < jheq:h' i = x⊢ False all_goals X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453g_ne_x:∀ {i : ℤ}, i ∈ Finset.Icc 1 ↑_fvar.21871 → @_fvar.35788 (@_fvar.39754 i) ≠ _fvar.50426 := fun {i} hi => @?_mvar.658108 i hii:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ _fvar.678801 := ?_mvar.681208hi'':_fvar.678801 ≤ ↑_fvar.21871 + 1 := ?_mvar.686500hlt:¬i < jheq:i + 1 = j⊢ False X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }h:{ x // x ∈ Icc 1 ↑(n + 1) } → { x // x ∈ X }hg:Function.Bijective ghh:Function.Bijective hπ:ℤ → { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } := fun i => if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Finset.Icc 1 (↑_fvar.21871 + 1) } → { x // x ∈ _fvar.35782 }), (∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), if hi : i ∈ Finset.Icc 1 (↑_fvar.21871 + 1) then @_fvar.21838 ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(g (@_fvar.39754 i)) := fun g => @?_mvar.41155 gx:{ x // x ∈ _fvar.35782 } := @_fvar.35788 (@_fvar.39754 (↑_fvar.21871 + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ _fvar.35782 } := fun i => if i < _fvar.50677 then @_fvar.35791 (@_fvar.39754 i) else @_fvar.35791 (@_fvar.39754 (i + 1))this:∑ i ∈ Finset.Icc 1 (↑_fvar.21871 + 1), @_fvar.21838 ↑(@_fvar.35791 (@_fvar.39754 i)) = ∑ i ∈ Finset.Icc 1 ↑_fvar.21871, @_fvar.21838 ↑(@_fvar.55166 i) + @_fvar.21838 ↑_fvar.50426 := Trans.trans (Trans.trans (Trans.trans (Trans.trans (Trans.trans ?_mvar.56768 ?_mvar.57577) ?_mvar.58230) ?_mvar.58866) ?_mvar.59391) ?_mvar.59453g_ne_x:∀ {i : ℤ}, i ∈ Finset.Icc 1 ↑_fvar.21871 → @_fvar.35788 (@_fvar.39754 i) ≠ _fvar.50426 := fun {i} hi => @?_mvar.658108 i hii:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ _fvar.678801 := ?_mvar.681208hi'':_fvar.678801 ≤ ↑_fvar.21871 + 1 := ?_mvar.686500hlt:i < jheq:i = j⊢ False All goals completed! 🐙 X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { x // x ∈ Icc 1 ↑n } → { x // x ∈ 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 ↑(