piAntidiag congruence

Stream: Is there code for X?

[Ralf Stephan]

Is the following true? If so, is there a congruence lemma to prove it?

import Mathlib
set_option autoImplicit false

open Nat Finset

example (n : ℕ) (t₁ t₂ : Type) [DecidableEq t₁] [DecidableEq t₂] (S : Finset t₁) (T : Finset t₂)
    (h : S.card = T.card) : (S.piAntidiag n).card = (T.piAntidiag n).card := by
  sorry

[Ralf Stephan]

For example, does this hold?

((range 2).piAntidiag n).card = ({true, false}.piAntidiag n).card

[Daniel Weber]

I believe it should be true, yes. To prove this you can apply docs#Finset.equivOfCardEq to h and then use docs#Finset.card_bij and explicitly give a bijection, or you could prove (S.piAntidiag n).card = (S.card + n - 1).choose n

[Daniel Weber]

I think I already saw stars and bars in Lean somewhere, but I can't remember where

[Daniel Weber]

I found #11380. @Yaël Dillies , did you PR Cut.lean?

[Yaël Dillies]

Given that the file doesn't exist in APAP anymore, yes I must have

[Yaël Dillies]

Stars and bars in Mathlib is stated using docs#Sym

[Ralf Stephan]

Thanks!