## 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):

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