-- Mathlib/Combinatorics/Additive/Energy.lean
@[to_additive (attr := simp)]
lemma mulEnergy_univ_left : Eₘ[univ, t] = Fintype.card α * t.card ^ 2

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
⊢ Set.InjOn f ↑(univ ×ˢ t ×ˢ t)

Tactic:
rintro ⟨a₁, b₁, c₁⟩ _ ⟨a₂, b₂, c₂⟩ h₂ h

Result:
case mk.mk.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : f (a₁, b₁, c₁) = f (a₂, b₂, c₂)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)) = #(image f (univ ×ˢ t ×ˢ t))

Tactic:
congr with a

Result:
case e_s.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ a ∈ filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t) ↔ a ∈ image f (univ ×ˢ t ×ˢ t)

Proof state:
case e_s.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ (∃ 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:
rintro ⟨b, c, d, hcd, rfl⟩

Result:
case e_s.h.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
b c d : α
hcd : c ∈ t ∧ d ∈ t
⊢ ((f (b, c, d)).2.1 ∈ t ∧ (f (b, c, d)).2.2 ∈ t) ∧
    (f (b, c, d)).1.1 * (f (b, c, d)).2.1 = (f (b, c, d)).1.2 * (f (b, c, d)).2.2

Proof state:
case e_s.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ a ∈ filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t) ↔ a ∈ image f (univ ×ˢ t ×ˢ t)

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

Result:
case e_s.h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
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

Proof state:
case mk.mk.mk.mk.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ : α
h₂ : (a₂, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
h : a₁ * c₁ = a₂ * c₁ ∧ a₁ * b₁ = a₂ * b₁
⊢ (a₁, b₁, c₁) = (a₂, b₁, c₁)

Tactic:
rw [mul_right_cancel h.1]

Result:
no goals

Proof state:
case e_s.h.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
b c d : α
hcd : c ∈ t ∧ d ∈ t
⊢ ((f (b, c, d)).2.1 ∈ t ∧ (f (b, c, d)).2.2 ∈ t) ∧
    (f (b, c, d)).1.1 * (f (b, c, d)).2.1 = (f (b, c, d)).1.2 * (f (b, c, d)).2.2

Tactic:
simpa [f, mul_right_comm]

Result:
no goals

Proof state:
case mk.mk.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : (a₁ * c₁ = a₂ * c₂ ∧ a₁ * b₁ = a₂ * b₂) ∧ b₁ = b₂ ∧ c₁ = c₂
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)

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

Result:
case mk.mk.mk.mk.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ : α
h₂ : (a₂, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
h : a₁ * c₁ = a₂ * c₁ ∧ a₁ * b₁ = a₂ * b₁
⊢ (a₁, b₁, c₁) = (a₂, b₁, c₁)

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)) = #(univ ×ˢ t ×ˢ t)

Tactic:
rw [← card_image_of_injOn this]

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)) = #(image f (univ ×ˢ t ×ˢ t))

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
h : (a.2.1 ∈ t ∧ a.2.2 ∈ t) ∧ a.1.1 * a.2.1 = a.1.2 * a.2.2
⊢ f (a.1.1 * a.2.2⁻¹, a.2.1, a.2.2) = a

Tactic:
simp [f, mul_right_comm, h.2]

Result:
no goals

Proof state:
case mk.mk.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : f (a₁, b₁, c₁) = f (a₂, b₂, c₂)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)

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

Result:
case mk.mk.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : (a₁ * c₁ = a₂ * c₂ ∧ a₁ * b₁ = a₂ * b₂) ∧ b₁ = b₂ ∧ c₁ = c₂
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)) = #(univ ×ˢ t ×ˢ t)

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]

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)) = #(univ ×ˢ t ×ˢ t)

Proof state:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)) = #(univ ×ˢ t ×ˢ t)

Tactic:
let f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)

Result:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
⊢ #(filter (fun x => x.1.1 * x.2.1 = x.1.2 * x.2.2) (univ ×ˢ t ×ˢ t)) = #(univ ×ˢ t ×ˢ t)