# Zulip Chat Archive

## Stream: new members

### Topic: Lean has trouble understanding intuitive sums (again)

#### Hanting Zhang (Jan 17 2021 at 00:10):

I'm once again stuck on a terrible sum that should be obvious, but turns out to be frustratingly hard for Lean to understand:

```
import tactic
import data.mv_polynomial.rename
import data.mv_polynomial.comm_ring
noncomputable theory
open finset
open_locale big_operators
namespace mv_polynomial
variables (σ : Type*) (R : Type*) {τ : Type*} {S : Type*}
variables [comm_semiring R] [comm_semiring S] [fintype σ] [fintype τ]
def esymm (n : ℕ) : mv_polynomial σ R :=
∑ t in powerset_len n univ, ∏ i in t, X i
/-- A second definition of `esymm σ R n` with range over a subtype instead of `powerset_len`.
Sometimes it's easier to reason with subtypes. -/
lemma esymm₂ (n : ℕ) : (esymm σ R n) =
∑ t : {s : finset σ // s.card = n}, ∏ i in (t : finset σ), X i :=
begin
sorry
end
end mv_polynomial
```

I'm trying to convert the sum over `powerset_len n univ`

to a sum over `{s : finset σ // s.card = n}`

. Both literally count the subsets of `σ`

that have cardinality `n`

. But the first is a finset of `finset σ`

and the second is a subtype `σ`

. I've tried using `congr`

, `attach`

, etc, but it's just a mess. Is there a good way to do this?

#### Hanting Zhang (Jan 17 2021 at 00:16):

@Johan Commelin Do you think it's a good idea to use `powerset_len`

? I've been using it because I'm stubborn and my original Vieta code uses it, but now I'm thinking it might not be worth it. Is there any preference for reasoning with subtypes in mathlib?

#### Adam Topaz (Jan 17 2021 at 00:17):

Maybe docs#finset.sum_bij or docs#finset.sum_bij' would help?

#### Hanting Zhang (Jan 17 2021 at 00:22):

Somehow I've missed these. D: Thanks!

#### Hanting Zhang (Jan 17 2021 at 01:52):

I'vee made some progress, but I've gotten stuck again ):

I need help reasoning with the big `i`

function:

```
import tactic
import data.mv_polynomial.rename
import data.mv_polynomial.comm_ring
noncomputable theory
open finset
open_locale big_operators
namespace mv_polynomial
variables (σ : Type*) (R : Type*) {τ : Type*} {S : Type*}
variables [comm_semiring R] [comm_semiring S] [fintype σ] [fintype τ]
def esymm (n : ℕ) : mv_polynomial σ R :=
∑ t in powerset_len n univ, ∏ i in t, X i
/-- A second definition of `esymm σ R n` with range over a subtype instead of `powerset_len`.
Sometimes it's easier to reason with subtypes. -/
lemma esymm₂ (n : ℕ) : (esymm σ R n) =
∑ t : {s : finset σ // s.card = n}, ∏ i in (t : finset σ), X i :=
begin
rw esymm,
have i : Π (a : finset σ), a ∈ powerset_len n univ → {s : finset σ // s.card = n} :=
by {intros a ha, split, exact (mem_powerset_len.mp ha).2, apply_instance },
apply sum_bij i,
{ intros, simp, },
{ intros,
apply prod_congr,
ext, split,
{ intro h,
sorry },
{ intro h,
sorry },
intros, refl,},
{ intros,
sorry },
{ intros, sorry },
end
end mv_polynomial
```

Maybe it's because I've been staring at it for too long, but how can I unwrap `a_1 ∈ ↑(i a ha)`

at the first `sorry`

? I want to change the membership statement into a logical one.

#### Alex J. Best (Jan 17 2021 at 01:59):

I'm not quite sure whats you are proving here but `i`

is some function which constructs data right, so possibly the problem is that you want to remember the definition of `i`

by using `let i`

rather than `have i`

? When you do that the first sorry is

```
dsimp [i], --actually you don't even need this line
exact h,
```

#### Alex J. Best (Jan 17 2021 at 02:02):

A small example of the difference is:

```
example : ∃ n, n = 2 :=
begin
have i := 2,
use i,
end
```

and you are left with an unprovable goal. But if you use let instead of have you get a proof.

#### Hanting Zhang (Jan 17 2021 at 02:03):

:fear: Oh... I didn't even know there was a difference.

#### Alex J. Best (Jan 17 2021 at 02:05):

Have forgets the term used whereas let doesn't, so for propositions have is more natural, in lean all proofs of the same proposition are equal so it doesn't matter what the original one was. But for things which are "data" like natural numbers, finsets, functions, you want to remember what their definition was mostly, so `let`

is what you need.

#### Hanting Zhang (Jan 17 2021 at 02:44):

Thanks! :tada:

Last updated: May 06 2021 at 22:13 UTC