theorem Finset.card_inter_smul_eq_card_filter {G : Type u_1} [DecidableEq G] [Group G] (s t : Finset G) (a : G) : (s ∩ a • t).card = {x ∈ s ×ˢ t | x.1 / x.2 = a}.card

theorem Finset.card_inter_vadd_eq_card_filter {G : Type u_1} [DecidableEq G] [AddGroup G] (s t : Finset G) (a : G) : (s ∩ (a +ᵥ t)).card = {x ∈ s ×ˢ t | x.1 - x.2 = a}.card

theorem Finset.card_inter_smul_inv_eq_card_filter {G : Type u_1} [DecidableEq G] [Group G] (s t : Finset G) (a : G) : (s ∩ a • t⁻¹).card = {x ∈ s ×ˢ t | x.1 * x.2 = a}.card

theorem Finset.card_inter_vadd_neg_eq_card_filter {G : Type u_1} [DecidableEq G] [AddGroup G] (s t : Finset G) (a : G) : (s ∩ (a +ᵥ -t)).card = {x ∈ s ×ˢ t | x.1 + x.2 = a}.card