mathlib3

320ea398 - feat(data/dfinsupp/basic): add missing lemmas about `single` (#14815)

feat(data/dfinsupp/basic): add missing lemmas about `single` (#14815) These lemmas were missed in #13076: * `comap_domain_single` * `comap_domain'_single` * `sigma_curry_single` * `sigma_uncurry_single` * `extend_with_single_zero` * `extend_with_zero` These are useful since many induction principles replace a generic `dfinsupp` with `dfinsupp.single`.