[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ card s * card t ≤ multiplicativeEnergy s t
[PROOFSTEP]
rw [← card_product]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ card (s ×ˢ t) ≤ multiplicativeEnergy s t
[PROOFSTEP]
refine'
  card_le_card_of_inj_on (@fun x => ((x.1, x.1), x.2, x.2))
    (by
      -- porting note: changed this from a `simp` proof without `only` because of a timeoutsimp only [← and_imp,
        mem_product, and_imp, Prod.forall, mem_filter, and_self, and_true, imp_self, implies_true])
    fun a _ b _ => _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ ∀ (a : α × α),
    a ∈ s ×ˢ t →
      (fun x => ((x.fst, x.fst), x.snd, x.snd)) a ∈
        filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) ((s ×ˢ s) ×ˢ t ×ˢ t)
[PROOFSTEP]
simp only [← and_imp, mem_product, and_imp, Prod.forall, mem_filter, and_self, and_true, imp_self, implies_true]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
a : α × α
x✝¹ : a ∈ s ×ˢ t
b : α × α
x✝ : b ∈ s ×ˢ t
⊢ (fun x => ((x.fst, x.fst), x.snd, x.snd)) a = (fun x => ((x.fst, x.fst), x.snd, x.snd)) b → a = b
[PROOFSTEP]
simp only [Prod.mk.inj_iff, and_self_iff, and_imp]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
a : α × α
x✝¹ : a ∈ s ×ˢ t
b : α × α
x✝ : b ∈ s ×ˢ t
⊢ a.fst = b.fst → a.snd = b.snd → a = b
[PROOFSTEP]
exact Prod.ext
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ multiplicativeEnergy ∅ t = 0
[PROOFSTEP]
simp [multiplicativeEnergy]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ multiplicativeEnergy s ∅ = 0
[PROOFSTEP]
simp [multiplicativeEnergy]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy s t
H : ¬(Finset.Nonempty s ∧ Finset.Nonempty t)
⊢ False
[PROOFSTEP]
simp_rw [not_and_or, not_nonempty_iff_eq_empty] at H 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy s t
H : s = ∅ ∨ t = ∅
⊢ False
[PROOFSTEP]
obtain rfl | rfl := H
[GOAL]
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s₁ s₂ t t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy ∅ t
⊢ False
[PROOFSTEP]
simp [Nat.not_lt_zero] at h 
[GOAL]
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy s ∅
⊢ False
[PROOFSTEP]
simp [Nat.not_lt_zero] at h 
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ multiplicativeEnergy s t = 0 ↔ s = ∅ ∨ t = ∅
[PROOFSTEP]
simp [← (Nat.zero_le _).not_gt_iff_eq, not_and_or, imp_iff_or_not, or_comm]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ multiplicativeEnergy s t = multiplicativeEnergy t s
[PROOFSTEP]
rw [multiplicativeEnergy, ← Finset.card_map (Equiv.prodComm _ _).toEmbedding, map_filter]
[GOAL]
α : 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
[PROOFSTEP]
simp [-Finset.card_map, eq_comm, multiplicativeEnergy, mul_comm, map_eq_image, Function.comp]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
⊢ multiplicativeEnergy univ t = Fintype.card α * card t ^ 2
[PROOFSTEP]
simp only [multiplicativeEnergy, univ_product_univ, Fintype.card, sq, ← card_product]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
⊢ card (filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t)) = card (univ ×ˢ t ×ˢ t)
[PROOFSTEP]
let f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
⊢ card (filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t)) = card (univ ×ˢ t ×ˢ t)
[PROOFSTEP]
have : (↑((univ : Finset α) ×ˢ t ×ˢ t) : Set (α × α × α)).InjOn f :=
  by
  rintro ⟨a₁, b₁, c₁⟩ _ ⟨a₂, b₂, c₂⟩ h₂ h
  simp_rw [Prod.ext_iff] at h 
  obtain ⟨h, rfl, rfl⟩ := h
  rw [mul_right_cancel h.1]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
