awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
⊢ (mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2

Tactic:
inter_mul_union_subset_union.trans (union_subset Subset.rfl ?_)

Premises used: Finset.union_subset, Finset.Subset.rfl, Set.Mem, setOf, HasSubset.Subset.trans, Finset.inter_mul_union_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
refine : op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2
⊢ (mulETransformLeft e x).1 * (mulETransformLeft e x).2 ⊆ x.1 * x.2

Tactic:
refine inter_mul_union_subset_union.trans (union_subset Subset.rfl ?_)

Premises used: Finset.union_subset, Finset.Subset.rfl, HasSubset.Subset.trans, Finset.inter_mul_union_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
rw : x.1 * e • e⁻¹ • x.2 ⊆ x.1 * x.2
rw₁ rw₂ : x.1 * x.2 ⊆ x.1 * x.2
⊢ op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2

Tactic:
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]

Premises used: Finset.op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
⊢ (mulETransformRight e x).1 * (mulETransformRight e x).2 ⊆ x.1 * x.2

Tactic:
union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)

Premises used: Finset.union_subset, Finset.Subset.rfl, Set.Mem, setOf, HasSubset.Subset.trans, Finset.union_mul_inter_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
refine : op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2
⊢ (mulETransformRight e x).1 * (mulETransformRight e x).2 ⊆ x.1 * x.2

Tactic:
refine union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)

Premises used: Finset.union_subset, Finset.Subset.rfl, HasSubset.Subset.trans, Finset.union_mul_inter_subset_union
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
rw : #x.1 + #x.1 = 2 * #x.1
rw₁ rw₂ : #x.1 + #x.1 = #x.1 + #x.1
⊢ #x.1 + #(op e • x.1) = 2 * #x.1

Tactic:
rw [card_smul_finset, two_mul]

Premises used: two_mul, Finset.card_smul_finset
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
rw : #x.2 + #x.2 = 2 * #x.2
rw₁ rw₂ : #x.2 + #x.2 = #x.2 + #x.2
⊢ #x.2 + #(e⁻¹ • x.2) = 2 * #x.2

Tactic:
rw [card_smul_finset, two_mul]

