-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive] lemma mulEnergy_eq_sum_sq' (s t : Finset α) :
    Eₘ[s, t] = ∑ a ∈ s * t, ((s ×ˢ t).filter fun (x, y) ↦ x * y = a).card ^ 2

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t)) =
    ∑ x ∈ s * t, #(filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t))

Tactic:
rw [← card_disjiUnion]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t)) =
    #((s * t).disjiUnion
        (fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)) ?h)

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ (↑(s * t)).PairwiseDisjoint fun x =>
    filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)

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

Tactic:
simp_rw [mulEnergy_eq_card_filter, sq, ← card_product]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t)) =
    ∑ x ∈ s * t, #(filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t))

Proof state:
case e_s.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
a✝ : (α × α) × α × α
⊢ ((a✝.1.1 ∈ s ∧ a✝.1.2 ∈ t) ∧ a✝.2.1 ∈ s ∧ a✝.2.2 ∈ t) ∧ a✝.1.1 * a✝.1.2 = a✝.2.1 * a✝.2.2 ↔
    ∃ a ∈ s * t, ((a✝.1.1 ∈ s ∧ a✝.1.2 ∈ t) ∧ a✝.1.1 * a✝.1.2 = a) ∧ (a✝.2.1 ∈ s ∧ a✝.2.2 ∈ t) ∧ a✝.2.1 * a✝.2.2 = a

Tactic:
aesop (add unsafe mul_mem_mul)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t)) =
    #((s * t).disjiUnion
        (fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)) ?h)

case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ (↑(s * t)).PairwiseDisjoint fun x =>
    filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)

Tactic:
swap

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ (↑(s * t)).PairwiseDisjoint fun x =>
    filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t)) =
    #((s * t).disjiUnion
        (fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)) ?h)

Proof state:
case e_s
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t) =
    (s * t).disjiUnion
      (fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)) ⋯

Tactic:
ext

Result:
case e_s.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
a✝ : (α × α) × α × α
⊢ a✝ ∈ filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t) ↔
    a✝ ∈
      (s * t).disjiUnion
        (fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)) ⋯

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ ⦃x : α⦄,
    x ∈ ↑s * ↑t →
      ∀ ⦃y : α⦄,
        y ∈ ↑s * ↑t →
          ¬x = y →
            ∀ (a b a_1 b_1 : α),
              a ∈ s →
                b ∈ t →
                  a * b = x →
                    a_1 ∈ s → b_1 ∈ t → a_1 * b_1 = x → a ∈ s → b ∈ t → a * b = y → a_1 ∈ s → b_1 ∈ t → ¬a_1 * b_1 = y

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ #(filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t)) =
    #((s * t).disjiUnion
        (fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)) ⋯)

Tactic:
congr

Result:
case e_s
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t) =
    (s * t).disjiUnion
      (fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)) ⋯

Proof state:
case e_s.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
a✝ : (α × α) × α × α
⊢ a✝ ∈ filter (fun x => x.1.1 * x.1.2 = x.2.1 * x.2.2) ((s ×ˢ t) ×ˢ s ×ˢ t) ↔
    a✝ ∈
      (s * t).disjiUnion
        (fun x => filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)) ⋯

Tactic:
simp only [mem_filter, mem_product, disjiUnion_eq_biUnion, mem_biUnion]

Result:
case e_s.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
a✝ : (α × α) × α × α
⊢ ((a✝.1.1 ∈ s ∧ a✝.1.2 ∈ t) ∧ a✝.2.1 ∈ s ∧ a✝.2.2 ∈ t) ∧ a✝.1.1 * a✝.1.2 = a✝.2.1 * a✝.2.2 ↔
    ∃ a ∈ s * t, ((a✝.1.1 ∈ s ∧ a✝.1.2 ∈ t) ∧ a✝.1.1 * a✝.1.2 = a) ∧ (a✝.2.1 ∈ s ∧ a✝.2.2 ∈ t) ∧ a✝.2.1 * a✝.2.2 = a

Proof state:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ (↑(s * t)).PairwiseDisjoint fun x =>
    filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t) ×ˢ filter (fun x_1 => x_1.1 * x_1.2 = x) (s ×ˢ t)

Tactic:
simp only [Set.PairwiseDisjoint, Set.Pairwise, coe_mul, ne_eq, disjoint_left, mem_product,
  mem_filter, not_and, and_imp, Prod.forall]

Result:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t : Finset α
⊢ ∀ ⦃x : α⦄,
    x ∈ ↑s * ↑t →
      ∀ ⦃y : α⦄,
        y ∈ ↑s * ↑t →
          ¬x = y →
            ∀ (a b a_1 b_1 : α),
              a ∈ s →
                b ∈ t →
                  a * b = x →
                    a_1 ∈ s → b_1 ∈ t → a_1 * b_1 = x → a ∈ s → b ∈ t → a * b = y → a_1 ∈ s → b_1 ∈ t → ¬a_1 * b_1 = y