chore(archive/imo): fix some naming inconsistencies and whitespace (#19155)

adomani · adomani · commit 308826471968 · 2023-06-05T02:20:49.000Z
I realize that this is the third PR concerning namespacing the files in `archive/imo`.  These are some simple inconsistencies in naming.  There is no rush in merging this PR, but in the long run it might help to have consistent namespacing, so that batch renames can be simpler.
diff --git a/archive/imo/imo1975_q1.lean b/archive/imo/imo1975_q1.lean
@@ -31,9 +31,7 @@ variables (hx : antitone_on x (finset.Icc 1 n))
 variables (hy : antitone_on y (finset.Icc 1 n))
 include hx hy hσ
 
-namespace imo1975_q1
-
-theorem IMO_1975_Q1 :
+theorem imo1975_q1 :
   ∑ i in finset.Icc 1 n, (x i - y i) ^ 2 ≤ ∑ i in finset.Icc 1 n, (x i - y (σ i)) ^ 2 :=
 begin
   simp only [sub_sq, finset.sum_add_distrib, finset.sum_sub_distrib],
@@ -48,5 +46,3 @@ begin
   -- them being `decreasing`
   exact antitone_on.monovary_on hx hy
 end
-
-end imo1975_q1
diff --git a/archive/imo/imo1977_q6.lean b/archive/imo/imo1977_q6.lean
@@ -36,6 +36,7 @@ begin
 end
 
 end imo1977_q6
+
 open imo1977_q6
 
 theorem imo1977_q6 (f : ℕ+ → ℕ+) (h : ∀ n, f (f n) < f (n + 1)) :
diff --git a/archive/imo/imo1988_q6.lean b/archive/imo/imo1988_q6.lean
@@ -186,6 +186,7 @@ begin
 end
 
 end imo1988_q6
+
 open imo1988_q6
 
 /--Question 6 of IMO1988. If a and b are two natural numbers
diff --git a/archive/imo/imo1994_q1.lean b/archive/imo/imo1994_q1.lean
@@ -46,6 +46,7 @@ begin
 end
 
 end imo1994_q1
+
 open imo1994_q1
 
 theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : finset ℕ) (hm : A.card = m + 1)
diff --git a/archive/imo/imo1998_q2.lean b/archive/imo/imo1998_q2.lean
@@ -198,6 +198,7 @@ lemma clear_denominators {a b k : ℕ} (ha : 0 < a) (hb : 0 < b) :
 by rw div_le_div_iff; norm_cast; simp [ha, hb]
 
 end imo1998_q2
+
 open imo1998_q2
 
 theorem imo1998_q2 [fintype J] [fintype C]