Premises used: two_mul, Finset.card_smul_finset
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
rw :
  #(mulETransformLeft e x).1 + #(mulETransformRight e x).1 +
      (#(mulETransformLeft e x).2 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)
rw₁ : 2 * #x.1 + (#(mulETransformLeft e x).2 + #(mulETransformRight e x).2) = #x.1 + #x.2 + (#x.1 + #x.2)
rw₂ : 2 * #x.1 + 2 * #x.2 = #x.1 + #x.2 + (#x.1 + #x.2)
rw₃ : 2 * (#x.1 + #x.2) = #x.1 + #x.2 + (#x.1 + #x.2)
rw₄ rw₅ : #x.1 + #x.2 + (#x.1 + #x.2) = #x.1 + #x.2 + (#x.1 + #x.2)
⊢ #(mulETransformLeft e x).1 + #(mulETransformLeft e x).2 +
      (#(mulETransformRight e x).1 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)

Tactic:
rw [add_add_add_comm, mulETransformLeft.card, mulETransformRight.card, ← mul_add, two_mul]

Premises used: two_mul, Finset.mulETransformLeft.card, mul_add, add_add_add_comm, Finset.mulETransformRight.card
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulETransformLeft e⁻¹ x = (mulETransformRight e x.swap).swap

Tactic:
simp [-op_inv, op_smul_eq_smul, mulETransformLeft, mulETransformRight]

Premises used: Finset.mulETransformLeft, Finset.mulETransformRight, MulOpposite.op_inv, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Combinatorics.Additive.ETransform
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulETransformRight e⁻¹ x = (mulETransformLeft e x.swap).swap

Tactic:
simp [-op_inv, op_smul_eq_smul, mulETransformLeft, mulETransformRight]

Premises used: Finset.mulETransformLeft, Finset.mulETransformRight, MulOpposite.op_inv, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s₁ s₂ t₁ t₂ : Finset α
hs : s₁ ⊆ s₂
ht : t₁ ⊆ t₂
⊢ #({x ∈ (s₁ ×ˢ s₁) ×ˢ t₁ ×ˢ t₁ | x.1.1 * x.2.1 = x.1.2 * x.2.2}) ≤
    #({x ∈ (s₂ ×ˢ s₂) ×ˢ t₂ ×ˢ t₂ | x.1.1 * x.2.1 = x.1.2 * x.2.2})

Tactic:
gcongr
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s₁ s₂ t : Finset α
hs : s₁ ⊆ s₂
⊢ Eₘ[s₁, t] ≤ Eₘ[s₂, t]

Tactic:
mulEnergy_mono hs Subset.rfl

Premises used: Finset.Subset.rfl, Finset.mulEnergy_mono
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t₁ t₂ : Finset α
ht : t₁ ⊆ t₂
⊢ Eₘ[s, t₁] ≤ Eₘ[s, t₂]

Tactic:
mulEnergy_mono Subset.rfl ht

Premises used: Finset.Subset.rfl, Finset.mulEnergy_mono
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
rw : #(s ×ˢ t) ≤ Eₘ[s, t]
⊢ #s * #t ≤ Eₘ[s, t]

Tactic:
rw [← card_product]

Premises used: Finset.card_product
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ Set.MapsTo (fun (x : α × α) ↦ ((x.1, x.1), x.2, x.2)) (↑(s ×ˢ t) : Set (α × α))
    (↑({x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2}) : Set ((α × α) × α × α))

Tactic:
simp [Set.MapsTo]

Premises used: Set.MapsTo
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ Set.InjOn (β := (α × α) × α × α) (fun (x : α × α) ↦ ((x.1, x.1), x.2, x.2)) (↑(s ×ˢ t) : Set (α × α))

Tactic:
simp
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ #(s ×ˢ t) ≤ Eₘ[s, t]

Tactic:
exact card_le_card_of_injOn (fun x => ((x.1, x.1), x.2, x.2)) (by simp [Set.MapsTo]) (by simp)

Premises used: Finset.card_le_card_of_injOn, Prod.mk
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
⊢ HPow.hPow (β := ℕ) (#s) 2 ≤ Eₘ[s]

Tactic:
sq #s ▸ le_mulEnergy

Premises used: Eq.rec, sq, Finset.le_mulEnergy, Finset.card, Eq.symm
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ 0 < Eₘ[s, t]

Tactic:
(mul_pos hs.card_pos ht.card_pos).trans_le le_mulEnergy

Premises used: Finset.Nonempty.card_pos, Finset.le_mulEnergy, mul_pos, LT.lt.trans_le
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
hs : s.Nonempty
⊢ 0 < Eₘ[s]

Tactic:
mulEnergy_pos hs hs

Premises used: Finset.mulEnergy_pos
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
t : Finset α
⊢ Eₘ[∅, t] = 0

Tactic:
simp [mulEnergy]

Premises used: Finset.mulEnergy
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
⊢ Eₘ[s, ∅] = 0

Tactic:
simp [mulEnergy]

Premises used: Finset.mulEnergy
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
h : 0 < Eₘ[s, t]
inl : ∀ (h : 0 < Eₘ[∅, t]), False
inr : ∀ (h : 0 < Eₘ[s, ∅]), False
⊢ s.Nonempty ∧ t.Nonempty

Tactic:
by_contra! +distrib rfl | rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
t : Finset α
h : 0 < Eₘ[∅, t]
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
h : 0 < Eₘ[s, ∅]
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ Eₘ[s, t] = 0 ↔ s = ∅ ∨ t = ∅

Tactic:
simp [← (Nat.zero_le _).not_lt_iff_eq', imp_iff_or_not, or_comm]

Premises used: Nat.zero_le, LE.le.not_lt_iff_eq', or_comm, imp_iff_or_not
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
rw : s.Nonempty ∧ s.Nonempty ↔ s.Nonempty
rw₁ rw₂ : s.Nonempty ↔ s.Nonempty
⊢ 0 < Eₘ[s] ↔ s.Nonempty

Tactic:
rw [mulEnergy_pos_iff, and_self_iff]

Premises used: Finset.mulEnergy_pos_iff, and_self_iff
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
rw : s = ∅ ∨ s = ∅ ↔ s = ∅
rw₁ rw₂ : s = ∅ ↔ s = ∅
⊢ Eₘ[s] = 0 ↔ s = ∅

Tactic:
rw [mulEnergy_eq_zero_iff, or_self_iff]

Premises used: or_self_iff, Finset.mulEnergy_eq_zero_iff
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ ∀ (i : (α × α) × α × α),
    i ∈ {x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2} ↔
      Membership.mem (α := (α × α) × α × α) ({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2})
        ((Equiv.prodProdProdComm α α α α : (a : (α × α) × α × α) → (α × α) × α × α) i : (α × α) × α × α)

Tactic:
simp [and_and_and_comm]

Premises used: and_and_and_comm
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
simp_rw :
  #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    ∑ x ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x})
⊢ Eₘ[s, t] = ∑ a ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = a})) 2

Tactic:
simp_rw [mulEnergy_eq_card_filter, sq, ← card_product]

Premises used: Finset.card_product, sq, Finset.mulEnergy_eq_card_filter
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
rw :
  #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    card (α := (α × α) × α × α)
      ((s * t).disjiUnion (fun (x : α) ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ⋯)
h :
  (↑(s * t) : Set α).PairwiseDisjoint (α := Finset ((α × α) × α × α)) fun (x : α) ↦
    {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}
⊢ #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    ∑ x ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x})

Tactic:
rw [← card_disjiUnion]

Premises used: Finset.card_disjiUnion
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ (↑(s * t) : Set α).PairwiseDisjoint (α := Finset ((α × α) × α × α)) fun (x : α) ↦
    {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}

Tactic:
aesop (add simp [Set.PairwiseDisjoint, Set.Pairwise, disjoint_left])

Premises used: Set.PairwiseDisjoint, Set.Pairwise, Finset.disjoint_left
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
e_s :
  {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2} =
    (s * t).disjiUnion (fun (x : α) ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ⋯
⊢ #({x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2}) =
    card (α := (α × α) × α × α)
      ((s * t).disjiUnion (fun (x : α) ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ⋯)

Tactic:
congr
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ {x ∈ (s ×ˢ t) ×ˢ s ×ˢ t | x.1.1 * x.1.2 = x.2.1 * x.2.2} =
    (s * t).disjiUnion (fun (x : α) ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ⋯

Tactic:
aesop (add unsafe mul_mem_mul)

Premises used: Finset.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
inst_2 : Fintype α
s t : Finset α
rw :
  Eq (α := ℕ) (∑ a ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = a})) 2)
    (∑ a : α, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = a})) 2)
