Finsupps commute when supports are disjoint

Stream: Is there code for X?

[Violeta Hernández]

What it says in the title.

import Mathlib.Data.Finsupp.Basic

variable {α β : Type*} [AddZeroClass α]

example {f g : β →₀ α} (h : Disjoint f.support g.support) : f + g = g + f :=
  sorry

[Aaron Liu]

It's not too hard to prove on your own, I doubt we have this in mathlib

import Mathlib.Data.Finsupp.Basic

variable {α β : Type*} [AddZeroClass α]

example {f g : β →₀ α} (h : Disjoint f.support g.support) : f + g = g + f := by
  classical
  rw [Finset.disjoint_iff_inter_eq_empty, ← Finset.coe_inj,
    Finset.coe_inter, Finset.coe_empty, ← compl_inj_iff,
    Set.compl_empty, Set.compl_inter, Set.eq_univ_iff_forall] at h
  ext x
  specialize h x
  aesop

[Eric Wieser]

#28761

[Antoine Chambert-Loir]

The use of

theorem Finsupp.addCommute_iff {f g : β →₀ α} :
    f + g = g + f ↔ ∀ x, AddCommute (f x) (g x) := by
  rw [Finsupp.ext_iff]
  aesop

makes it clearer, but not shorter, but that additional lemma might be useful.
I also feel that a lemma is needed to shorten the 3-line rw.

[Eric Wieser]

I think that's really a lemma about Pi types and AddCommute

[Aaron Liu]

docs#Pi.addCommute_iff

[Eric Wieser]

Anyway, I've asked in the PR for the stronger version of the iff