diff --git a/archive/imo/imo2001_q2.lean b/archive/imo/imo2001_q2.lean
@@ -67,6 +67,7 @@ calc _ ≥ _ : add_le_add (add_le_add (bound ha hb hc) (bound hb hc ha)) (bound
    ... = 1 : by rw [h₁, h₂, ← add_div, ← add_div, div_self $ ne_of_gt $ denom_pos ha hb hc]
 
 end imo2001_q2
+
 open imo2001_q2
 
 theorem imo2001_q2 (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
diff --git a/archive/imo/imo2005_q3.lean b/archive/imo/imo2005_q3.lean
@@ -45,6 +45,7 @@ begin
 end
 
 end imo2005_q3
+
 open imo2005_q3
 
 theorem imo2005_q3 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x*y*z ≥ 1) :
diff --git a/archive/imo/imo2005_q4.lean b/archive/imo/imo2005_q4.lean
@@ -55,8 +55,12 @@ begin
   ... = 0 : by ring,
 end
 
+end imo2005_q4
+
+open imo2005_q4
+
 /-- Main statement:  The only positive integer coprime to all terms of the sequence `a` is `1`. -/
-example {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → is_coprime (a n) k) ↔ k = 1 :=
+theorem imo2005_q4 {k : ℕ} (hk : 0 < k) : (∀ n : ℕ, 1 ≤ n → is_coprime (a n) k) ↔ k = 1 :=
 begin
   split, rotate,
   { -- The property is clearly true for `k = 1`
@@ -95,5 +99,3 @@ begin
   -- Contradiction!
   contradiction,
 end
-
-end imo2005_q4
diff --git a/archive/imo/imo2006_q3.lean b/archive/imo/imo2006_q3.lean
@@ -136,6 +136,7 @@ begin
 end
 
 end imo2006_q3
+
 open imo2006_q3
 
 theorem imo2006_q3 (M : ℝ) :
diff --git a/archive/imo/imo2006_q5.lean b/archive/imo/imo2006_q5.lean
@@ -201,6 +201,7 @@ begin
 end
 
 end imo2006_q5
+
 open imo2006_q5
 
 /-- The general problem follows easily from the k = 2 case. -/
diff --git a/archive/imo/imo2008_q3.lean b/archive/imo/imo2008_q3.lean
@@ -80,6 +80,7 @@ begin
 end
 
 end imo2008_q3
+
 open imo2008_q3
 
 theorem imo2008_q3 : ∀ N : ℕ, ∃ n : ℕ, n ≥ N ∧
diff --git a/archive/imo/imo2008_q4.lean b/archive/imo/imo2008_q4.lean
@@ -30,6 +30,7 @@ by rw [← pow_left_inj (abs_nonneg x) zero_le_one (pos_iff_ne_zero.2 hn), one_p
   abs_one]
 
 end imo2008_q4
+
 open imo2008_q4
 
 theorem imo2008_q4
diff --git a/archive/imo/imo2013_q1.lean b/archive/imo/imo2013_q1.lean
@@ -46,6 +46,7 @@ begin
 end
 
 end imo2013_q1
+
 open imo2013_q1
 
 theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
diff --git a/archive/imo/imo2013_q5.lean b/archive/imo/imo2013_q5.lean
@@ -199,6 +199,7 @@ begin
 end
 
 end imo2013_q5
+
 open imo2013_q5
 
 theorem imo2013_q5
diff --git a/archive/imo/imo2019_q1.lean b/archive/imo/imo2019_q1.lean
@@ -19,9 +19,7 @@ Note that there is a much more compact proof of this fact in Isabelle/HOL
   - http://downthetypehole.de/paste/4YbGgqb4
 -/
 
-namespace imo2019_q1
-
-theorem imo2019Q1 (f : ℤ → ℤ) :
+theorem imo2019_q1 (f : ℤ → ℤ) :
   (∀ a b : ℤ, f (2 * a) + 2 * (f b) = f (f (a + b))) ↔
     (f = 0) ∨ ∃ c, f = λ x, 2 * x + c :=
 begin
@@ -51,5 +49,3 @@ begin
   { right, use c, ext b, simp [H, add_comm] },
   { left, ext b, simpa [H, two_ne_zero] using H3 }
 end
-
-end imo2019_q1
diff --git a/archive/imo/imo2019_q2.lean b/archive/imo/imo2019_q2.lean
@@ -583,6 +583,7 @@ end
 end imo2019q2_cfg
 
 end imo2019_q2
+
 open imo2019_q2
 
 theorem imo2019_q2 (A B C A₁ B₁ P Q P₁ Q₁ : Pt)
diff --git a/archive/imo/imo2019_q4.lean b/archive/imo/imo2019_q4.lean
@@ -28,7 +28,7 @@ open finset multiplicity nat (hiding zero_le prime)
 
 namespace imo2019_q4
 
-theorem imo2019_q4_upper_bound {k n : ℕ} (hk : k > 0)
+theorem upper_bound {k n : ℕ} (hk : k > 0)
   (h : (k! : ℤ) = ∏ i in range n, (2 ^ n - 2 ^ i)) : n < 6 :=
 begin
   have prime_2 : prime (2 : ℤ),
@@ -70,7 +70,6 @@ begin
 end
 
 end imo2019_q4
-open imo2019_q4
 
 theorem imo2019_q4 {k n : ℕ} (hk : k > 0) (hn : n > 0) :
   (k! : ℤ) = (∏ i in range n, (2 ^ n - 2 ^ i)) ↔ (k, n) = (1, 1) ∨ (k, n) = (3, 2) :=
@@ -81,7 +80,7 @@ begin
     norm_num [prod_range_succ, succ_mul] },
   intro h,
   /- We know that n < 6. -/
-  have := imo2019_q4_upper_bound hk h,
+  have := imo2019_q4.upper_bound hk h,
   interval_cases n,
   /- n = 1 -/
   { left, congr, norm_num at h, rw [factorial_eq_one] at h, apply antisymm h,
diff --git a/archive/imo/imo2021_q1.lean b/archive/imo/imo2021_q1.lean
@@ -152,7 +152,11 @@ begin
     rintros d (rfl|rfl|rfl); split; linarith only [hna, hab, hbc, hcn], },
 end
 
-theorem IMO_2021_Q1 : ∀ (n : ℕ), 100 ≤ n → ∀ (A ⊆ finset.Icc n (2 * n)),
+end imo2021_q1
+
+open imo2021_q1
+
+theorem imo2021_q1 : ∀ (n : ℕ), 100 ≤ n → ∀ (A ⊆ finset.Icc n (2 * n)),
   (∃ (a b ∈ A), a ≠ b ∧ ∃ (k : ℕ), a + b = k * k) ∨
   (∃ (a b ∈ finset.Icc n (2 * n) \ A), a ≠ b ∧ ∃ (k : ℕ), a + b = k * k) :=
 begin
@@ -180,5 +184,3 @@ begin
   cases hCA; [right, left];
   exact ⟨a, (hCA ha).2, b, (hCA hb).2, hab, h₁ a (hCA ha).1 b (hCA hb).1 hab⟩,
 end
-
-end imo2021_q1
