problem extraction via pseudo-attributes

MathPuzzles/Bulgaria1998Q1.lean

@@ -10,7 +10,7 @@ import Mathlib.Tactic.IntervalCases
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 Bulgarian Mathematical Olympiad 1998, Problem 1
 
 Find the least natural number n (n ≥ 3) with the following property:
@@ -19,16 +19,16 @@ there exist three points Aᵢ, Aⱼ, A₂ⱼ₋ᵢ, 1 ≤ i < 2j - i ≤ n, whic
 the same color.
 -/
 
-namespace Bulgaria1998Q1
+#[problem_setup] namespace Bulgaria1998Q1
 
-@[problem_setup]
+#[problem_setup]
 def coloring_has_desired_points (m : ℕ) (color : Set.Icc 1 m → Fin 2) : Prop :=
   ∃ i j : Set.Icc 1 m,
     i < j ∧
     ∃ h3 : 2 * j.val - i ∈ Set.Icc 1 m,
     color i = color j ∧ color i = color ⟨2 * j - i, h3⟩
 
-@[solution_data]
+#[solution_data]
 def n := 9
 
 def coloring_of_eight : Set.Icc 1 8 → Fin 2
@@ -42,7 +42,7 @@ def coloring_of_eight : Set.Icc 1 8 → Fin 2
 | ⟨8, _⟩ => 0
 | _ => 0 -- unreachable
 
-@[problem_statement]
+#[problem_statement]
 theorem bulgaria1998_q1a :
     ∃ f: Set.Icc 1 (n - 1) → Fin 2, ¬coloring_has_desired_points (n - 1) f := by
   use coloring_of_eight
@@ -53,7 +53,6 @@ theorem bulgaria1998_q1a :
   dsimp[coloring_of_eight] at *
   interval_cases i <;> interval_cases j <;> aesop
 
-@[problem_statement]
+#[problem_statement]
 theorem bulgaria1998_q1b (color : Set.Icc 1 n → Fin 2) : coloring_has_desired_points n f := by
   sorry
-

MathPuzzles/Bulgaria1998Q11.lean

@@ -12,7 +12,7 @@ import Mathlib.Tactic.Zify
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 Bulgarian Mathematical Olympiad 1998, Problem 11
 
 Let m,n be natural numbers such that
@@ -22,7 +22,7 @@ Let m,n be natural numbers such that
 is an integer. Prove that A is odd.
 -/
 
-namespace Bulgaria1998Q11
+#[problem_setup] namespace Bulgaria1998Q11
 
 lemma mod_plus_pow (m n : ℕ) : (m + 3)^n % 3 = m^n % 3 := by
   induction' n with pn hpn
@@ -39,7 +39,7 @@ lemma foo1 (m n : ℕ) (ho : Odd m) : (m + 3) ^ n.succ % 2 = 0 := by
   rw[hw, Nat.pow_succ, show 2 * w + 1 + 3 = 2 * (w + 2) by ring, Nat.mul_mod,
      Nat.mul_mod_right, mul_zero, Nat.zero_mod]
 
-@[problem_statement]
+#[problem_statement]
 theorem bulgaria1998_q11
     (m n A : ℕ)
     (h : 3 * m * A = (m + 3)^n + 1) : Odd A := by

MathPuzzles/Bulgaria1998Q2.lean

@@ -11,21 +11,20 @@ import Mathlib.Geometry.Euclidean.Triangle
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 Bulgarian Mathematical Olympiad 1998, Problem 2
 
 A convex quadrilateral ABCD has AD = CD and ∠DAB = ∠ABC < 90°.
 The line through D and the midpoint of BC intersects line AB
 in point E. Prove that ∠BEC = ∠DAC. (Note: The problem is valid
 without the assumption ∠ABC < 90°.)
-
 -/
 
 namespace Bulgaria1998Q2
 
 open EuclideanGeometry
 
-@[problem_statement]
+#[problem_statement]
 theorem bulgaria1998_q2
     (A B C D E M: EuclideanSpace ℝ (Fin 2))
     (H1 : dist D A = dist D C)

MathPuzzles/Bulgaria1998Q3.lean

