feat(archive/imo/imo2008_q3): golf (#13232)

archive/imo/imo2008_q3.lean

@@ -8,6 +8,7 @@ import data.real.sqrt
 import data.nat.prime
 import number_theory.primes_congruent_one
 import number_theory.quadratic_reciprocity
+import tactic.linear_combination
 
 /-!
 # IMO 2008 Q3
@@ -51,43 +52,29 @@ begin
 
   have hnat₅ : p ∣ k ^ 2 + 4,
   { cases hnat₁ with x hx,
-    let p₁ := (p : ℤ), let n₁ := (n : ℤ), let k₁ := (k : ℤ), let x₁ := (x : ℤ),
-    have : p₁ ∣ k₁ ^ 2 + 4,
-    { use p₁ - 4 * n₁ + 4 * x₁,
-      have hcast₁ : k₁ = p₁ - 2 * n₁, { assumption_mod_cast },
-      have hcast₂ : n₁ ^ 2 + 1 = p₁ * x₁, { assumption_mod_cast },
-      calc  k₁ ^ 2 + 4
-          = (p₁ - 2 * n₁) ^ 2 + 4                   : by rw hcast₁
-      ... = p₁ ^ 2 - 4 * p₁ * n₁ + 4 * (n₁ ^ 2 + 1) : by ring
-      ... = p₁ ^ 2 - 4 * p₁ * n₁ + 4 * (p₁ * x₁)    : by rw hcast₂
-      ... = p₁ * (p₁ - 4 * n₁ + 4 * x₁)             : by ring },
+    have : (p:ℤ) ∣ k ^ 2 + 4,
+    { use (p:ℤ) - 4 * n + 4 * x,
+      have hcast₁ : (k:ℤ) = p - 2 * n, { assumption_mod_cast },
+      have hcast₂ : (n:ℤ) ^ 2 + 1 = p * x, { assumption_mod_cast },
+      linear_combination (hcast₁, (k:ℤ) + p - 2 * n) (hcast₂, 4) },
     assumption_mod_cast },
 
   have hnat₆ : k ^ 2 + 4 ≥ p := nat.le_of_dvd (k ^ 2 + 3).succ_pos hnat₅,
 
-  let p₀ := (p : ℝ), let n₀ := (n : ℝ), let k₀ := (k : ℝ),
+  have hreal₁ : (k:ℝ) = p - 2 * n, { assumption_mod_cast },
+  have hreal₂ : (p:ℝ) > 20,        { assumption_mod_cast },
+  have hreal₃ : (k:ℝ) ^ 2 + 4 ≥ p, { assumption_mod_cast },
 
-  have hreal₁ : p₀ = 2 * n₀ + k₀, { linarith [(show k₀ = p₀ - 2 * n₀, by assumption_mod_cast)] },
-  have hreal₂ : p₀ > 20,          { assumption_mod_cast },
-  have hreal₃ : k₀ ^ 2 + 4 ≥ p₀,  { assumption_mod_cast },
+  have hreal₅ : (k:ℝ) > 4,
+  { apply lt_of_pow_lt_pow 2 k.cast_nonneg,
+    linarith only [hreal₂, hreal₃] },
 
-  have hreal₄ : k₀ ≥ sqrt(p₀ - 4),
-  { calc k₀ = sqrt(k₀ ^ 2) : eq.symm (sqrt_sq (nat.cast_nonneg k))
-    ...     ≥ sqrt(p₀ - 4) : sqrt_le_sqrt (by linarith [hreal₃]) },
+  have hreal₆ : (k:ℝ) > sqrt (2 * n),
+  { apply lt_of_pow_lt_pow 2 k.cast_nonneg,
+    rw sq_sqrt (mul_nonneg zero_le_two n.cast_nonneg),
+    linarith only [hreal₁, hreal₃, hreal₅] },
 
-  have hreal₅ : k₀ > 4,
-  { calc k₀ ≥ sqrt(p₀ - 4) : hreal₄
-    ...     > sqrt(4 ^ 2)  : sqrt_lt_sqrt (by norm_num) (by linarith [hreal₂])
-    ...     = 4            : sqrt_sq zero_lt_four.le },
-
-  have hreal₆ : p₀ > 2 * n₀ + sqrt(2 * n),
-  { calc p₀ = 2 * n₀ + k₀                    : hreal₁
-    ...     ≥ 2 * n₀ + sqrt(p₀ - 4)          : add_le_add_left hreal₄ _
-    ...     = 2 * n₀ + sqrt(2 * n₀ + k₀ - 4) : by rw hreal₁
-    ...     > 2 * n₀ + sqrt(2 * n₀) : add_lt_add_left
-        (sqrt_lt_sqrt (mul_nonneg zero_le_two n.cast_nonneg) $ by linarith [hreal₅]) (2 * n₀) },
-
-  exact ⟨n, hnat₁, hreal₆⟩,
+  exact ⟨n, hnat₁, by linarith only [hreal₆, hreal₁]⟩,
 end
 
 theorem imo2008_q3 : ∀ N : ℕ, ∃ n : ℕ, n ≥ N ∧
@@ -98,7 +85,7 @@ begin
   obtain ⟨n, hnat, hreal⟩ := p_lemma p hpp hpmod4 (by linarith [hineq₁, nat.zero_le (N ^ 2)]),
 
   have hineq₂  : n ^ 2 + 1 ≥ p := nat.le_of_dvd (n ^ 2).succ_pos hnat,
-  have hineq₃  : n * n ≥ N * N, { linarith [hineq₁, hineq₂, (sq n), (sq N)] },
+  have hineq₃  : n * n ≥ N * N, { linarith [hineq₁, hineq₂] },
   have hn_ge_N : n ≥ N := nat.mul_self_le_mul_self_iff.mpr hineq₃,
 
   exact ⟨n, hn_ge_N, p, hpp, hnat, hreal⟩,