Inclusion–exclusion (two sets)

import Mathlib

theorem incl_excl_two {α : Type*} [DecidableEq α] (A B : Finset α) : (A ∪ B).card = A.card + B.card - (A ∩ B).card := by
  have := Finset.card_union_add_card_inter A B
  omega