⊢ Eₘ[s, t] = ∑ a : α, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = a})) 2

Tactic:
rw [mulEnergy_eq_sum_sq']

Premises used: Finset.mulEnergy_eq_sum_sq'
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
inst_2 : Fintype α
s t : Finset α
⊢ ∀ (i : α), HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = i})) 2 ≠ 0 → i ∈ s * t

Tactic:
aesop (add simp [filter_eq_empty_iff, mul_mem_mul])

Premises used: Finset.filter_eq_empty_iff, Finset.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
inst_2 : Fintype α
s t : Finset α
⊢ Eq (α := ℕ) (∑ a ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = a})) 2)
    (∑ a : α, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = a})) 2)

Tactic:
exact Fintype.sum_subset <| by aesop (add simp [filter_eq_empty_iff, mul_mem_mul])

Premises used: Fintype.sum_subset
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
rw rw₁ :
  HPow.hPow (α := ℕ) (β := ℕ) (∑ j ∈ u, #({i ∈ s ×ˢ t | i.1 * i.2 = j})) 2 =
    HPow.hPow (α := ℕ) (β := ℕ) (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2
⊢ HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u})) 2 =
    HPow.hPow (α := ℕ) (β := ℕ) (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2

Tactic:
rw [← sum_card_fiberwise_eq_card_filter]

Premises used: Finset.sum_card_fiberwise_eq_card_filter
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
⊢ HPow.hPow (α := ℕ) (β := ℕ) (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2 ≤
    #u * ∑ c ∈ u, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2

Tactic:
simpa using sum_mul_sq_le_sq_mul_sq (R := ℕ) _ 1 _

Premises used: OfNat.ofNat, Finset.sum_mul_sq_le_sq_mul_sq
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
⊢ #u * ∑ c ∈ u, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2 ≤
    #u * ∑ c ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2

Tactic:
mul_le_mul_right (sum_le_sum_of_ne_zero ?_) _

Premises used: mul_le_mul_right, Finset.sum_le_sum_of_ne_zero
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
refine : ∀ x ∈ u, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = x})) 2 ≠ 0 → x ∈ s * t
⊢ #u * ∑ c ∈ u, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2 ≤
    #u * ∑ c ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2

Tactic:
refine mul_le_mul_right (sum_le_sum_of_ne_zero ?_) _

Premises used: mul_le_mul_right, Finset.sum_le_sum_of_ne_zero
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
⊢ ∀ x ∈ u, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = x})) 2 ≠ 0 → x ∈ s * t

Tactic:
aesop (add simp [filter_eq_empty_iff]) (add unsafe mul_mem_mul)

