equality of sums of functions

Stream: new members

[Yakov Pechersky]

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]

Basically, the reverse of a congr step.

[Kenny Lau]

don't get there to begin with

[Kenny Lau]

use congr' 1

[Kenny Lau]

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

[Kenny Lau]

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

[Yakov Pechersky]

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]

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]

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

[Yakov Pechersky]

I think I get what you mean

[Yakov Pechersky]

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