filtered finset cardinality

Stream: Is there code for X?

[Evan Lohn]

Wasn't sure how to use properties of cardinality and/or finsets to show that the number of 2d indices from some finite grid satisfying some condition is equal to the sum over all rows in the grid of the number of elements satisfying the condition in the row. Am I unaware of some super-helpful lemma?

import data.finset.basic
import tactic.linarith
import data.matrix.basic

open_locale classical
noncomputable theory

variables (M N: Type*) (flatInds : finset N) (boxInds : finset (N × N)) (filter_func : M → (N × N) → Prop)

def boxInds := finset.product flatInds flatInds

lemma split_card (x: M) :
  (finset.filter (filter_func x) boxInds).card =
    flatInds.sum (
      λ (row : N), (finset.filter (filter_func x) ([row].to_finset.product flatInds)).card
    ) :=
begin
  sorry
end

[Yaël Dillies]

This is tricky without knowing your way around the library!

[Yaël Dillies]

You're writing the RHS in a weird way. It's better to use flatInds.image (λ column, (row, column)). Then you should be able to get it using docs#finset.product_eq_bUnion, docs#finset.filter_bUnion, docs#finset.card_bUnion.