Premises used: Finset.filter_eq_empty_iff, Finset.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
rw rw₁ :
  #u * ∑ c ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2 =
    #u * ∑ a ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = a})) 2
⊢ #u * ∑ c ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2 = #u * Eₘ[s, t]

Tactic:
rw [mulEnergy_eq_sum_sq']

Premises used: Finset.mulEnergy_eq_sum_sq'
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
_ :
  HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u})) 2 =
    HPow.hPow (α := ℕ) (β := ℕ) (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2
_₁ :
  HPow.hPow (α := ℕ) (β := ℕ) (∑ c ∈ u, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2 ≤
    #u * ∑ c ∈ u, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2
_₂ :
  #u * ∑ c ∈ u, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2 ≤
    #u * ∑ c ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2
_₃ : #u * ∑ c ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2 = #u * Eₘ[s, t]
⊢ HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u})) 2 ≤ #u * Eₘ[s, t]

Tactic:
calc
    _ = (∑ c ∈ u, #{xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 := by
        rw [← sum_card_fiberwise_eq_card_filter]
    _ ≤ #u * ∑ c ∈ u, #{xy ∈ s ×ˢ t | xy.1 * xy.2 = c} ^ 2 := by
        simpa using sum_mul_sq_le_sq_mul_sq (R := ℕ) _ 1 _
    _ ≤ #u * ∑ c ∈ s * t, #{xy ∈ s ×ˢ t | xy.1 * xy.2 = c} ^ 2 := by
        refine mul_le_mul_right (sum_le_sum_of_ne_zero ?_) _
        aesop (add simp [filter_eq_empty_iff]) (add unsafe mul_mem_mul)
    _ = #u * Eₘ[s, t] := by rw [mulEnergy_eq_sum_sq']

Premises used: HMul.hMul, SProd.sprod, Finset.card, Finset.filter, Eq, Finset.sum
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
rw : ∀ x ∈ s ×ˢ t, x.1 * x.2 ∈ s * t
⊢ HPow.hPow (β := ℕ) (#s) 2 * HPow.hPow (β := ℕ) (#t) 2 = HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ s * t})) 2

Tactic:
rw [filter_eq_self.2, card_product, mul_pow]

Premises used: Iff.mpr, Finset.card_product, Finset.filter_eq_self, mul_pow
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ ∀ x ∈ s ×ˢ t, x.1 * x.2 ∈ s * t

Tactic:
aesop (add unsafe mul_mem_mul)

Premises used: Finset.mul_mem_mul
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
s t : Finset α
rw :
  #(filter
        ((fun (x : (α × α) × α × α) ↦ x.1.1 * x.2.1 = x.1.2 * x.2.2) ∘
          (⇑(Equiv.symm (Equiv.prodComm (α × α) (α × α))) : (a : (α × α) × α × α) → (α × α) × α × α))
        (map (Equiv.toEmbedding (Equiv.prodComm (α × α) (α × α))) ((s ×ˢ s) ×ˢ t ×ˢ t))) =
    Eₘ[t, s]
⊢ Eₘ[s, t] = Eₘ[t, s]

Tactic:
rw [mulEnergy, ← Finset.card_map (Equiv.prodComm _ _).toEmbedding, map_filter]

Premises used: Finset.map_filter, Equiv.prodComm, Finset.mulEnergy, Finset.card_map, Equiv.toEmbedding
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
s t : Finset α
⊢ #(filter
        ((fun (x : (α × α) × α × α) ↦ x.1.1 * x.2.1 = x.1.2 * x.2.2) ∘
          (⇑(Equiv.symm (Equiv.prodComm (α × α) (α × α))) : (a : (α × α) × α × α) → (α × α) × α × α))
        (map (Equiv.toEmbedding (Equiv.prodComm (α × α) (α × α))) ((s ×ˢ s) ×ˢ t ×ˢ t))) =
    Eₘ[t, s]

Tactic:
simp [mulEnergy, mul_comm, map_eq_image]

Premises used: Finset.mulEnergy, Finset.map_eq_image, mul_comm
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
simp :
  #({x ∈ SProd.sprod (α := Finset (α × α)) univ (t ×ˢ t) | x.1.1 * x.2.1 = x.1.2 * x.2.2}) =
    #(SProd.sprod (α := Finset α) univ (t ×ˢ t))
