Аналіз I, Глава 7.1

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. hen 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:

We do not attempt to replicate the full API for Finset.sum.{u_3, u_4} {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : βFinset.sum here, but in subsequent sections we shall make liberal use of this API.

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

Визначення 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:ℤhx:x ∈ Icc m n⊢ a x = 0 n:ℤm:ℤh:n < ma:ℤ → ℝx:ℤhx:m ≤ x ∧ x ≤ n⊢ a x = 0 All goals completed! 🐙

Визначення 7.1.1. This is similar to Mathlib's Finset.sum_Icc_succ_top.{u_2} {M : Type u_2} [AddCommMonoid M] {a b : ℕ} (hab : a ≤ b + 1) (f : ℕ → M) : ∑ k ∈ Finset.Icc a (b + 1), f k = ∑ k ∈ Finset.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:ℤ → ℝi:ℤ⊢ i ∈ Icc m (n + 1) ↔ i ∈ insert (n + 1) (Icc m n); n:ℤm:ℤh:n ≥ m - 1a:ℤ → ℝi:ℤ⊢ m ≤ i ∧ i ≤ n + 1 ↔ i = n + 1 ∨ m ≤ i ∧ i ≤ 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! 🐙

Ремарка 7.1.3

example (a: ℤ → ℝ) (m n:ℤ) : ∑ i ∈ Icc m n, a i = ∑ j ∈ Icc m n, a j := rfl

Лема 7.1.4(a) / Вправа 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! 🐙

Лема 7.1.4(b) / Вправа 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! 🐙

Лема 7.1.4(c) / Вправа 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! 🐙

Лема 7.1.4(d) / Вправа 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! 🐙

Лема 7.1.4(e) / Вправа 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! 🐙

Лема 7.1.4(f) / Вправа 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! 🐙
-- This lemma is not part of the original textbook, but proven similarly to the other results -- above, and is handy. Finset.sum_congr.{u_1, u_4} {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M} (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g#check sum_congr
Finset.sum_congr.{u_1, u_4} {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [AddCommMonoid M] {f g : ι → M}
  (h : s₁ = s₂) : (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g

Proposition 7.1.8. There is an unfortunate hack here in that one needs to extend the expressions unknown identifier 'f'f g i and unknown identifier 'f'f h i outside of unknown identifier 'Icc'Icc 1 n, leading to a certain uglification of the code.

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! 🐙 -- A technical step: we extend g, h to the entire integers using a slightly artificial map π 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 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))⊢ ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i)) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑(g (π (↑n + 1))) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = x⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj'✝:j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'✝⟩ = xhj':1 ≤ j ∧ j ≤ ↑n + 1⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) have : ∑ i ∈ Icc (1:ℤ) (n + 1), f (h (π i)) = ∑ i ∈ Icc (1:ℤ) n, f (h' i) + f x := calc _ = ∑ i ∈ Icc (1:ℤ) j, f (h (π i)) + ∑ i ∈ Icc (j+1:ℤ) (n + 1), f (h (π i)) := 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 j, f ↑(h (π i)) + ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ j ≤ ↑n + 1 all_goals 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 j, f ↑(h (π i)) + ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) + ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 j, f ↑(h (π i)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ 1 ≤ j 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) + ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑x + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc (j + 1) (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑(h (π j)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑x 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))x✝:ℤa✝:x✝ ∈ Icc (j + 1) (↑n + 1)⊢ f ↑(h (π x✝)) = f ↑(h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + f ↑x + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) = ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) + f ↑x 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) + f ↑x = ∑ i ∈ Icc 1 (j - 1), f ↑(h' i) + ∑ i ∈ Icc j ↑n, f ↑(h' i) + f ↑x 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 (j - 1), f ↑(h' i)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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) = ∑ i ∈ Icc j ↑n, f ↑(h' i) all_goals 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))i:ℤhi:i ∈ Icc j ↑n⊢ f ↑(h (π (i + 1))) = f ↑(h' i); 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))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:ℕ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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))i:ℤhi:1 ≤ i ∧ i ≤ j - 1⊢ f ↑(h (π i)) = f ↑(if i < j then h (π i) else h (π (i + 1))) have : i < 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) + f ↑x = ∑ i ∈ Icc 1 (j - 1), f ↑(h' i) + ∑ i ∈ Icc j ↑n, f ↑(h' i) + f ↑x All goals completed! 🐙 All goals completed! 🐙 have : ¬ i < 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h (π i)) + ∑ i ∈ Icc j ↑n, f ↑(h (π (i + 1))) + f ↑x = ∑ i ∈ Icc 1 (j - 1), f ↑(h' i) + ∑ i ∈ Icc j ↑n, f ↑(h' i) + f ↑x 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h' i) + ∑ i ∈ Icc j ↑n, f ↑(h' i) + f ↑x = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑x 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ ∑ i ∈ Icc 1 (j - 1), f ↑(h' i) + ∑ i ∈ Icc j ↑n, f ↑(h' i) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))⊢ j - 1 ≤ ↑n all_goals 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑x⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) + f ↑x = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑x 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑x⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) have g_ne_x {i:ℤ} (hi : i ∈ Icc (1:ℤ) n) : g (π i) ≠ x := 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xi:ℤhi:1 ≤ i ∧ i ≤ ↑n⊢ g (π i) ≠ x 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi'':i ≤ ↑n + 1⊢ ¬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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑n⊢ h' i ≠ x have hi' : 0 ≤ i := 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:i < j⊢ h' i ≠ 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:¬i < j⊢ h' i ≠ x 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:¬i < jheq:h' i = x⊢ False all_goals 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:¬i < jheq:i + 1 = j⊢ False 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1hlt:i < jheq:i = j⊢ False 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xi:ℤhi:1 ≤ i ∧ i ≤ ↑nhi':0 ≤ ihi'':i ≤ ↑n + 1heq:i + 1 = jhlt:¬False⊢ i < j; All goals completed! 🐙 set gtil : Icc (1:ℤ) n → X.erase x := fun i ↦ ⟨ (g (π i)).val, 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xi:{ x // x ∈ Icc 1 ↑n }⊢ ↑(g (π ↑i)) ∈ X.erase ↑x All goals completed! 🐙 ⟩ set htil : Icc (1:ℤ) n → X.erase x := fun i ↦ ⟨ (h' i).val, 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩i:{ x // x ∈ Icc 1 ↑n }⊢ ↑(h' ↑i) ∈ X.erase ↑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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑y⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) have why : Function.Bijective gtil := 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 why2 : Function.Bijective htil := 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! 🐙 calc _ = ∑ i ∈ Icc (1:ℤ) n, if hi: i ∈ Icc (1:ℤ) n then ftil (gtil ⟨ 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ ∑ i ∈ Icc 1 ↑n, f ↑(g (π i)) = ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then ftil (gtil ⟨i, hi⟩) else 0 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ ∀ x ∈ Icc 1 ↑n, f ↑(g (π x)) = if hi : x ∈ Icc 1 ↑n then ftil (gtil ⟨x, hi⟩) else 0 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htili:ℤhi:i ∈ Icc 1 ↑n⊢ f ↑(g (π i)) = if hi : i ∈ Icc 1 ↑n then ftil (gtil ⟨i, hi⟩) else 0 All goals completed! 🐙 _ = ∑ i ∈ Icc (1:ℤ) n, if hi: i ∈ Icc (1:ℤ) n then ftil (htil ⟨ 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then ftil (gtil ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then ftil (htil ⟨i, hi⟩) else 0 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ #(X.erase ↑x) = 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ n + 1 - 1 = nX':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ ↑x ∈ X X':Type u_1f:X' → ℝn:ℕhn:∀ (X : Finset X'), #X = n → ∀ (g h : { 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ n + 1 - 1 = n 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then ftil (htil ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htil⊢ ∀ x ∈ Icc 1 ↑n, (if hi : x ∈ Icc 1 ↑n then ftil (htil ⟨x, hi⟩) else 0) = f ↑(h' x) 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 ∈ Icc 1 (↑n + 1) } := fun i => if hi : i ∈ Icc 1 (↑n + 1) then ⟨i, hi⟩ else ⟨1, ⋯⟩hπ:∀ (g : { x // x ∈ Icc 1 (↑n + 1) } → { x // x ∈ X }), (∑ i ∈ Icc 1 (↑n + 1), if hi : i ∈ Icc 1 (↑n + 1) then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ Icc 1 (↑n + 1), f ↑(g (π i))x:{ x // x ∈ X } := g (π (↑n + 1))j:ℤhj':j ∈ Icc 1 ↑(n + 1)hj:h ⟨j, hj'⟩ = xhj1:1 ≤ jhj2:j ≤ ↑n + 1h':ℤ → { x // x ∈ X } := fun i => if i < j then h (π i) else h (π (i + 1))this:∑ i ∈ Icc 1 (↑n + 1), f ↑(h (π i)) = ∑ i ∈ Icc 1 ↑n, f ↑(h' i) + f ↑xg_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → g (π i) ≠ xh'_ne_x:∀ {i : ℤ}, i ∈ Icc 1 ↑n → h' i ≠ xgtil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(g (π ↑i)), ⋯⟩htil:{ x // x ∈ Icc 1 ↑n } → { x_1 // x_1 ∈ X.erase ↑x } := fun i => ⟨↑(h' ↑i), ⋯⟩ftil:{ x_1 // x_1 ∈ X.erase ↑x } → ℝ := fun y => f ↑ywhy:Function.Bijective gtilwhy2:Function.Bijective htili:ℤhi:i ∈ Icc 1 ↑n⊢ (if hi : i ∈ Icc 1 ↑n then ftil (htil ⟨i, hi⟩) else 0) = f ↑(h' i) All goals completed! 🐙

This fact ensures that Definition 7.1.6 would be well-defined even if we did not appeal to the existing Finset.sum.{u_3, u_4} {α : Type u_3} {β : Type u_4} [AddCommMonoid β] (s : Finset α) (f : α → β) : βFinset.sum method.

theorem exist_bijection {n:ℕ} {Y:Type*} (X: Finset Y) (hcard: X.card = n) : ∃ g: Icc (1:ℤ) n → X, Function.Bijective g := n:ℕY:Type u_1X:Finset Yhcard:#X = n⊢ ∃ g, Function.Bijective g have : (Icc (1:ℤ) n).card = X.card := n:ℕY:Type u_1X:Finset Yhcard:#X = n⊢ ∃ g, Function.Bijective g All goals completed! 🐙 n:ℕY:Type u_1X:Finset Yhcard:#X = nthis:{ x // x ∈ Icc 1 ↑n } ≃ { x // x ∈ X }⊢ ∃ g, Function.Bijective g n:ℕY:Type u_1X:Finset Yhcard:#X = nthis:{ x // x ∈ Icc 1 ↑n } ≃ { x // x ∈ X }⊢ Function.Bijective ⇑this All goals completed! 🐙

Визначення 7.1.6

theorem finite_series_eq {n:ℕ} {Y:Type*} (X: Finset Y) (f: Y → ℝ) (g: Icc (1:ℤ) n → X) (hg: Function.Bijective g) : ∑ i ∈ X, f i = ∑ i ∈ Icc (1:ℤ) n, (if hi:i ∈ Icc (1:ℤ) n then f (g ⟨ i, hi ⟩) else 0) := n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective g⊢ ∑ i ∈ X, f i = ∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0 n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective g⊢ (∑ i ∈ Icc 1 ↑n, if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) = ∑ i ∈ X, f i n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective g⊢ ∀ (a : ℤ) (ha : a ∈ Icc 1 ↑n), (fun i hi => ↑(g ⟨i, hi⟩)) a ha ∈ Xn:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective g⊢ ∀ (a₁ : ℤ) (ha₁ : a₁ ∈ Icc 1 ↑n) (a₂ : ℤ) (ha₂ : a₂ ∈ Icc 1 ↑n), (fun i hi => ↑(g ⟨i, hi⟩)) a₁ ha₁ = (fun i hi => ↑(g ⟨i, hi⟩)) a₂ ha₂ → a₁ = a₂n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective g⊢ ∀ b ∈ X, ∃ a, ∃ (ha : a ∈ Icc 1 ↑n), (fun i hi => ↑(g ⟨i, hi⟩)) a ha = bn:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective g⊢ ∀ (a : ℤ) (ha : a ∈ Icc 1 ↑n), (if hi : a ∈ Icc 1 ↑n then f ↑(g ⟨a, hi⟩) else 0) = f ((fun i hi => ↑(g ⟨i, hi⟩)) a ha) n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective g⊢ ∀ (a : ℤ) (ha : a ∈ Icc 1 ↑n), (fun i hi => ↑(g ⟨i, hi⟩)) a ha ∈ X n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective gi:ℤhi:i ∈ Icc 1 ↑n⊢ (fun i hi => ↑(g ⟨i, hi⟩)) i hi ∈ X; All goals completed! 🐙 n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective g⊢ ∀ (a₁ : ℤ) (ha₁ : a₁ ∈ Icc 1 ↑n) (a₂ : ℤ) (ha₂ : a₂ ∈ Icc 1 ↑n), (fun i hi => ↑(g ⟨i, hi⟩)) a₁ ha₁ = (fun i hi => ↑(g ⟨i, hi⟩)) a₂ ha₂ → a₁ = a₂ n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective gi:ℤhi:i ∈ Icc 1 ↑nj:ℤhj:j ∈ Icc 1 ↑nh:(fun i hi => ↑(g ⟨i, hi⟩)) i hi = (fun i hi => ↑(g ⟨i, hi⟩)) j hj⊢ i = j n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective gi:ℤhi:i ∈ Icc 1 ↑nj:ℤhj:j ∈ Icc 1 ↑nh:i = j⊢ i = j; All goals completed! 🐙 n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective g⊢ ∀ b ∈ X, ∃ a, ∃ (ha : a ∈ Icc 1 ↑n), (fun i hi => ↑(g ⟨i, hi⟩)) a ha = b n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective gb:Yhb:b ∈ X⊢ ∃ a, ∃ (ha : a ∈ Icc 1 ↑n), (fun i hi => ↑(g ⟨i, hi⟩)) a ha = b n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective gb:Yhb:b ∈ Xi:ℤhi:i ∈ Icc 1 ↑nh:g ⟨i, hi⟩ = ⟨b, hb⟩⊢ ∃ a, ∃ (ha : a ∈ Icc 1 ↑n), (fun i hi => ↑(g ⟨i, hi⟩)) a ha = b n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective gb:Yhb:b ∈ Xi:ℤhi:i ∈ Icc 1 ↑nh:g ⟨i, hi⟩ = ⟨b, hb⟩⊢ (fun i hi => ↑(g ⟨i, hi⟩)) i hi = b; All goals completed! 🐙 n:ℕY:Type u_1X:Finset Yf:Y → ℝg:{ x // x ∈ Icc 1 ↑n } → { x // x ∈ X }hg:Function.Bijective gi:ℤhi:i ∈ Icc 1 ↑n⊢ (if hi : i ∈ Icc 1 ↑n then f ↑(g ⟨i, hi⟩) else 0) = f ((fun i hi => ↑(g ⟨i, hi⟩)) i hi); All goals completed! 🐙

Твердження 7.1.11(a) / Вправа 7.1.2

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

Твердження 7.1.11(b) / Вправа 7.1.2

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

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

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

Твердження 7.1.11(c) / Вправа 7.1.2

theorem declaration uses 'sorry'map_finite_series {X:Type*} [Fintype X] [Fintype Y] (f: X → ℝ) {g:Y → X} (hg: Function.Bijective g) : ∑ x, f x = ∑ y, f (g y) := Y:Type u_2X:Type u_1inst✝¹:Fintype Xinst✝:Fintype Yf:X → ℝg:Y → Xhg:Function.Bijective g⊢ ∑ x, f x = ∑ y, f (g y) All goals completed! 🐙
-- Proposition 7.1.11(d) is `rfl` in our formalism and is therefore omitted.

Твердження 7.1.11(e) / Вправа 7.1.2

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

Твердження 7.1.11(f) / Вправа 7.1.2

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

Твердження 7.1.11(g) / Вправа 7.1.2

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

Твердження 7.1.11(h) / Вправа 7.1.2

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

Твердження 7.1.11(i) / Вправа 7.1.2

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

Лема 7.1.13 -

theorem declaration uses 'sorry'finite_series_of_finite_series {XX YY:Type*} (X: Finset XX) (Y: Finset YY) (f: XX × YY → ℝ) : ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ Finset.product X Y, f z := XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝn:ℕh:#X = n⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕ⊢ ∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝ⊢ ∀ (X : Finset XX), #X = 0 → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z⊢ ∀ (X : Finset XX), #X = n + 1 → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝ⊢ ∀ (X : Finset XX), #X = 0 → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z All goals completed! 🐙 XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z have hnon : X.Nonempty := XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1⊢ #X ≠ 0; All goals completed! 🐙 XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ X⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z have hcard : X'.card = n := XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z All goals completed! 🐙 have hunion : X = X' ∪ {x₀} := XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nx:XX⊢ x ∈ X ↔ x ∈ X' ∪ {x₀} XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nx:XXh:x = x₀⊢ x ∈ X ↔ x ∈ X' ∪ {x₀}XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nx:XXh:¬x = x₀⊢ x ∈ X ↔ x ∈ X' ∪ {x₀} all_goals All goals completed! 🐙 have hdisj : Disjoint X' {x₀} := XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f z All goals completed! 🐙 calc _ = ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ x ∈ {x₀}, ∑ y ∈ Y, f (x, y) := XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ x ∈ {x₀}, ∑ y ∈ Y, f (x, y) All goals completed! 🐙 _ = ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ y ∈ Y, f (x₀, y) := XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ x ∈ {x₀}, ∑ y ∈ Y, f (x, y) = ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ y ∈ Y, f (x₀, y) All goals completed! 🐙 _ = ∑ z ∈ Finset.product X' Y, f z + ∑ y ∈ Y, f (x₀, y) := XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ x ∈ X', ∑ y ∈ Y, f (x, y) + ∑ y ∈ Y, f (x₀, y) = ∑ z ∈ X'.product Y, f z + ∑ y ∈ Y, f (x₀, y) All goals completed! 🐙 _ = ∑ z ∈ Finset.product X' Y, f z + ∑ z ∈ Finset.product {x₀} Y, f z := XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ z ∈ X'.product Y, f z + ∑ y ∈ Y, f (x₀, y) = ∑ z ∈ X'.product Y, f z + ∑ z ∈ {x₀}.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ y ∈ Y, f (x₀, y) = ∑ z ∈ {x₀}.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ x, f (x₀, ↑x) = ∑ x, f ↑x set π : Finset.product {x₀} Y → Y := fun z ↦ ⟨ z.val.2, XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}z:{ x // x ∈ {x₀}.product Y }⊢ (↑z).2 ∈ Y XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}z:XX × YYhz:z ∈ {x₀}.product Y⊢ (↑⟨z, hz⟩).2 ∈ Y; XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}z:XX × YYhz:∃ a ∈ Y, (x₀, a) = z⊢ z.2 ∈ Y; XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}a:YYha:a ∈ Y⊢ (x₀, a).2 ∈ Y; All goals completed! 🐙 ⟩ have hπ : Function.Bijective π := XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ z ∈ X'.product Y, f z + ∑ y ∈ Y, f (x₀, y) = ∑ z ∈ X'.product Y, f z + ∑ z ∈ {x₀}.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩⊢ Function.Injective πXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩⊢ Function.Surjective π XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩⊢ Function.Injective π XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩x:XXy:YYhz:(x, y) ∈ {x₀}.product Yx':XXy':YYhz':(x', y') ∈ {x₀}.product Yhzz':π ⟨(x, y), hz⟩ = π ⟨(x', y'), hz'⟩⊢ ⟨(x, y), hz⟩ = ⟨(x', y'), hz'⟩ XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩x:XXy:YYx':XXy':YYhz:y ∈ Y ∧ x₀ = xhz':y' ∈ Y ∧ x₀ = x'hzz':y = y'⊢ x = x' ∧ y = y' All goals completed! 🐙 XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩y:YYhy:y ∈ Y⊢ ∃ a, π a = ⟨y, hy⟩ use ⟨ (x₀, y), XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩y:YYhy:y ∈ Y⊢ (x₀, y) ∈ {x₀}.product Y All goals completed! 🐙 ⟩ XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩hπ:Function.Bijective πz:{ x // x ∈ {x₀}.product Y }a✝:z ∈ univ⊢ z.1.1 = x₀ XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩hπ:Function.Bijective πx:XXy:YYhz:(x, y) ∈ {x₀}.product Ya✝:⟨(x, y), hz⟩ ∈ univ⊢ ⟨(x, y), hz⟩.1.1 = x₀ XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}π:{ x // x ∈ {x₀}.product Y } → { x // x ∈ Y } := fun z => ⟨(↑z).2, ⋯⟩hπ:Function.Bijective πx:XXy:YYhz✝:(x, y) ∈ {x₀}.product Ya✝:⟨(x, y), hz✝⟩ ∈ univhz:y ∈ Y ∧ x₀ = x⊢ x = x₀; All goals completed! 🐙 _ = _ := XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ ∑ z ∈ X'.product Y, f z + ∑ z ∈ {x₀}.product Y, f z = ∑ z ∈ X.product Y, f z XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ X.product Y = X'.product Y ∪ {x₀}.product YXX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ Disjoint (X'.product Y) ({x₀}.product Y) XX:Type u_1YY:Type u_2Y:Finset YYf:XX × YY → ℝn:ℕhn:∀ (X : Finset XX), #X = n → ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ z ∈ X.product Y, f zX:Finset XXhX:#X = n + 1hnon:X.Nonemptyx₀:XXhx₀:x₀ ∈ XX':Finset XX := X.erase x₀hcard:#X' = nhunion:X = X' ∪ {x₀}hdisj:Disjoint X' {x₀}⊢ X.product Y = X'.product Y ∪ {x₀}.product Y All goals completed! 🐙 All goals completed! 🐙

Наслідок 7.1.14 (Fubini's theorem for finite series)

theorem finite_series_refl {XX YY:Type*} (X: Finset XX) (Y: Finset YY) (f: XX × YY → ℝ) : ∑ z ∈ Finset.product X Y, f z = ∑ z ∈ Finset.product Y X, f (z.2, z.1) := XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ z ∈ X.product Y, f z = ∑ z ∈ Y.product X, f (z.2, z.1) set h : Finset.product Y X → Finset.product X Y := fun z ↦ ⟨ (z.val.2, z.val.1), XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝz:{ x // x ∈ Y.product X }⊢ ((↑z).2, (↑z).1) ∈ X.product Y XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝz:YY × XXhz:z ∈ Y.product X⊢ ((↑⟨z, hz⟩).2, (↑⟨z, hz⟩).1) ∈ X.product Y; XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝz:YY × XXhz:z.1 ∈ Y ∧ z.2 ∈ X⊢ z.2 ∈ X ∧ z.1 ∈ Y; All goals completed! 🐙 ⟩ have hh : Function.Bijective h := XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ z ∈ X.product Y, f z = ∑ z ∈ Y.product X, f (z.2, z.1) XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩⊢ Function.Injective hXX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩⊢ Function.Surjective h XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩⊢ Function.Injective h XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩y:YYx:XXhz:(y, x) ∈ Y.product Xy':YYx':XXhz':(y', x') ∈ Y.product Xhzz':h ⟨(y, x), hz⟩ = h ⟨(y', x'), hz'⟩⊢ ⟨(y, x), hz⟩ = ⟨(y', x'), hz'⟩ XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩y:YYx:XXy':YYx':XXhz:y ∈ Y ∧ x ∈ Xhz':y' ∈ Y ∧ x' ∈ Xhzz':x = x' ∧ y = y'⊢ y = y' ∧ x = x' All goals completed! 🐙 XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩z:XX × YYhz:z ∈ X.product Y⊢ ∃ a, h a = ⟨z, hz⟩ XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩z:XX × YYhz✝:z ∈ X.product Yhz:z.1 ∈ X ∧ z.2 ∈ Y⊢ ∃ a, h a = ⟨z, hz✝⟩ use ⟨ (z.2, z.1), XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩z:XX × YYhz✝:z ∈ X.product Yhz:z.1 ∈ X ∧ z.2 ∈ Y⊢ (z.2, z.1) ∈ Y.product X All goals completed! 🐙 ⟩ XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩hh:Function.Bijective h⊢ ∑ x, f ↑x = ∑ z ∈ Y.product X, f (z.2, z.1) XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝh:{ x // x ∈ Y.product X } → { x // x ∈ X.product Y } := fun z => ⟨((↑z).2, (↑z).1), ⋯⟩hh:Function.Bijective h⊢ ∑ x, f ↑x = ∑ x, f ((↑x).2, (↑x).1) All goals completed! 🐙
theorem finite_series_comm {XX YY:Type*} (X: Finset XX) (Y: Finset YY) (f: XX × YY → ℝ) : ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ y ∈ Y, ∑ x ∈ X, f (x, y) := XX:Type u_1YY:Type u_2X:Finset XXY:Finset YYf:XX × YY → ℝ⊢ ∑ x ∈ X, ∑ y ∈ Y, f (x, y) = ∑ y ∈ Y, ∑ x ∈ X, f (x, y) All goals completed! 🐙-- Вправа 7.1.3 : develop as many analogues as you can of the above theory for finite products -- instead of finite sums. Nat.factorial_zero : Nat.factorial 0 = 1#check Nat.factorial_zero
Nat.factorial_zero : Nat.factorial 0 = 1
Nat.factorial_succ (n : ℕ) : (n + 1).factorial = (n + 1) * n.factorial#check Nat.factorial_succ
Nat.factorial_succ (n : ℕ) : (n + 1).factorial = (n + 1) * n.factorial

Вправа 7.1.4. Note: there may be some technicalities passing back and forth between natural numbers and integers. Look into the tactics unknown identifier 'zify'zify, unknown identifier 'norm_cast'norm_cast, and unknown identifier 'omega'omega

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

Вправа 7.1.5

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