α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ card (s ×ˢ t) ≤ multiplicativeEnergy s t
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ card s * card t ≤ multiplicativeEnergy s t
rw [← card_product]
α : 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
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ card (s ×ˢ t) ≤ multiplicativeEnergy s t
refine'
  card_le_card_of_inj_on (@fun x => ((x.1, x.1), x.2, x.2)) (by
  simp only [ ← and_imp, mem_product, and_imp, Prod.forall, mem_filter,
      and_self, and_true, imp_self, implies_true]) fun a _ b _ => _
α : 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
α : 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
simp only [Prod.mk.inj_iff, and_self_iff, and_imp]
no goals
α : 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
exact Prod.ext
no goals
α : 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)
simp only [ ← and_imp, mem_product, and_imp, Prod.forall, mem_filter,
  and_self, and_true, imp_self, implies_true]