mathlib

41c227a1 - feat(algebra/infinite_sum): make tsum irreducible (#4679)

feat(algebra/infinite_sum): make tsum irreducible (#4679) See https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F.20tactics/topic/congr'.20is.20slow