# Zulip Chat Archive

## Stream: general

### Topic: how to call this lemma

#### Johan Commelin (Aug 07 2018 at 12:03):

lemma quux {A : Type*} [add_comm_group A] {n : ℕ} (f : fin (n+1) → A) : sum univ f = f n + sum univ (λ i : fin n, f i.raise) := begin sorry end

#### Johan Commelin (Aug 07 2018 at 12:06):

Ooh, and if you don't know a name, but you know a *proof*... that's fine too.

#### Kevin Buzzard (Aug 07 2018 at 12:23):

Johan, I think Kenny might have generated a proof of this once, when I was trying to figure out induction.

#### Kevin Buzzard (Aug 07 2018 at 12:24):

https://xenaproject.wordpress.com/2018/03/30/proofs-by-induction/

#### Kevin Buzzard (Aug 07 2018 at 12:25):

check out def4 in https://github.com/kckennylau/Lean/blob/master/proofs_by_induction.lean

#### Kevin Buzzard (Aug 07 2018 at 12:25):

Apparently it uses a lemma called `chris`

. I'm not sure if this is the official mathlib-sanctioned name.

#### Johan Commelin (Aug 07 2018 at 12:30):

Ok, thanks. I'll take a look in a minute!

#### Chris Hughes (Aug 07 2018 at 12:56):

I proved a slightly weaker version

lemma quux {A : Type*} [add_comm_group A] {n : ℕ} (f : fin (n+1) → A) : sum univ f = f ⟨n, nat.lt_succ_self _⟩ + sum univ (λ i : fin n, f i.raise) := by rw [← insert_erase (mem_univ (⟨n, nat.lt_succ_self _⟩ : fin (n + 1))), sum_insert (not_mem_erase _ _), add_left_inj]; exact sum_bij (λ a ha, ⟨a, lt_of_le_of_ne (nat.le_of_lt_succ a.2) (fin.vne_of_ne (mem_erase.1 ha).1)⟩ ) (λ _ _, mem_univ _) (λ ⟨_, _⟩ _, rfl) (λ ⟨a, _⟩ ⟨b, _⟩ _ _ h, fin.eq_of_veq (fin.veq_of_eq h : _)) (λ b hb, ⟨⟨b.1, nat.lt_succ_of_lt b.2⟩, mem_erase.2 ⟨fin.ne_of_vne (ne_of_lt b.2), mem_univ _⟩, by cases b; refl⟩)

#### Johan Commelin (Aug 07 2018 at 12:57):

Why is it weaker?

#### Johan Commelin (Aug 07 2018 at 12:57):

Also, apparently I ought to be using `finset.range`

...

#### Chris Hughes (Aug 07 2018 at 12:57):

I used `⟨n, nat.lt_succ_self _⟩`

instead of `\u n`

#### Johan Commelin (Aug 07 2018 at 12:58):

Aaah, but that is better.

#### Johan Commelin (Aug 07 2018 at 12:58):

Silly me didn't understand that `\u n`

is difficult.

#### Johan Commelin (Aug 07 2018 at 12:59):

I think you can use `nat.le_refl _`

for some golfing.

#### Johan Commelin (Aug 07 2018 at 12:59):

But I will first think about the `finset.range`

version. Maybe it becomes a whole lot easier.

#### Johan Commelin (Aug 07 2018 at 14:08):

lemma quux {A : Type*} [add_comm_group A] (n : ℕ) (f : ℕ → A) : (finset.range (n+1)).sum f = f n + (finset.range n).sum f := by simp

#### Johan Commelin (Aug 07 2018 at 14:09):

So, that might not be even worth stating as a lemma.

#### Kenny Lau (Aug 07 2018 at 14:09):

what's the use of this lemma if you could just `simp`

?

#### Johan Commelin (Aug 07 2018 at 14:10):

That's exactly my point.

Last updated: May 13 2021 at 22:15 UTC