⊢ Eₘ[univ, t] = Fintype.card α * HPow.hPow (β := ℕ) (#t) 2

Tactic:
simp only [mulEnergy, univ_product_univ, Fintype.card, sq, ← card_product]

Premises used: Finset.card_product, Finset.mulEnergy, Fintype.card, Finset.univ_product_univ, sq
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
h_1 : (a₁, b₁, c₁) ∈ (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
h : f (a₁, b₁, c₁) = f (a₂, b₂, c₂)
⊢ (a₁ * c₁ = a₂ * c₂ ∧ a₁ * b₁ = a₂ * b₂) ∧ b₁ = b₂ ∧ c₁ = c₂

Tactic:
simp_rw [f, Prod.ext_iff] at h

Premises used: Prod.ext_iff
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
h_1 : (a₁, b₁, c₁) ∈ (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
h : (a₁ * c₁ = a₂ * c₂ ∧ a₁ * b₁ = a₂ * b₂) ∧ b₁ = b₂ ∧ c₁ = c₂
obtain :
  ∀ (h₂ : (a₂, b₁, c₁) ∈ (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α)))
    (h : a₁ * c₁ = a₂ * c₁ ∧ a₁ * b₁ = a₂ * b₁), (a₁, b₁, c₁) = (a₂, b₁, c₁)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)

Tactic:
obtain ⟨h, rfl, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
h_1 : (a₁, b₁, c₁) ∈ (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
a₂ : α
h₂ : (a₂, b₁, c₁) ∈ (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
h : a₁ * c₁ = a₂ * c₁ ∧ a₁ * b₁ = a₂ * b₁
rw rw₁ : (a₂, b₁, c₁) = (a₂, b₁, c₁)
⊢ (a₁, b₁, c₁) = (a₂, b₁, c₁)

Tactic:
rw [mul_right_cancel h.1]

Premises used: And.left, mul_right_cancel
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
⊢ Set.InjOn f (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))

Tactic:
have : (↑((univ : Finset α) ×ˢ t ×ˢ t) : Set (α × α × α)).InjOn f := by
    rintro ⟨a₁, b₁, c₁⟩ _ ⟨a₂, b₂, c₂⟩ h₂ h
    simp_rw [f, Prod.ext_iff] at h
    obtain ⟨h, rfl, rfl⟩ := h
    rw [mul_right_cancel h.1]
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
rw :
  #({x ∈ SProd.sprod (α := Finset (α × α)) univ (t ×ˢ t) | x.1.1 * x.2.1 = x.1.2 * x.2.2}) =
    #(image f (SProd.sprod (α := Finset α) univ (t ×ˢ t)))
⊢ #({x ∈ SProd.sprod (α := Finset (α × α)) univ (t ×ˢ t) | x.1.1 * x.2.1 = x.1.2 * x.2.2}) =
    #(SProd.sprod (α := Finset α) univ (t ×ˢ t))

Tactic:
rw [← card_image_of_injOn this]

Premises used: Finset.card_image_of_injOn
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
e_s :
  ∀ (a : (α × α) × α × α),
    a ∈ {x ∈ SProd.sprod (α := Finset (α × α)) univ (t ×ˢ t) | x.1.1 * x.2.1 = x.1.2 * x.2.2} ↔
      a ∈ image f (SProd.sprod (α := Finset α) univ (t ×ˢ t))
⊢ #({x ∈ SProd.sprod (α := Finset (α × α)) univ (t ×ˢ t) | x.1.1 * x.2.1 = x.1.2 * x.2.2}) =
    #(image f (SProd.sprod (α := Finset α) univ (t ×ˢ t)))

Tactic:
congr with a
-- Module: Mathlib.Combinatorics.Additive.Energy
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun (x : α × α × α) ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f (↑(SProd.sprod (α := Finset α) univ (t ×ˢ t)) : Set (α × α × α))
a : (α × α) × α × α
e_s :
  (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2 ↔
    ∃ (a_1 : α) (a_2 : α) (b : α), (a_2 ∈ t ∧ b ∈ t) ∧ f (a_1, a_2, b) = a
⊢ a ∈ {x ∈ SProd.sprod (α := Finset (α × α)) univ (t ×ˢ t) | x.1.1 * x.2.1 = x.1.2 * x.2.2} ↔
    a ∈ image f (SProd.sprod (α := Finset α) univ (t ×ˢ t))

Tactic:
simp only [mem_filter, mem_product, mem_univ, true_and, mem_image,
    Prod.exists]

Premises used: Finset.mem_univ, Finset.mem_image, Finset.mem_filter, Prod.exists, Finset.mem_product, true_and