Simplifying commutative ring summations

Stream: new members

[Kauê Campos]

Hello, I'm new to Lean and I was wondering why simp couldn't simplify the following - 1 + 1s inside this expression:

inst✝ : CommRing R
x y : R
n : ℕ
hs : ∑ x_1 in range (n + 1), x ^ (x_1 - 1 + 1) * y ^ (n - (x_1 - 1)) * ↑(Nat.choose n (x_1 - 1)) - x * y ^ n = ∑ x_1 in range n, x ^ (x_1 + 1) * y ^ (n - x_1) * ↑(Nat.choose n x_1)

I'm just trying to do simp at hs and it won't progress any further, this isn't the first time I've had issues with simplifying the inner function inside a sum, so I'm wondering what's the proper way of doing it or what I'm doing wrong?

My context is the following:

import Mathlib.Tactic.IntervalCases
import Mathlib.Algebra.BigOperators.Order
import Mathlib.Data.Nat.Multiplicity

open scoped Nat BigOperators
open Nat
open Finset multiplicity

[Eric Wieser]

Well, 0 - 1 + 1 ≠ 0 in lean...

[Riccardo Brasca]

But in a ring it's true, and we have docs#add_sub_cancel (that is tagged simp).

[Riccardo Brasca]

Ah, sorry, it is for the exponents, so it is in Nat.

[Riccardo Brasca]

Well, then the reason, as Eric said, it that it is not true, because 0-1=0

[Riccardo Brasca]

(deleted)

[Riccardo Brasca]

(deleted)

[Kauê Campos]

Ah, I see, I didn't realize it was a natural there. I'll try another approach to doing this then, I suppose that's why I couldn't simplify other stuff inside summations, thanks.

[Kauê Campos]

Okay, I've changed some stuff and now it's

hs: ∑ x_1 in erase (range (n + 1)) 0, x ^ (x_1 - 1 + 1) * y ^ (n - (x_1 - 1)) * ↑(Nat.choose n (x_1 - 1)) =
  ∑ x_1 in range n, x ^ (x_1 + 1) * y ^ (n - x_1) * ↑(Nat.choose n x_1)

and I've already got

hs1: ∀ (x : ℕ), x ∈ erase (range (n + 1)) 0 → x > 0

and a

theorem pos_sub_one_plus_one (a : ℕ) (h: a > 0) : a-1+1 = a

but I'm not sure how I could apply these to x1-1+1 exponent inside the big sum, any ideas?

[Kevin Buzzard]

Why are you using natural subtraction at all? It is a pathological operation. You would be better off rewriting to avoid it completely if possible.

[Kevin Buzzard]

There is docs#Finset.antidiagonal for example, which can be useful for avoiding these things.

[Kauê Campos]

I trying to adapt this from a pen and paper proof as an exercise to learn lean and that's what I ended up doing. I'll take a look at antidiagonals, but it should be possible to simply the expression I got now, and I'm curious to the general case of how to use summation indices in contexts like this, specially for more complicated examples.

[Eric Wieser]

Kevin Buzzard said:

There is docs#Finset.antidiagonal for example, which can be useful for avoiding these things.

Annoyingly while you can really write that in lean code, to get to the docs page you have to write docs#Finset.HasAntidiagonal.antidiagonal