How to rewrite sub-expression inside lambda?

Stream: new members

[Anthony Peterson]

I've been proving some simple natural number theorems to practice my Lean skills. I'm struggling with the Binomial theorem however because it involves summing the values of a function or lambda (maybe Lean calls it a binder?). I can't seem to rewrite using a known equality inside the function:

def binomial_thereom (x y p : Nat) : (x + y) ^ p = Nat.sum (List.map (binterm x y p) (List.range (p + 1))) := by
<<proof terms omitted>>

My current proof state is

p' x y : ℕ ih : ∀ (x y : ℕ), (x + y) ^ p' = (List.map (binterm x y p') (List.range (p' + 1))).sum ⊢ (List.map (fun i => x ^ i * y ^ (p' - i) * combin p' i) (List.range (p' + 1))).sum * (x + y) = (List.map (fun i => x ^ i * y ^ (p' + 1 - i) * combin (p' + 1) i) (List.range (p' + 2))).sum
where combin and binterm are:

def combin (p i : Nat) := p.factorial / (i.factorial * (p - i).factorial) def binterm (x y p i : Nat) := x ^ i * y ^ (p - i) * combin p i

I want to rewrite y ^ (p' + 1 - i) into y ^ (p' - i + 1), and then take out a factor of y, but when I try to rw [Nat.add_sub_assoc] it fails.

I read another discussion here about how rw doesn't work in binders and I should use simp_rw, but I tried simp_rw and I was also unable to progress with that. It said no progress made.

Any tips for working with this type of proof?

[Kevin Buzzard]

I think the tips which would help most here are #backticks and #mwe . If you edit your original message so that it's a mwe then it will become much easier for other people to see what you're doing wrong.

[Luigi Massacci]

Having said that, just by reading your first paragraph, it is indeed the case that rw can’t work under binders, try using simp_rw

[Anthony Peterson]

I’ll try to put in a MWE tomorrow. I tried simp_rw and it didn’t work but I’ll show that.

[Luigi Massacci]

do you know about conv? (if not, see here)

[Anthony Peterson]

Here's my MWE:

def sum_power_rearrange (x y : Nat) : Nat.sum (List.map (fun i => x ^ (y + 1 - i)) (List.range (y + 1))) = Nat.sum (List.map (fun i => x * x ^ (y  - i)) (List.range (y + 1))) := by

simp_rw [Nat.add_sub_assoc]

The simp_rw doesn't make any progress, and rw doesn't work.

[Yaël Dillies]

That's because docs#Nat.add_sub_assoc has a side condition k ≤ m. If you provide that side condition, then simp_rw will work

[Anthony Peterson]

Ah, ok during normal rewriting with the side conditions it would just add it as another thing to proof afterwards

[Anthony Peterson]

Any hints on how to prove that the index of the summation is always y or less if the list is Range (y + 1)?

[Edward van de Meent]

rewrite using List.attach_map_val

[Edward van de Meent]

then use congr

[Anthony Peterson]

Thank you. I will spend some time working through this to understand more.