@@ -11,7 +11,7 @@ import Mathlib.Analysis.SpecificLimits.Basic
 
 import MathPuzzles.Meta.Attributes
 
-/-
+#[problem_setup]/-!
 Bulgarian Mathematical Olympiad 1998, Problem 3
 
 Let ℝ⁺ be the set of positive real numbers. Prove that there does not exist a function
@@ -23,7 +23,8 @@ for every x,y ∈ ℝ⁺.
 
 -/
 
-namespace Bulgaria1998Q3
+#[problem_setup] namespace Bulgaria1998Q3
+
 open BigOperators
 
 lemma geom_sum_bound (n : ℕ) : ∑ i in Finset.range n, (1:ℝ) / (2^i) < 3 :=
@@ -32,7 +33,7 @@ lemma geom_sum_bound (n : ℕ) : ∑ i in Finset.range n, (1:ℝ) / (2^i) < 3 :=
         _ ≤ 2 := sum_geometric_two_le n
         _ < 3 := by norm_num
 
-@[problem_statement]
+#[problem_statement]
 theorem bulgaria1998_q3
     (f : ℝ → ℝ)
     (hpos : ∀ x : ℝ, 0 < x → 0 < f x)

MathPuzzles/Bulgaria1998Q6.lean

@@ -12,7 +12,7 @@ import Mathlib.Tactic.Ring
 
 import MathPuzzles.Meta.Attributes
 
-/-
+#[problem_setup]/-
 Bulgarian Mathematical Olympiad 1998, Problem 6
 
 Prove that the equation
@@ -23,7 +23,7 @@ has no solutions in positive integers.
 
 -/
 
-namespace Bulgaria1998Q6
+#[problem_setup] namespace Bulgaria1998Q6
 
 lemma lemma_0
     (a b c x : ℤ)
