-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive card_sq_le_card_mul_addEnergy]
lemma card_sq_le_card_mul_mulEnergy (s t u : Finset α) :
    ((s ×ˢ t).filter fun (a, b) ↦ a * b ∈ u).card ^ 2 ≤ u.card * Eₘ[s, t]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #u *
      ∑ c ∈ s * t,
        #(filter
              (fun x =>
                match x with
                | (a, b) => a * b = c)
              (s ×ˢ t)) ^
          2 =
    #u * Eₘ[s, t]

Tactic:
rw [mulEnergy_eq_sum_sq']

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #u *
      ∑ c ∈ u,
        #(filter
              (fun x =>
                match x with
                | (a, b) => a * b = c)
              (s ×ˢ t)) ^
          2 ≤
    #u *
      ∑ c ∈ s * t,
        #(filter
              (fun x =>
                match x with
                | (a, b) => a * b = c)
              (s ×ˢ t)) ^
          2

Tactic:
refine mul_le_mul_left' (sum_le_sum_of_ne_zero ?_) _

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ ∀ x ∈ u,
    #(filter
              (fun x_1 =>
                match x_1 with
                | (a, b) => a * b = x)
              (s ×ˢ t)) ^
          2 ≠
        0 →
      x ∈ s * t

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ ∀ x ∈ u,
    #(filter
              (fun x_1 =>
                match x_1 with
                | (a, b) => a * b = x)
              (s ×ˢ t)) ^
          2 ≠
        0 →
      x ∈ s * t

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

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ (∑ c ∈ u,
        #(filter
            (fun x =>
              match x with
              | (a, b) => a * b = c)
            (s ×ˢ t))) ^
      2 ≤
    #u *
      ∑ c ∈ u,
        #(filter
              (fun x =>
                match x with
                | (a, b) => a * b = c)
              (s ×ˢ t)) ^
          2

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

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #(filter
          (fun x =>
            match x with
            | (a, b) => a * b ∈ u)
          (s ×ˢ t)) ^
      2 =
    (∑ c ∈ u,
        #(filter
            (fun x =>
              match x with
              | (a, b) => a * b = c)
            (s ×ˢ t))) ^
      2

Tactic:
rw [← sum_card_fiberwise_eq_card_filter]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #(filter
          (fun x =>
            match x with
            | (a, b) => a * b ∈ u)
          (s ×ˢ t)) ^
      2 ≤
    #u * Eₘ[s, t]

Tactic:
calc
  _ = (∑ c ∈ u, ((s ×ˢ t).filter fun (a, b) ↦ a * b = c).card) ^ 2 := by
      rw [← sum_card_fiberwise_eq_card_filter]
  _ ≤ u.card * ∑ c ∈ u, ((s ×ˢ t).filter fun (a, b) ↦ a * b = c).card ^ 2 := by
      simpa using sum_mul_sq_le_sq_mul_sq (R := ℕ) _ 1 _
  _ ≤ u.card * ∑ c ∈ s * t, ((s ×ˢ t).filter fun (a, b) ↦ a * b = c).card ^ 2 := by
      refine mul_le_mul_left' (sum_le_sum_of_ne_zero ?_) _
      aesop (add simp [filter_eq_empty_iff]) (add unsafe mul_mem_mul)
  _ = u.card * Eₘ[s, t] := by rw [mulEnergy_eq_sum_sq']

Result:
no goals