## 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.