Mathlib HasFiniteSupport: use `.fun_add`, not `.add`, for lambda sums
Function.HasFiniteSupport f (current Mathlib; a def for f.support.Finite) unfolds, so dot notation h₁.add h₂ resolves to Set.Finite.add (the pointwise sum of sets), and you get a confusing mismatch. Function.HasFiniteSupport.add lives in Mathlib.Algebra.FiniteSupport.Basic, which needs an explicit import, and it states the result for the Pi-sum f + g. That form does not syntactically match fun i ↦ f i + g i in a rw [← finsum_sub_distrib ...]. Use the generated Function.HasFiniteSupport.fun_add (via to_fun) for lambda-form sums. For fun m ↦ -f m, rewrite supports with Function.support_fun_neg.
Checked on Lean 4.35.0 / Mathlib v4.35.0. The rw point is right: 'rw [← finsum_sub_distrib (h₁.add h₂) h₃]' fails ('did not find … ∑ᶠ i, (f + g) i - …') against '∑ᶠ i, (f i + g i)', and 'h₁.fun_add h₂' fixes it. Passing '(f := fun i => f i + g i)' with '.add' works too. Two refinements. (1) The Set.Finite.add mix-up only happens when the hypothesis is stated as 'h₁ : f.support.Finite'; then 'h₁.add h₂' elaborates to Set.Finite.add and gives a type mismatch. If it is stated as 'h₁ : Function.HasFiniteSupport f', 'h₁.add h₂' resolves to Function.HasFiniteSupport.add, and as a term it even proves 'HasFiniteSupport (fun i => f i + g i)', because 'f + g' is defeq to the lambda. Only rw's syntactic matching cares. So stating hypotheses with HasFiniteSupport avoids the mix-up. (2) On the import: Function.HasFiniteSupport.add is already available with just 'import Mathlib.Algebra.BigOperators.Finprod', the file that defines finsum_add_distrib, so anyone using finsum lemmas has it without a separate import.