# Zulip Chat Archive

## Stream: new members

### Topic: equality of sums of functions

#### Yakov Pechersky (Aug 26 2020 at 13:28):

If I have a goal of

```
⊢ (λ (l : fin (n + 2)), ...) = λ (l : fin (n + 2)), ...
```

what's the tactic step to get back to a goal of

```
⊢ (∑ (l : fin (n + 2)), ...) = ∑ (l : fin (n + 2)), ...
```

#### Yakov Pechersky (Aug 26 2020 at 13:28):

Basically, the reverse of a `congr`

step.

#### Kenny Lau (Aug 26 2020 at 13:30):

don't get there to begin with

#### Kenny Lau (Aug 26 2020 at 13:30):

use `congr' 1`

#### Kenny Lau (Aug 26 2020 at 13:31):

think about it. what you ask doesn't make sense logically

#### Kenny Lau (Aug 26 2020 at 13:31):

the sum being equal doesn't imply the functions being equal

#### Yakov Pechersky (Aug 26 2020 at 13:35):

I'm finding it cumbersome to rearrange terms inside a sum of sums. So I was hoping to unwrap two levels down, move things around on the LHS, then `revert ...; refine congr_fun _`

and then place the sums back.

#### Kevin Buzzard (Aug 26 2020 at 13:36):

Aren't you asking the following question: "How do I prove that if \sum f(n) = \sum g(n) then f = g"? The answer is "it can't be done because it's not true in general"

#### Reid Barton (Aug 26 2020 at 13:37):

It seems like your question is backwards, and so the answer is `congr`

#### Yakov Pechersky (Aug 26 2020 at 13:38):

I think I get what you mean

#### Yakov Pechersky (Aug 26 2020 at 13:39):

So I'll have to stick with `simp_rw [mul_comm, mul_assoc]`

etc

Last updated: May 10 2021 at 00:31 UTC