awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∪ e • x.2 ∪ e • (x.2 ∩ e⁻¹ • x.1) = x.1 ∪ e • x.2
have fst : x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2
Tactic: rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ∩ e⁻¹ • (x.1 ∪ e • x.2) = x.2 ∩ e⁻¹ • x.1
have snd : x.2 ∩ e⁻¹ • x.1 ⊆ x.2 ∪ e⁻¹ • x.1
Tactic: rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (x.2 ∩ e⁻¹ • x.1) ⊆ x.1 ∪ e • x.2
have rw : x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2
Tactic: rw [smul_finset_inter, smul_inv_smul, inter_comm]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
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
have refine : op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2
Tactic: refine inter_mul_union_subset_union.trans (union_subset Subset.rfl ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2
have rw : x.1 * e • e⁻¹ • x.2 ⊆ x.1 * x.2
Tactic: rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
rw : x.1 * e • e⁻¹ • x.2 ⊆ x.1 * x.2
⊢ op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2
have rw₁ : x.1 * x.2 ⊆ x.1 * x.2
Tactic: rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
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
have refine : op e • x.1 * e⁻¹ • x.2 ⊆ x.1 * x.2
Tactic: refine union_mul_inter_subset_union.trans (union_subset Subset.rfl ?_)
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
⊢ #x.1 + #(op e • x.1) = 2 * #x.1
have rw : #x.1 + #x.1 = 2 * #x.1
Tactic: rw [card_smul_finset, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
rw : #x.1 + #x.1 = 2 * #x.1
⊢ #x.1 + #(op e • x.1) = 2 * #x.1
have rw₁ : #x.1 + #x.1 = #x.1 + #x.1
Tactic: rw [card_smul_finset, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
⊢ #x.2 + #(e⁻¹ • x.2) = 2 * #x.2
have rw : #x.2 + #x.2 = 2 * #x.2
Tactic: rw [card_smul_finset, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
rw : #x.2 + #x.2 = 2 * #x.2
⊢ #x.2 + #(e⁻¹ • x.2) = 2 * #x.2
have rw₁ : #x.2 + #x.2 = #x.2 + #x.2
Tactic: rw [card_smul_finset, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Group α
e : α
x : Finset α × Finset α
⊢ #(mulETransformLeft e x).1 + #(mulETransformLeft e x).2 +
      (#(mulETransformRight e x).1 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)
have 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)
Tactic: rw [add_add_add_comm, mulETransformLeft.card, mulETransformRight.card, ← mul_add, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
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)
⊢ #(mulETransformLeft e x).1 + #(mulETransformLeft e x).2 +
      (#(mulETransformRight e x).1 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)
have rw₁ : 2 * #x.1 + (#(mulETransformLeft e x).2 + #(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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
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)
⊢ #(mulETransformLeft e x).1 + #(mulETransformLeft e x).2 +
      (#(mulETransformRight e x).1 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)
have rw₂ : 2 * #x.1 + 2 * #x.2 = #x.1 + #x.2 + (#x.1 + #x.2)
Tactic: rw [add_add_add_comm, mulETransformLeft.card, mulETransformRight.card, ← mul_add, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
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)
⊢ #(mulETransformLeft e x).1 + #(mulETransformLeft e x).2 +
      (#(mulETransformRight e x).1 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)
have rw₃ : 2 * (#x.1 + #x.2) = #x.1 + #x.2 + (#x.1 + #x.2)
Tactic: rw [add_add_add_comm, mulETransformLeft.card, mulETransformRight.card, ← mul_add, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.ETransform (goal)
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)
⊢ #(mulETransformLeft e x).1 + #(mulETransformLeft e x).2 +
      (#(mulETransformRight e x).1 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)
have rw₄ : #x.1 + #x.2 + (#x.1 + #x.2) = #x.1 + #x.2 + (#x.1 + #x.2)
Tactic: rw [add_add_add_comm, mulETransformLeft.card, mulETransformRight.card, ← mul_add, two_mul]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ #s * #t ≤ Eₘ[s, t]
have rw : #(s ×ˢ t) ≤ Eₘ[s, t]
Tactic: rw [← card_product]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
h : 0 < Eₘ[s, t]
⊢ s.Nonempty ∧ t.Nonempty
have inl : ∀ (h : 0 < Eₘ[∅, t]), False
Tactic: by_contra! +distrib rfl | rfl
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
h : 0 < Eₘ[s, t]
inl : ∀ (h : 0 < Eₘ[∅, t]), False
⊢ s.Nonempty ∧ t.Nonempty
have inr : ∀ (h : 0 < Eₘ[s, ∅]), False
Tactic: by_contra! +distrib rfl | rfl
Cleared hypotheses: t, h
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
⊢ 0 < Eₘ[s] ↔ s.Nonempty
have rw : s.Nonempty ∧ s.Nonempty ↔ s.Nonempty
Tactic: rw [mulEnergy_pos_iff, and_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
rw : s.Nonempty ∧ s.Nonempty ↔ s.Nonempty
⊢ 0 < Eₘ[s] ↔ s.Nonempty
have rw₁ : s.Nonempty ↔ s.Nonempty
Tactic: rw [mulEnergy_pos_iff, and_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
⊢ Eₘ[s] = 0 ↔ s = ∅
have rw : s = ∅ ∨ s = ∅ ↔ s = ∅
Tactic: rw [mulEnergy_eq_zero_iff, or_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s : Finset α
rw : s = ∅ ∨ s = ∅ ↔ s = ∅
⊢ Eₘ[s] = 0 ↔ s = ∅
have rw₁ : s = ∅ ↔ s = ∅
Tactic: rw [mulEnergy_eq_zero_iff, or_self_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ Eₘ[s, t] = ∑ a ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = a})) 2
have 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})
Tactic: simp_rw [mulEnergy_eq_card_filter, sq, ← card_product]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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}) =
    ∑ x ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x})
have 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}) sorry)
Tactic: rw [← card_disjiUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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}) ⋯)
⊢ #({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})
have h : (↑(s * t) : Set α).PairwiseDisjoint (α := Finset ((α × α) × α × α)) fun (x : α) ↦
  {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}
