Can't rw Finset.inclusion_exclusion_card_biUnion

Stream: new members

[Luis Berlioz]

I'm trying to use the Finset.inclusion_exclusion_card_biUnion Theorem in mathlib, or any theorem in the Inclusion-Exclusion file.

Here's what I've tried:

import Mathlib

def f: ℕ → Finset ℕ
| 0 => {12, 13}
| 1 => {13, 14}
| _ => ∅

#eval ({0,1}: Finset ℕ ).biUnion f -- this works, outputs {12, 13, 14}

example : (({0,1}: Finset ℕ ).biUnion f).card = 3 := by
 rw [Finset.inclusion_exclusion_sum_biUnion ({0,1}: Finset ℕ) f]

This gives me the error message:

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
↑({0, 1}.biUnion f).card
⊢ ({0, 1}.biUnion f).card = 3

Any MWE on how to use this result would also be very helpful.

[Aaron Liu]

In the web editor, I get the error

tactic 'rewrite' failed, did not find instance of the pattern in the target expression
∑ a ∈ {0, 1}.biUnion f, ?f a
⊢ ({0, 1}.biUnion f).card = 3

[Aaron Liu]

Here's an example

import Mathlib

def f: ℕ → Finset ℕ
| 0 => {12, 13}
| 1 => {13, 14}
| _ => ∅

#eval ({0,1}: Finset ℕ ).biUnion f -- this works, outputs {12, 13, 14}

example : (({0,1}: Finset ℕ).biUnion f).card = 3 := by
  zify
  rw [Finset.inclusion_exclusion_card_biUnion ({0,1}: Finset ℕ) f]

[Luis Berlioz]

Nice, thanks!