@@ -63,7 +63,7 @@ lemma lemma_1
   rw [←hs'] at h
   sorry
 
-@[problem_statement]
+#[problem_statement]
 theorem bulgaria1998_q6
     (x y z : ℤ)
     (hx : 0 < x)

MathPuzzles/Bulgaria1998Q8.lean

@@ -10,18 +10,18 @@ import Mathlib.Tactic.Ring
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 Bulgarian Mathematical Olympiad 1998, Problem 8
 The polynomials Pₙ(x,y) for n = 1, 2, ... are defined by P₁(x,y) = 1 and
   Pₙ₊₁(x,y) = (x + y - 1)(y + 1)Pₙ(x,y+2) + (y - y²)Pₙ(x,y)
 Prove that Pₙ(x,y) = Pₙ(y,x) for all x,y,n.
 -/
 
-namespace Bulgaria1998Q8
+#[problem_setup] namespace Bulgaria1998Q8
 
-variable {R : Type} [CommRing R]
+#[problem_setup] variable {R : Type} [CommRing R]
 
-@[problem_setup]
+#[problem_setup]
 def P : ℕ → R → R → R
 | 0, _, _ => 1
 | n+1, x, y => (x + y - 1) * (y + 1) * P n x (y + 2) + (y - y^2) * P n x y
@@ -46,7 +46,7 @@ def U : ℕ → R → R → R
 | n, x, y => (x + y - 1) *((y + 1)*(x - x^2) * P n (y + 2) x
                            + (x + 1) * (y - y^2) * P n y (x + 2))
 
-@[problem_statement]
+#[problem_statement]
 theorem bulgaria1998_q8 (n : ℕ) (x y : R) : P n x y = P n y x := by
   -- We induct on n. For n = 1,2 the result is evident.
   -- So we take n > 1 and suppose that the result is true for

MathPuzzles/Canada1998Q3.lean

@@ -14,19 +14,19 @@ import Mathlib.Tactic.Positivity
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 Canadian Mathematical Olympiad 1998, Problem 3
 
 Let n be a natural number such that n ≥ 2. Show that
 
   (1/(n + 1))(1 + 1/3 + ... + 1/(2n - 1)) > (1/n)(1/2 + 1/4 + ... + 1/2n).
 -/
 
-namespace Canada1998Q3
+#[problem_setup] namespace Canada1998Q3
 
-open BigOperators
+#[problem_setup] open BigOperators
 
-@[problem_statement]
+#[problem_statement]
 theorem canada1998_q3 (n : ℕ) (hn : 2 ≤ n) :
     (1/((n:ℝ) + 1)) * ∑ i in Finset.range n, (1/(2 * (i:ℝ) + 1)) >
     (1/(n:ℝ)) * ∑ i in Finset.range n, (1/(2 * (i:ℝ) + 2)) := by

MathPuzzles/Canada1998Q5.lean

@@ -8,7 +8,7 @@ import Mathlib.Data.Int.Basic
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 Canadian Mathematical Olympiad 1998, Problem 5
 
 Let m be a positive integer. Define the sequence {aₙ} by a₀ = 0,
@@ -20,15 +20,15 @@ a₁ = m, and aₙ₊₁ = m²aₙ - aₙ₋₁ for n ≥ 1. Prove that an order
 if an only if (a,b) = (aₙ,aₙ₊₁) for some n ≥ 0.
 -/
 
-namespace Canada1998Q5
+#[problem_setup] namespace Canada1998Q5
 
-@[problem_setup]
+#[problem_setup]
 def A (m : ℕ) (hm : 0 < m) : ℕ → ℤ
 | 0 => 0
 | 1 => (↑m)
 | n + 2 => (m : ℤ)^2 * A m hm (n + 1) - A m hm n
 
-@[problem_statement]
+#[problem_statement]
 theorem canada1998_q5 (m : ℕ) (hm : 0 < m) (a b : ℕ) (hab : a ≤ b) :
     a^2 + b^2 = m^2 * (a * b + 1) ↔
      ∃ n : ℕ, (a:ℤ) = A m hm n ∧ (b:ℤ) = A m hm (n + 1) := by

MathPuzzles/Hungary1998Q6.lean

@@ -13,16 +13,16 @@ import Mathlib.Tactic.Ring
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 Hungarian Mathematical Olympiad 1998, Problem 6
 
 Let x, y, z be integers with z > 1. Show that
 
  (x + 1)² + (x + 2)² + ... + (x + 99)² ≠ yᶻ.
 -/
 
-namespace Hungary1998Q6
-open BigOperators
+#[problem_setup] namespace Hungary1998Q6
+#[problem_setup] open BigOperators
 
 lemma sum_range_square_mul_six (n : ℕ) :
     (∑i in Finset.range n, (i+1)^2) * 6 = n * (n + 1) * (2*n + 1) := by
@@ -41,7 +41,7 @@ lemma cast_sum_square (n : ℕ) :
   ∑i in Finset.range n, ((i:ℤ)+1)^2 =
    (((∑i in Finset.range n, (i+1)^2):ℕ) :ℤ) := by norm_cast
 
-@[problem_statement]
+#[problem_statement]
 theorem hungary1998_q6 (x y : ℤ) (z : ℕ) (hz : 1 < z) :
     (∑ i in Finset.range 99, (x + i + 1)^2) ≠ y^z := by
   -- Suppose (x + 1)² + (x + 2)² + ... + (x + 99)² = yᶻ.

MathPuzzles/Imo1959Q1.lean

@@ -10,7 +10,7 @@ import Mathlib.Data.Nat.Prime
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 # IMO 1959 Q1
 Prove that the fraction `(21n+4)/(14n+3)` is irreducible for every
 natural number `n`.
@@ -30,7 +30,7 @@ lemma calculation
   have h5 : 3 * (14 * n + 3) = 2 * (21 * n + 4) + 1 := by ring
   exact (Nat.dvd_add_right h3).mp (h5 ▸ h4)
 
-@[problem_statement]
+#[problem_statement]
 theorem imo1959_q1 : ∀ n : ℕ, Nat.Coprime (21 * n + 4) (14 * n + 3) :=
 fun n => Nat.coprime_of_dvd' <| λ k _ h1 h2 => calculation n k h1 h2
 

MathPuzzles/Imo1964Q1B.lean

@@ -10,13 +10,13 @@ import Mathlib.Tactic.Linarith
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 # International Mathematical Olympiad 1964, Problem 1b
 
 Prove that there is no positive integer n for which 2ⁿ + 1 is divisible by 7.
 -/
 
-namespace Imo1964Q1
+#[problem_setup] namespace Imo1964Q1
 
 /-
 Informal proof (credit to twitch.tv viewer int_fast64_t):
@@ -26,7 +26,7 @@ Informal proof (credit to twitch.tv viewer int_fast64_t):
     2^n mod 7 = (2^3 mod 7)^k * 2^j mod 7 = 1 mod 7 * 2^j mod 7,
   but 2^j < 5
 -/
-@[problem_statement]
+#[problem_statement]
 theorem imo_1964_q1b (n : ℕ) : ¬ 7 ∣ (2^n + 1) := by
   intro h
   replace h := Nat.mod_eq_zero_of_dvd h

MathPuzzles/Imo1964Q4.lean

@@ -10,7 +10,7 @@ import Mathlib.Tactic.Linarith
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 # International Mathematical Olympiad 1964, Problem 4
 
 Seventeen people correspond by mail with one another -- each one with
@@ -21,7 +21,7 @@ about the same topic.
 
 -/
 
-namespace Imo1964Q4
+#[problem_setup] namespace Imo1964Q4
 
 /--
  Smaller version of the problem, with 6 (or more) people and 2 topics.
@@ -109,7 +109,7 @@ theorem lemma1
       have h9 := ht3 t3'
       rw[←h9]
 
-@[problem_statement]
+#[problem_statement]
 theorem imo1964_q4
     (Person Topic : Type)
     [Fintype Person] [DecidableEq Person]

MathPuzzles/Imo1986Q1.lean

@@ -12,13 +12,15 @@ import Mathlib.Tactic
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 # IMO 1986 Q1
 
 Let d be any positive integer not equal to 2, 5 or 13.
 Show that one can find distinct a, b in the set {2, 5, 13, d} such that ab - 1
 is not a perfect square.
+-/
 
+/-
 # Solution
 
 We proof a slightly stronger statement, namely the statement:
@@ -92,7 +94,7 @@ theorem imo1986_q1' (d : ℤ):
     exact ⟨w * v, hnm'⟩
   exact Int.even_iff_not_odd.mp hdeven hdodd
 
-@[problem_statement]
+#[problem_statement]
 theorem imo1986_q1 (d : ℤ) (_hdpos : 1 ≤ d) (h2 : d ≠ 2) (h5 : d ≠ 5) (h13 : d ≠ 13) :
     ∃ a b :({2, 5, 13, d} : Finset ℤ), (a ≠ b) ∧ ¬ ∃ z, z^2 = (a * (b : ℤ) - 1) := by
   by_contra h

MathPuzzles/Imo1987Q4.lean

@@ -9,19 +9,18 @@ import Mathlib.Data.Nat.Basic
 import Mathlib.Data.Nat.Interval
 import Mathlib.Data.Set.Basic
 import Mathlib.Data.Fintype.Card
-import Mathlib.Tactic.LibrarySearch
 import Mathlib.Tactic.Ring
 
 import MathPuzzles.Meta.Attributes
 
-/-!
+#[problem_setup]/-!
 # International Mathematical Olympiad 1987, Problem 4
 
 Prove that there is no function f : ℕ → ℕ such that f(f(n)) = n + 1987
 for every n.
 -/
 
-namespace Imo1987Q4
+#[problem_setup] namespace Imo1987Q4
 
 lemma subset_finite {A B : Set ℕ} (h : A ⊆ B) (hab : Finite ↑B) : Finite ↑A := by
   rw[Set.finite_coe_iff]
@@ -113,7 +112,7 @@ theorem imo1987_q4_generalized (m : ℕ) :
   apply_fun (· % 2) at h2
   norm_num at h2
 
-@[problem_statement]
+#[problem_statement]
 theorem imo1987_q4 : (¬∃ f : ℕ → ℕ, ∀ n, f (f n) = n + 1987) := by
   rw[show 1987 = (2 * 993 + 1) by norm_num]
   exact imo1987_q4_generalized 993