Finset.map_sdiff, Finset.map_compl

Stream: Is there code for X?

[Terence Tao]

Mathlib.Data.Finset.Image contains docs#Finset.map_union, docs#Finset.map_inter, docs#Finset.map_singleton, etc., but appears to be missing these two lemmas:

import Mathlib

theorem Finset.map_sdiff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ : Finset α) (s₂ : Finset α) :
Finset.map f (s₁ \ s₂) = Finset.map f s₁ \ Finset.map f s₂ := by
  aesop

theorem Finset.map_compl {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s : Finset α)  :
Finset.map f sᶜ  = Finset.map f Finset.univ \ Finset.map f s := by
  convert Finset.map_sdiff _ _

(I found it remarkably hard to prove the former result without aesop, by the way.) Would it be worth putting them into Mathlib (with presumably a faster proof)?

[Johan Commelin]

Those definitely seem sensible to include in mathlib. By the way, do you know that aesop? will make aesop spill its secrets, so that you can find out which proof it found.

[Johan Commelin]

aesop finds a rather hands-on "chasing elements" proof.
Since docs#Finset.image_sdiff exists, here is a proof that reduces to that case:

import Mathlib

theorem Finset.map_sdiff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ : Finset α) (s₂ : Finset α) :
    Finset.map f (s₁ \ s₂) = Finset.map f s₁ \ Finset.map f s₂ := by
  simp only [Finset.map_eq_image]
  apply Finset.image_sdiff _ _ f.injective


theorem Finset.map_compl {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s : Finset α)  :
    Finset.map f sᶜ  = Finset.map f Finset.univ \ Finset.map f s :=
  Finset.map_sdiff _ _

[Johan Commelin]

The simp; apply pattern could be golfed into simpa ... using

[Eric Wieser]

I think these might be deliberately missing, since if you have the DecidableEq needed to make sense of diff and compl then map simplifies to image; but maybe they're still useful.

[Terence Tao]

For what it's worth, here is the specific use case I had for this lemma. It would be inconvenient to swap from map to image halfway through the argument, since most of the other tools I need are spelled in terms of map. Also, it seems that Finset.map_to_image isn't a simp lemma, so there doesn't seem to be a general preference within Mathlib to use the latter in place of the former.

import Mathlib

theorem Finset.map_sdiff {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s₁ : Finset α) (s₂ : Finset α) :
Finset.map f (s₁ \ s₂) = Finset.map f s₁ \ Finset.map f s₂ := by
  simp only [Finset.map_eq_image]
  apply Finset.image_sdiff _ _ f.injective

theorem Finset.map_compl {α : Type u_1} {β : Type u_2} [Fintype α] [DecidableEq α] [DecidableEq β] {f : α ↪ β} (s : Finset α)  :
Finset.map f sᶜ  = Finset.map f Finset.univ \ Finset.map f s := Finset.map_sdiff _ _

theorem sum_of_iio_last (N: ℕ) (f: Fin (N+1) → ℝ) : ∑ d in Finset.Iio (N : Fin (N+1)), f d = ∑ d : Fin N, f d.castSucc := by
  convert Finset.sum_image (s := Finset.univ) (g := Fin.castSucc) (f := f) ?_
  . rw [Fin.image_castSucc, <-Finset.map_inj (f := Fin.valEmbedding), Finset.map_compl]
    simp only [Fin.map_valEmbedding_Iio, Fin.map_valEmbedding_univ, Fin.coe_castSucc, Finset.map_singleton, Fin.valEmbedding_apply, Fin.natCast_eq_last, Fin.val_last,Finset.sdiff_singleton_eq_erase]
    convert (Finset.Iic_erase N).symm using 1
  intro _ _ _ _
  exact Fin.castSucc_inj.mp