α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ Finset.card (x.fst ∪ e • x.snd) + Finset.card (x.snd ∩ e⁻¹ • x.fst) = Finset.card x.fst + Finset.card x.snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ Finset.card (mulDysonEtransform e x).fst + Finset.card (mulDysonEtransform e x).snd =
    Finset.card x.fst + Finset.card x.snd
dsimp
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ Finset.card (x.fst ∪ e • x.snd) + Finset.card (x.snd ∩ e⁻¹ • x.fst) = Finset.card x.fst + Finset.card x.snd
rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm,
  card_union_add_card_inter, card_smul_finset]