From 8b3ee67cf8d06c409ee77329e9a3cf1fc01157dc Mon Sep 17 00:00:00 2001
From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com>
Date: Sun, 28 Jul 2024 14:07:11 -0700
Subject: [PATCH 1/3] [Usa1979P1] Add proof

---
 Compfiles/Usa1979P1.lean | 50 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 Compfiles/Usa1979P1.lean

diff --git a/Compfiles/Usa1979P1.lean b/Compfiles/Usa1979P1.lean
new file mode 100644
index 00000000..e8811ef7
--- /dev/null
+++ b/Compfiles/Usa1979P1.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2024 The Compfiles Contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Hongyu Ouyang
+-/
+
+import Mathlib.Tactic
+
+import ProblemExtraction
+
+problem_file { tags := [.Algebra, .Inequality] }
+
+/-!
+# USA Mathematical Olympiad 1979, Problem 1
+
+Determine all non-negative integral solutions (n₁, n₂, ..., n₁₄) if any,
+apart from permutations, of the Diophantine Equation $n₁⁴ + n₂⁴ + ... + n₁₄⁴ = 1599.
+-/
+
+namespace Usa1979P1
+
+structure Perm14 where
+  s : Multiset ℕ
+  p : Multiset.card s = 14
+
+set_option diagnostics true in
+determine SolutionSet : Set Perm14 := ∅
+
+problem usa1979_p1 : ∀ e, e ∈ SolutionSet ↔ (e.s.map (fun x ↦ x ^ 4)).sum = 1599 := by
+  -- solution from
+  -- https://artofproblemsolving.com/wiki/index.php/1979_USAMO_Problems/Problem_1
+  unfold SolutionSet
+  intro e
+  constructor
+  · simp only [Set.mem_empty_iff_false, false_implies]
+  · intro contra
+    apply_fun (· % 16) at contra
+    rw [Multiset.sum_nat_mod, Multiset.map_map] at contra
+    simp only [Function.comp_apply, Nat.reduceMod] at contra
+    suffices : (Multiset.map (fun x ↦ x ^ 4 % 16) e.s).sum ≤ 14; omega
+    rw [show 14 = Multiset.card (e.s.map (fun x ↦ x ^ 4 % 16)) * 1 by rw [Multiset.card_map, e.p]]
+    apply Multiset.sum_le_card_nsmul
+    intro x
+    rw [Multiset.mem_map]
+    intro ⟨i, ⟨_, h⟩⟩
+    rw [← h, Nat.pow_mod]
+    mod_cases i % 16
+    all_goals rw [H]; try norm_num
+
+end Usa1979P1

From 424912ff140c8fc62adfcb018c6a95230c24d638 Mon Sep 17 00:00:00 2001
From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com>
Date: Sun, 28 Jul 2024 14:13:08 -0700
Subject: [PATCH 2/3] Update Compfiles

---
 Compfiles.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Compfiles.lean b/Compfiles.lean
index f13eddbf..15816858 100644
--- a/Compfiles.lean
+++ b/Compfiles.lean
@@ -158,6 +158,7 @@ import Compfiles.UK2024R1P2
 import Compfiles.UpperLowerContinuous
 import Compfiles.Usa1974P2
 import Compfiles.Usa1978P1
+import Compfiles.Usa1979P1
 import Compfiles.Usa1980P5
 import Compfiles.Usa1981P5
 import Compfiles.Usa1982P4

From fdf7c92425b590dbceb0330ac6ac3cc3338cd351 Mon Sep 17 00:00:00 2001
From: Hongyu Ouyang <96765450+casavaca@users.noreply.github.com>
Date: Sun, 28 Jul 2024 16:53:01 -0700
Subject: [PATCH 3/3] Clean up and rename

---
 Compfiles/Usa1979P1.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Compfiles/Usa1979P1.lean b/Compfiles/Usa1979P1.lean
index e8811ef7..6303052d 100644
--- a/Compfiles/Usa1979P1.lean
+++ b/Compfiles/Usa1979P1.lean
@@ -13,18 +13,18 @@ problem_file { tags := [.Algebra, .Inequality] }
 /-!
 # USA Mathematical Olympiad 1979, Problem 1
 
-Determine all non-negative integral solutions (n₁, n₂, ..., n₁₄) if any,
-apart from permutations, of the Diophantine Equation $n₁⁴ + n₂⁴ + ... + n₁₄⁴ = 1599.
+Determine all non-negative integral solutions $(n_1,n_2,\dots , n_{14})$ if any,
+apart from permutations, of the Diophantine Equation $n_1^4+n_2^4+\cdots +n_{14}^4=1599$.
 -/
 
 namespace Usa1979P1
 
-structure Perm14 where
+structure MultisetNatOfLen14 where
   s : Multiset ℕ
   p : Multiset.card s = 14
 
 set_option diagnostics true in
-determine SolutionSet : Set Perm14 := ∅
+determine SolutionSet : Set MultisetNatOfLen14 := ∅
 
 problem usa1979_p1 : ∀ e, e ∈ SolutionSet ↔ (e.s.map (fun x ↦ x ^ 4)).sum = 1599 := by
   -- solution from