# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: sum_sum_elim for fintypes

#### Oliver Nash (Jul 04 2020 at 16:11):

I'd like to use the `fintype`

-flavour version of the result `finset.sum_sum_elim`

and can't seem to find it. Does it already exist?

#### Oliver Nash (Jul 04 2020 at 16:11):

More precisely, what I would like is `hidden.sum_sum_elim`

:

```
namespace hidden
open_locale classical
open_locale big_operators
lemma sum_sum_elim
{l m A : Type*} [fintype l] [fintype m] [add_comm_monoid A] (f : l → A) (g : m → A) :
∑ i, sum.elim f g i = (∑ i, f i) + (∑ i, g i) :=
begin
have : @finset.univ (l ⊕ m) _ = finset.image sum.inl finset.univ ∪ finset.image sum.inr finset.univ :=
by { ext a, rcases a; simp, },
by rw [←finset.sum_sum_elim, this],
end
end hidden
```

#### Jalex Stark (Jul 04 2020 at 16:13):

i thought the point of proving things for `finset`

s is that you can apply them to `fintype`

s and lean will insert the coercion to `univ`

for you

#### Oliver Nash (Jul 04 2020 at 16:14):

Oh I see, that lines up with my surprise at not finding anything for `fintype`

s. Thank you I'll try to proceed along these lines.

#### Oliver Nash (Jul 04 2020 at 16:18):

I wonder if something like the following is missing:

```
@[simp] lemma finset.univ_sum_union {l m : Type*} [fintype l] [fintype m] :
@finset.univ (l ⊕ m) _ = finset.image sum.inl finset.univ ∪ finset.image sum.inr finset.univ :=
by { ext a, rcases a; simp, }
```

since we then have:

```
example {l m : Type*} [fintype l] [fintype m] (f : l → R) (g : m → R) :
∑ i, sum.elim f g i = (∑ i, f i) + (∑ i, g i) :=
by simp
```

#### Oliver Nash (Jul 04 2020 at 16:34):

(P.S. I love this newish notation for `big_operators`

.)

#### Johan Commelin (Jul 04 2020 at 16:37):

You're welcome :wink:

#### Jalex Stark (Jul 04 2020 at 16:48):

your `finset.univ_sum_union`

looks good to me

#### Jalex Stark (Jul 04 2020 at 16:51):

i'm not sure what file `finset.univ_sum_union`

goes in, but putting that somewhere and `sum_sum_elim`

in big_operators sounds like a fine PR

#### Oliver Nash (Jul 04 2020 at 17:06):

Great. I’ll either include it with some other changes or else make a mini-PR along the lines you suggest.

#### Chris Hughes (Jul 04 2020 at 18:32):

To make this consistent in style with things like `sum_sigma`

and `sum_product`

it would make sense to define the function taking a `finset X`

and a `finset Y`

and returns the disjoint union as a `finset (X \oplus Y) `

#### Chris Hughes (Jul 04 2020 at 18:42):

This would provide a nicer way to manipulate sums than using `sum_union`

and providing a disjointness proof.

#### Scott Morrison (Jul 05 2020 at 00:18):

I'm not sure that should be a simp lemma.

#### Oliver Nash (Jul 05 2020 at 16:59):

Scott Morrison said:

I'm not sure that should be a simp lemma.

I agree: if anything, it should simplify in the other direction: the disjoint union of two `finset.univ`

s is a single `finset.univ`

!

#### Oliver Nash (Jul 05 2020 at 17:01):

I was just looking to pick up this thread again and I discovered that what I was looking for yesterday in fact _does_ exist. It's called `fintype.sum_sum_type`

.

#### Oliver Nash (Jul 05 2020 at 17:07):

I had just started down the road (which I like) that @Chris Hughes had sketched out, which I interpreted as something like:

```
variables {α γ : Type*}
def disjoint_union (s : finset α) (t : finset γ) : finset (α ⊕ γ) :=
s.image sum.inl ∪ t.image sum.inr
def finset.sum_proj_l (s : finset (α ⊕ γ)) : (finset α) := sorry
def finset.sum_proj_r (s : finset (α ⊕ γ)) : (finset γ) := sorry
lemma finset.proj_l_disjoint_union (s : finset α) (t : finset γ) :
s = (disjoint_union s t).sum_proj_l := sorry
lemma finset.proj_r_disjoint_union (s : finset α) (t : finset γ) :
t = (disjoint_union s t).sum_proj_r := sorry
lemma finset.disjoint_union_proj_lr (s : finset (α ⊕ γ)) :
s = disjoint_union s.sum_proj_l s.sum_proj_r := sorry
def finset.sum_equiv' : finset (α ⊕ γ) ≃ (finset α) × (finset γ) := sorry
-- The lemma I originally wanted, so that I could use `finset.sum_sum_elim`:
@[simp] lemma finset.disjoint_union_univ {l m : Type*} [fintype l] [fintype m] :
disjoint_union finset.univ finset.univ = @finset.univ (l ⊕ m) _ :=
by { ext a, rcases a; simp [disjoint_union], }
```

but having found `fintype.sum_sum_type`

I'm going to park all this, even if the existence of `fintype.sum_sum_type`

does seem a bit inconsistent with the philosophy outlined by @Jalex Stark

Last updated: May 07 2021 at 21:10 UTC