!4#4352 apply_congr in BernoulliPolynomials

Stream: mathlib4

[Moritz Firsching]

In !4#4352 there are 3 uses of apply_congr, two of which currently fail. One with the rather concise error message "failed" and the other with "Left-hand side must be an application of a constant."
Should we try to work around this avoiding apply_congr or would it be better to try to make apply_congr work here?

[Alex J. Best]

There were several issues at play here, I have fixed them on the branch:

• Pushed a fix for at least one apply_congr bug (the one with the helpful error message).
• I made a more helpful error message for the second one, which reveals the the proof structure is actually wrong before, due to the following issue:
• I think mathport is generating skips in convs in a way that doesn't make sense, in

conv { skip, blah}

should become

conv =>
  . skip
  . blah

not

conv =>
  skip
  blah

• I added nonrec, so that lean realizes the correct sum_bernoulli lemma to be used is not the one being proved
• we dont have apply_congr with h or a conv mode rename_i https://github.com/leanprover-community/mathlib/issues/2882 so one has to be sneaky to apply the lemmas without naming the arguments by hand, turns out there were some golfs anyway