⊢ Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
[PROOFSTEP]
rintro ⟨a₁, b₁, c₁⟩ _ ⟨a₂, b₂, c₂⟩ h₂ h
[GOAL]
case mk.mk.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : f (a₁, b₁, c₁) = f (a₂, b₂, c₂)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)
[PROOFSTEP]
simp_rw [Prod.ext_iff] at h 
[GOAL]
case mk.mk.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : (a₁ * c₁ = a₂ * c₂ ∧ a₁ * b₁ = a₂ * b₂) ∧ b₁ = b₂ ∧ c₁ = c₂
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)
[PROOFSTEP]
obtain ⟨h, rfl, rfl⟩ := h
[GOAL]
case mk.mk.mk.mk.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ : α
h₂ : (a₂, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
h : a₁ * c₁ = a₂ * c₁ ∧ a₁ * b₁ = a₂ * b₁
⊢ (a₁, b₁, c₁) = (a₂, b₁, c₁)
[PROOFSTEP]
rw [mul_right_cancel h.1]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ card (filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t)) = card (univ ×ˢ t ×ˢ t)
[PROOFSTEP]
rw [← card_image_of_injOn this]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ card (filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t)) =
    card (image f (univ ×ˢ t ×ˢ t))
[PROOFSTEP]
congr with a
[GOAL]
case e_s.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ a ∈ filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t) ↔ a ∈ image f (univ ×ˢ t ×ˢ t)
[PROOFSTEP]
simp only [mem_filter, mem_product, mem_univ, true_and_iff, mem_image, exists_prop, Prod.exists]
[GOAL]
case e_s.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ (a.snd.fst ∈ t ∧ a.snd.snd ∈ t) ∧ a.fst.fst * a.snd.fst = a.fst.snd * a.snd.snd ↔
    ∃ a_1 a_2 b, (a_2 ∈ t ∧ b ∈ t) ∧ ((a_1 * b, a_1 * a_2), a_2, b) = a
[PROOFSTEP]
refine' ⟨fun h => ⟨a.1.1 * a.2.2⁻¹, _, _, h.1, by simp [mul_right_comm, h.2]⟩, _⟩
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
h : (a.snd.fst ∈ t ∧ a.snd.snd ∈ t) ∧ a.fst.fst * a.snd.fst = a.fst.snd * a.snd.snd
⊢ ((a.fst.fst * a.snd.snd⁻¹ * a.snd.snd, a.fst.fst * a.snd.snd⁻¹ * a.snd.fst), a.snd.fst, a.snd.snd) = a
[PROOFSTEP]
simp [mul_right_comm, h.2]
[GOAL]
case e_s.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ (∃ a_1 a_2 b, (a_2 ∈ t ∧ b ∈ t) ∧ ((a_1 * b, a_1 * a_2), a_2, b) = a) →
    (a.snd.fst ∈ t ∧ a.snd.snd ∈ t) ∧ a.fst.fst * a.snd.fst = a.fst.snd * a.snd.snd
[PROOFSTEP]
rintro ⟨b, c, d, hcd, rfl⟩
[GOAL]
case e_s.a.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
b c d : α
hcd : c ∈ t ∧ d ∈ t
⊢ (((b * d, b * c), c, d).snd.fst ∈ t ∧ ((b * d, b * c), c, d).snd.snd ∈ t) ∧
    ((b * d, b * c), c, d).fst.fst * ((b * d, b * c), c, d).snd.fst =
      ((b * d, b * c), c, d).fst.snd * ((b * d, b * c), c, d).snd.snd
[PROOFSTEP]
simpa [mul_right_comm]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
⊢ multiplicativeEnergy s univ = Fintype.card α * card s ^ 2
[PROOFSTEP]
rw [multiplicativeEnergy_comm, multiplicativeEnergy_univ_left]
