Absolute difference of cardinality bound

Stream: Is there code for X?

[Reuven Peleg]

When trying to prove a theorem, Gemini hallucination a theorem stating

import Mathlib.Data.Finset.SymmDiff
import Mathlib.Data.Finset.Card

theorem Finset.dist_card_le_card_symmDiff {α : Type*} [DecidableEq α] (s t : Finset α) :
  dist s.card t.card ≤ (s.symmDiff t).card

Which does not seem to match and existing LEAN theorem, although mathematically correct.
Is there a similar theorem, maybe with different name or phrasing? If no, is there a place for something like this in mathlib, since I am going to prove it?

[Aaron Liu]

this is not mathematically correct I think

[Aaron Liu]

what if s = t

[Aaron Liu]

then their symmDiff is empty

[Aaron Liu]

wait no

[Reuven Peleg]

The sketch of proof is card(A) = card(A \ B) + card(A intersect B) and the same for B, then in |card(A) - card(B)| the intersection cancel out and we left with |card(A \ B) - card(B \ A)|, less then equal the sum of them, which is card(symmetric diff)

[Aaron Liu]

quick proof I put together

import Mathlib

theorem Finset.dist_card_le_card_symmDiff {α : Type*} [DecidableEq α] (s t : Finset α) :
    Nat.dist s.card t.card ≤ (symmDiff s t).card := by
  rw [symmDiff_def, Finset.sup_eq_union, Finset.card_union,
    ← Finset.inf_eq_inter, sdiff_inf_sdiff, Finset.bot_eq_empty,
    Finset.card_empty, Nat.sub_zero]
  have := Finset.card_inter_add_card_sdiff s t
  have := Finset.card_inter_add_card_sdiff t s
  have := congrArg Finset.card (Finset.inter_comm s t)
  obtain hst | hts := le_total s.card t.card
  · rw [Nat.dist_eq_sub_of_le hst]
    lia
  · rw [Nat.dist_eq_sub_of_le_right hts]
    lia

[Bhavik Mehta]

I think this makes sense for mathlib, if you want to make a PR and ping me on it

[Reuven Peleg]

@Bhavik Mehta great, working on it. Do you think it belongs to Mathlib\Data\Finset\Card.lean, Mathlib\Data\Finset\CastCard.lean, or is there a third place which makes more sense?

[Kevin Buzzard]

If you run #find_home on Aaron's proof above, does it suggest Data/Finset/Card.lean? If so then this would be a natural place to put it. But in general you shouldn't be adding imports to files so low down in the heirarchy so really the best answer is probably "the first place where it can go" which #find_home will hopefully report.

[Reuven Peleg]

i opened https://github.com/leanprover-community/mathlib4/pull/33419/files for a change in cardinality theorem only: in addition to the existing

theorem le_card_sdiff (s t : Finset α) : #t - #s ≤ #(t \ s)

I added

lemma eq_card_diff_of_sdiff (s t : Finset α) : #t - #s = #(t \ s) - #(s \ t)

So the set-theory part of the proof will be there.

@Bhavik Mehta can you review?