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

State before:
α : Type u_1
inst✝ : DecidableEq α
A B : Finset α
⊢ (symmDiff A B).card + 2 * (A ∩ B).card = A.card + B.card
Tactic:
rw [two_mul, ← add_assoc, ← card_union_of_disjoint (disjoint_symmDiff_inter A B),
  symmDiff_union_inter_eq_union, card_union_add_card_inter]
State after:
no goals