Remove some spoilers in IMO problems

Compfiles/Imo2003P5.lean

@@ -201,17 +201,16 @@ problem imo2003_p5 (n : ℕ) (hn : 2 < n) (x : ℕ → ℝ) (hx : MonotoneOn x (
         exact sum_congr rfl fun i _ => sum_congr rfl fun j _ => by
           rw [yeq i, yeq j]; congr 1; ring
 
-/-- The equality case: equality holds iff the sequence is an arithmetic progression.
-
-For the forward direction, with `y i = x i - m` (so `∑ y = 0`) the equality rewrites as
-`(∑ cᵢ yᵢ)² = (∑ cᵢ²)(∑ yᵢ²)` with `cᵢ = 2i + 1 - n`, i.e. equality in Cauchy-Schwarz.
-With `t = (∑ cᵢ yᵢ)/(∑ cᵢ²)` we get `∑ (t cᵢ - yᵢ)² = 0`, hence `yᵢ = t cᵢ` for all `i`,
-which says exactly that the `xᵢ` form an arithmetic progression. -/
+/-- The equality case: equality holds iff the sequence is an arithmetic progression. -/
 problem imo2003_p5_equality (n : ℕ) (hn : 2 < n) (x : ℕ → ℝ) (hx : MonotoneOn x (range n)) :
     (∑ i ∈ range n, ∑ j ∈ range n, |x i - x j|) ^ 2 =
       2 / 3 * ((n : ℝ) ^ 2 - 1) * ∑ i ∈ range n, ∑ j ∈ range n, (x i - x j) ^ 2 ↔
     ∃ a d : ℝ, ∀ i ∈ range n, x i = a + d * (i : ℝ) := by
   constructor
+    /- For the forward direction, with `y i = x i - m` (so `∑ y = 0`) the equality rewrites as
+    `(∑ cᵢ yᵢ)² = (∑ cᵢ²)(∑ yᵢ²)` with `cᵢ = 2i + 1 - n`, i.e. equality in Cauchy-Schwarz.
+    With `t = (∑ cᵢ yᵢ)/(∑ cᵢ²)` we get `∑ (t cᵢ - yᵢ)² = 0`, hence `yᵢ = t cᵢ` for all `i`,
+    which says exactly that the `xᵢ` form an arithmetic progression. -/
   · intro heq
     have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by lia)
     set S : ℝ := ∑ i ∈ range n, x i with hS

Compfiles/Imo2004P3.lean

@@ -48,6 +48,14 @@ def hookShapes : Finset (Finset (ℤ × ℤ)) :=
 /-- A hook is a translate of one of the eight orientations. -/
 def IsHook (s : Finset (ℤ × ℤ)) : Prop := ∃ σ ∈ hookShapes, ∃ t, s = σ.image (· + t)
 
+/-- `R` can be tiled by hooks: there is a finite family of pairwise
+disjoint hooks whose union is `R`. -/
+def Tileable (R : Finset (ℤ × ℤ)) : Prop :=
+  ∃ 𝒯 : Finset (Finset (ℤ × ℤ)), (∀ H ∈ 𝒯, IsHook H) ∧
+    (∀ H₁ ∈ 𝒯, ∀ H₂ ∈ 𝒯, H₁ ≠ H₂ → Disjoint H₁ H₂) ∧ R = 𝒯.biUnion id
+
+snip begin
+
 /-- The six orientations of the two-hook "tiles" (pairs of interlocking
 hooks): the `3 × 4` rectangle, the `4 × 3` rectangle, and the four
 orientations of the zigzag shape. -/
@@ -62,14 +70,6 @@ def tileShapes : Finset (Finset (ℤ × ℤ)) :=
 /-- A tile is a translate of one of the six tile shapes. -/
 def IsTile (s : Finset (ℤ × ℤ)) : Prop := ∃ τ ∈ tileShapes, ∃ t, s = τ.image (· + t)
 
-/-- `R` can be tiled by hooks: there is a finite family of pairwise
-disjoint hooks whose union is `R`. -/
-def Tileable (R : Finset (ℤ × ℤ)) : Prop :=
-  ∃ 𝒯 : Finset (Finset (ℤ × ℤ)), (∀ H ∈ 𝒯, IsHook H) ∧
-    (∀ H₁ ∈ 𝒯, ∀ H₂ ∈ 𝒯, H₁ ≠ H₂ → Disjoint H₁ H₂) ∧ R = 𝒯.biUnion id
-
-snip begin
-
 /-- The lower-left corner of the bounding box of a set of cells. -/
 def lo (s : Finset (ℤ × ℤ)) : ℤ × ℤ :=
   (((s.image Prod.fst).min).getD 0, ((s.image Prod.snd).min).getD 0)
@@ -1156,14 +1156,12 @@ lemma not_tileable_5 (n : ℕ) (hn : 0 < n) : ¬ Tileable (rect 5 n) := by
     exact ⟨hm.1, hm.2.1, hm.2.2.1, by lia⟩
   exact corner_check τ hτ h00T τ' hτ'' v hv_mem hbounds hdisj
 
-snip end
-
 /-- The predicate characterising the rectangles that can be tiled by hooks. -/
 def GoodRect (m n : ℕ) : Prop :=
   m ≠ 1 ∧ m ≠ 2 ∧ m ≠ 5 ∧ n ≠ 1 ∧ n ≠ 2 ∧ n ≠ 5 ∧ (3 ∣ m ∨ 3 ∣ n) ∧ (4 ∣ m ∨ 4 ∣ n)
 
-/-- The answer: exactly the rectangles with `{1, 2, 5} ∩ {m, n} = ∅`,
-`3 ∣ mn` (i.e. `3 ∣ m` or `3 ∣ n`) and `4 ∣ mn` (i.e. `4 ∣ m` or `4 ∣ n`). -/
+snip end
+
 determine answer : Set (ℕ × ℕ) :=
   {p | GoodRect p.1 p.2}
 

Compfiles/Imo2017P3.lean

@@ -1043,7 +1043,7 @@ end
 snip end
 
 /-- The answer to the question "can the hunter always ensure that the distance
-between her and the rabbit becomes at most 100?" is no. -/
+between her and the rabbit becomes at most 100?" -/
 determine does_exist : Bool := false
 
 problem imo2017_p3 :

Compfiles/Imo2018P4.lean

@@ -40,8 +40,6 @@ K such that Amy can ensure that she places at least K stones.
   occupies two new sites, so `CanEnsure K 400 ∅ ∅` (with fuel exceeding
   any possible length of play) is the exact game-theoretic meaning of
   "Amy can ensure at least `K` stones", abbreviated `AmyEnsures K`.
-
-The answer is `K = 100`.
 -/
 
 namespace Imo2018P4

Compfiles/Imo2019P5.lean

@@ -65,6 +65,8 @@ coin from the left; otherwise (all coins show tails) do nothing. -/
 def step {n : ℕ} (c : Fin n → Bool) : Fin n → Bool :=
   if h : numHeads c = 0 then c else Function.update c (flipIx c h) (!c (flipIx c h))
 
+snip begin
+
 /-- The sum of the 1-based positions of the coins showing heads. -/
 def weightedSum {n : ℕ} (c : Fin n → Bool) : ℕ :=
   ∑ i : Fin n, (i.val + 1) * (if c i then 1 else 0)
@@ -76,9 +78,11 @@ step (see `step_meas`), hence it equals the number of steps the process takes. -
 def meas {n : ℕ} (c : Fin n → Bool) : ℤ :=
   2 * (weightedSum c : ℤ) - (numHeads c : ℤ) ^ 2
 
+snip end
+
 /-- The number of steps that Harry's process takes starting from
 configuration `c`. -/
-def L {n : ℕ} (c : Fin n → Bool) : ℕ := (meas c).toNat
+determine L {n : ℕ} (c : Fin n → Bool) : ℕ := (meas c).toNat
 
 snip begin
 
@@ -589,6 +593,18 @@ problem imo2019_p5_parta (n : ℕ) (c : Fin n → Bool) :
     ∃ m : ℕ, step^[m] c = fun _ ↦ false :=
   ⟨L c, iterate_L c⟩
 
+/-- Part (b): The number of steps that Harry's process takes starting from
+configuration `c` is L -/
+problem imo2019_p5_partb_definition (n : ℕ) (c : Fin n → Bool) :
+    IsLeast {m : ℕ| step^[m] c = fun _ ↦ false} (L c) := by
+  simp [IsLeast]
+  constructor
+  · exact iterate_L c
+  · rw [mem_lowerBounds]
+    intro a ha
+    contrapose! ha
+    exact not_iterate_lt_L _ ha
+
 /-- Part (b): the average number of steps over all `2 ^ n` configurations is
 `n * (n + 1) / 4`. -/
 problem imo2019_p5_partb (n : ℕ) (hn : 0 < n) :

Compfiles/Imo2026P1.lean

@@ -75,6 +75,8 @@ def HasUniqueLarge (B : Board) : Prop :=
 terminal board `B'` is precisely a witness of `Reachable B B'` with `IsTerminal B'`. -/
 def Reachable (B B' : Board) : Prop := Relation.ReflTransGen Move B B'
 
+snip begin
+
 /-- The exponent `g_p` for a prime `p` and board `B`: the `gcd` of the `p`-adic
 valuations of the entries of `B`.  Since `gcd(a, 0) = a`, valuations equal to `0`
 (entries not divisible by `p`) do not affect this gcd, so `gExp p B` is the gcd of
@@ -88,8 +90,6 @@ of `B` of `p` raised to the gcd of the `p`-adic valuations. -/
 noncomputable def Mval (B : Board) : ℕ :=
   ∏ p ∈ B.prod.primeFactors, p ^ gExp p B
 
-snip begin
-
 /-!
 ### Proof sketch
 
@@ -491,53 +491,4 @@ problem imo2026_p1b_invariance (B₀ : Board) (hB₀ : IsInitial B₀)
     have hMv := large_mem_eq_Mval hB₀ h₂ t₂ hM hMem
     exact ⟨hM, (hMv.trans hx₁val.symm) ▸ hx₁mem⟩
 
-/-- **Value of `M` (correctness of the explicit formula).**  For any terminal board
-`B'` reachable from an initial board `B₀`, the unique entry `M > 1` of `B'` equals
-the invariant `Mval B₀`. -/
-problem imo2026_p1_terminal_value (B₀ : Board) (hB₀ : IsInitial B₀)
-    (B' : Board) (hreach : Reachable B₀ B') (hterm : IsTerminal B')
-    (M : ℕ) (hM : 1 < M) (hMem : M ∈ B') :
-    M = Mval B₀ :=
-  large_mem_eq_Mval hB₀ hreach hterm hM hMem
-
-/-- The invariant terminal value is itself `> 1`, since all initial entries exceed
-`1`. -/
-problem imo2026_p1_mval_gt_one (B₀ : Board) (hB₀ : IsInitial B₀) : 1 < Mval B₀ := by
-  have hge2 : ∀ a ∈ B₀, 2 ≤ a := hB₀.2
-  have hcard : B₀.card = 2026 := hB₀.1
-  have hB₀ne : B₀ ≠ 0 := by
-    intro hz
-    rw [hz, Multiset.card_zero] at hcard
-    exact absurd hcard (by decide)
-  obtain ⟨a, ha⟩ := Multiset.exists_mem_of_ne_zero hB₀ne
-  have ha2 : 2 ≤ a := hge2 a ha
-  obtain ⟨p, hpp, hpdvd⟩ := Nat.exists_prime_and_dvd (n := a) (by lia)
-  have hproddvd : a ∣ B₀.prod := Multiset.dvd_prod ha
-  have hpd : p ∣ B₀.prod := hpdvd.trans hproddvd
-  have hp0 : B₀.prod ≠ 0 := by
-    rw [Ne, Multiset.prod_eq_zero_iff]
-    intro h0
-    have := hge2 0 h0
-    lia
-  have hpmem : p ∈ B₀.prod.primeFactors := Nat.mem_primeFactors.mpr ⟨hpp, hpd, hp0⟩
-  have : Fact p.Prime := ⟨hpp⟩
-  have hva : 1 ≤ padicValNat p a := one_le_padicValNat_of_dvd (by lia) hpdvd
-  have hgexp : 1 ≤ gExp p B₀ := by
-    have hmem : padicValNat p a ∈ B₀.map (fun a => padicValNat p a) :=
-      Multiset.mem_map.mpr ⟨a, ha, rfl⟩
-    have hne : (B₀.map fun a => padicValNat p a).gcd ≠ 0 := by
-      intro hz0
-      rw [Multiset.gcd_eq_zero_iff] at hz0
-      exact (show padicValNat p a ≠ 0 by lia) (hz0 _ hmem)
-    exact Nat.one_le_iff_ne_zero.mpr hne
-  have hpow : p ≤ p ^ gExp p B₀ := by
-    conv_lhs => rw [← pow_one p]
-    exact Nat.pow_le_pow_right hpp.one_lt.le hgexp
-  have hp2 : 1 < p := hpp.one_lt
-  have hbig : 1 < p ^ gExp p B₀ := lt_of_lt_of_le hp2 hpow
-  unfold Mval
-  exact lt_of_lt_of_le hbig
-    (Finset.single_le_prod
-      (fun q hq => Nat.one_le_pow (gExp q B₀) q (Nat.prime_of_mem_primeFactors hq).pos) hpmem)
-
 end Imo2026P1

Compfiles/Imo2026P6.lean

@@ -46,10 +46,10 @@ def IsValidSeq (a : ℕ → ℕ) : Prop :=
         (∀ b, a n < b → b < a (n + 1) → ∃ i ≤ n, Nat.gcd b (a i) = 1))
 
 /-- For any sequence satisfying Definition 1, there exist positive integers `T` and `L` such that
-`a (n + T) = a n + L` for every `n`. Equivalently, the sequence of consecutive differences is
-purely periodic. -/
+`a (n + T) = a n + L` for every `n`.  -/
 problem imo2026_p6 (a : ℕ → ℕ) (ha : IsValidSeq a) :
     ∃ T L : ℕ, 0 < T ∧ 0 < L ∧ ∀ n, a (n + T) = a n + L := by
+  -- Equivalently, the sequence of consecutive differences is purely periodic .
   -- Any later term shares a common factor with every earlier term.
   have hgcd : ∀ i j : ℕ, i < j → 1 < Nat.gcd (a j) (a i) := by
     intro i j hij