no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ card (mulEtransformLeft e x).fst + card (mulEtransformLeft e x).snd +
      (card (mulEtransformRight e x).fst + card (mulEtransformRight e x).snd) =
    card x.fst + card x.snd + (card x.fst + card x.snd)
rw [add_add_add_comm, mulEtransformLeft.card, mulEtransformRight.card, ← mul_add, two_mul]