English
Similarly, if the right argument is universal, E_m[s, univ] = |α| · |s|^2.
Русский
Аналогично, если правый аргумент энергии — универ, то E_m[s, univ] = |α| · |s|^2.
LaTeX
$$E_m[s, univ] = |α| · |s|^2$$
Lean4
@[to_additive (attr := simp)]
theorem mulEnergy_univ_left : Eₘ[univ, t] = Fintype.card α * t.card ^ 2 :=
by
simp only [mulEnergy, univ_product_univ, Fintype.card, sq, ← card_product]
let f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
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]
rw [← card_image_of_injOn this]
congr with a
simp only [mem_filter, mem_product, mem_univ, true_and, mem_image, Prod.exists]
refine ⟨fun h => ⟨a.1.1 * a.2.2⁻¹, _, _, h.1, by simp [f, mul_right_comm, h.2]⟩, ?_⟩
rintro ⟨b, c, d, hcd, rfl⟩
simpa [f, mul_right_comm]