Tactic: rw [← card_disjiUnion]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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}) =
    card (α := (α × α) × α × α)
      ((s * t).disjiUnion (fun (x : α) ↦ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x} ×ˢ {xy ∈ s ×ˢ t | xy.1 * xy.2 = x}) ⋯)
have 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}) sorry
Tactic: congr
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
inst_2 : Fintype α
s t : Finset α
⊢ Eₘ[s, t] = ∑ a : α, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = a})) 2
have 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)
Tactic: rw [mulEnergy_eq_sum_sq']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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
have 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
Tactic: rw [← sum_card_fiberwise_eq_card_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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
have refine : ∀ x ∈ u, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = x})) 2 ≠ 0 → x ∈ s * t
Tactic: refine mul_le_mul_right (sum_le_sum_of_ne_zero ?_) _
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
⊢ #u * ∑ c ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 2 = #u * Eₘ[s, t]
have 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
Tactic: rw [mulEnergy_eq_sum_sq']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t u : Finset α
⊢ HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u})) 2 ≤ #u * Eₘ[s, t]
have _ : 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: 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']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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 (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u})) 2 ≤ #u * Eₘ[s, t]
have _₁ : 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: 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']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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
⊢ HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u})) 2 ≤ #u * Eₘ[s, t]
have _₂ : #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: 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']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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
⊢ HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ u})) 2 ≤ #u * Eₘ[s, t]
have _₃ : #u * ∑ c ∈ s * t, HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 = c})) 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']
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Mul α
s t : Finset α
⊢ HPow.hPow (β := ℕ) (#s) 2 * HPow.hPow (β := ℕ) (#t) 2 = HPow.hPow (β := ℕ) (#({xy ∈ s ×ˢ t | xy.1 * xy.2 ∈ s * t})) 2
have rw : ∀ x ∈ s ×ˢ t, x.1 * x.2 ∈ s * t
Tactic: rw [filter_eq_self.2, card_product, mul_pow]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommMonoid α
s t : Finset α
⊢ Eₘ[s, t] = Eₘ[t, s]
have 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]
Tactic: rw [mulEnergy, ← Finset.card_map (Equiv.prodComm _ _).toEmbedding, map_filter]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : CommGroup α
inst_2 : Fintype α
t : Finset α
⊢ Eₘ[univ, t] = Fintype.card α * HPow.hPow (β := ℕ) (#t) 2
have 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))
Tactic: simp only [mulEnergy, univ_product_univ, Fintype.card, sq, ← card_product]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (hypothesis)
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₁, b₁, c₁) = (a₂, b₂, c₂)
have h₁ : (a₁ * c₁ = a₂ * c₂ ∧ a₁ * b₁ = a₂ * b₂) ∧ b₁ = b₂ ∧ c₁ = c₂
Tactic: simp_rw [f, Prod.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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₂
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)
have 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₁)
Tactic: obtain ⟨h, rfl, rfl⟩ := h
Cleared hypotheses: b₂, c₂, h₂, h
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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₁
⊢ (a₁, b₁, c₁) = (a₂, b₁, c₁)
have rw : (a₂, b₁, c₁) = (a₂, b₁, c₁)
Tactic: rw [mul_right_cancel h.1]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (hypothesis)
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)
⊢ #({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))
have this : 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]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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 (α × α × α))
⊢ #({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))
have 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)))
Tactic: rw [← card_image_of_injOn this]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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 (α × α × α))
⊢ #({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)))
have 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))
Tactic: congr with a
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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 : (α × α) × α × α
⊢ 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))
have 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
Tactic: simp only [mem_filter, mem_product, mem_univ, true_and, mem_image,
    Prod.exists]
-- Lean 4 proof step from Mathlib.Combinatorics.Additive.Energy (goal)
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 : (α × α) × α × α
⊢ (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
have e_s : (∃ (a_1 : α) (a_2 : α) (b : α), (a_2 ∈ t ∧ b ∈ t) ∧ f (a_1, a_2, b) = a) →
  (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2
Tactic: refine ⟨fun h => ⟨a.1.1 * a.2.2⁻¹, _, _, h.1, by simp [f, mul_right_comm, h.2]⟩, ?_⟩