feat: port Algebra.BigOperators.Intervals

Stream: mathlib4

[Moritz Firsching]

in mathlib4#1901,
I'm stuck here:
https://github.com/leanprover-community/mathlib4/blob/168aabd8e9e8c5b9a9a39bac66aad8ba5bf2f87a/Mathlib/Algebra/BigOperators/Intervals.lean#L298

conv => pattern (occs := 2) f _ • g _ <;> (rw [← sum_range_succ_sub_sum g])

This was

 conv { for (f _ • g _) [2] { rw ← sum_range_succ_sub_sum g } },

before and is supposed to change the occurances of g k in the rhs of the goal

f m • g m + Finset.sum (Ico (m + 1) n) fun k => f k • g k

I get two unknown metavariable '?_uniq.95707' error.
I tried already changing the line to

conv => pattern (occs := 2) (f _) • (g _) ; (rw [← sum_range_succ_sub_sum g])

but it didn't help.
How to fix it best?

[David Renshaw]

That looks to me like a bug in conv.

This seems to work:

  have h₃: (Finset.sum (Ico (m+1) n) fun i => f i • g i) =
             (Finset.sum (Ico (m+1) n) fun i =>
                f i • ((Finset.sum (Finset.range (i + 1)) g) -
                        (Finset.sum (Finset.range i) g))) := by congr; funext; rw [← sum_range_succ_sub_sum g]
  rw [h₃]

[Moritz Firsching]

Great, thanks @David Renshaw , I put you as a co-author for that commit.
I had to do the same thing for a second conv in the proof and left porting notes saying conv was removed.
I think this is good for the port of the file at hand.
Perhaps it is worth looking into what exactly goes wrong with conv here, possibly constructing a MWE...