α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ card
      (filter ((fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) ∘ ↑(Equiv.prodComm (α × α) (α × α)).symm)
        (map (Equiv.toEmbedding (Equiv.prodComm (α × α) (α × α))) ((s ×ˢ s) ×ˢ t ×ˢ t))) =
    multiplicativeEnergy t s
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ multiplicativeEnergy s t = multiplicativeEnergy t s
rw [multiplicativeEnergy, ← Finset.card_map (Equiv.prodComm _ _).toEmbedding, map_filter]
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ card
      (filter ((fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) ∘ ↑(Equiv.prodComm (α × α) (α × α)).symm)
        (map (Equiv.toEmbedding (Equiv.prodComm (α × α) (α × α))) ((s ×ˢ s) ×ˢ t ×ˢ t))) =
    multiplicativeEnergy t s
simp [-Finset.card_map, eq_comm, multiplicativeEnergy, mul_comm, map_eq_image, Function.comp]