Finset subset card diff 1 has `cons` equal representation

Stream: Is there code for X?

[Jihoon Hyun]

theorem subset_card_succ_eq_cons {α : Type*}
  {s t : Finset α} (h₁ : s ⊆ t) (h₂ : s.card + 1 = t.card)
  {a : α} (h₃ : a ∈ t) (h₄ : a ∉ s) :
    Finset.cons a s h₄ = t := by
  apply Finset.eq_of_subset_of_card_le _ (by simp; omega)
  intro _ h
  apply Or.elim (Finset.mem_cons.mp h) <;> intro h
  · exact h ▸ h₃
  · exact h₁ h

It seems like there is no such lemma present. Please tell me if I'm wrong. Also, I'll make a pull request on this shortly, but I'm not sure where the lemma should be placed. Maybe around line 326 of Mathlib.Data.Finset.Card.lean?

[Yaël Dillies]

You're missing a lemma, namely docs#Finset.cons_subset

[Yaël Dillies]

So the proof of your lemma is just eq_subset_of_card_le (cons_subset.2 \<h\_3, h\_1\>) (by simpa) (sorry for the lack of unicode, I'm on my phone) and I don't think it's worth having as a separate lemma

[Jihoon Hyun]

neat!

[Yaël Dillies]

Morally, your lemma is just a variation of eq_subset_of_card_le with one lemma specialised to Finset.cons. The solution is to unspecialise and then apply the general lemma, rather than adding a specialised lemma (of which there would be many)