Theorem: IMOSL.IMO2009C1.symmDiff_card_mod_two (IMOSLLean4/IMO2009/C1/C1.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
A B : Finset α
⊢ (symmDiff A B).card % 2 = (A.card + B.card) % 2
Tactic:
rw [← symmDiff_card_add_two_mul_inter_card, Nat.add_mul_mod_self_left]
State after:
no goals