Merge remote-tracking branch 'origin/master' into torsion-free-groups

* origin/master: (394 commits) feat(data/set/[basic|prod]): make `×ˢ` bind more strongly, and define `mem.out` (#13422) feat(order/basic): Simple shortcut lemmas (#13421) chore(number_theory/dioph): Cleanup (#13403) feat(analysis/normed_space/exponential): ring homomorphisms are preserved by the exponential (#13402) feat(algebraic_geometry/projective_spectrum): degree zero part of a localized ring (#13398) feat(set_theory/cardinal): A set of cardinals is small iff it's bounded (#13373) feat(data/polynomial/{derivative, iterated_deriv}): reduce assumptions (#13368) feat(algebra/monoid_algebra/grading): Use the new graded_algebra API (#13360) feat(algebra/group/to_additive): let @[to_additive] mimic alias’s docstrings (#13330) feat(set_theory/cofinality): Basic fundamental sequences (#13326) feat(special_functions/pow): continuity of real to complex power (#13244) feat(group_theory/torsion): extension closedness, and torsion scalars in modules (#13172) feat(category_theory/path_category): canonical quotient of a path category (#13159) refactor(number_theory/padics/padic_norm): Switch nat and rat definitions (#12454) feat(analysis/normed): more lemmas about the sup norm on pi types and matrices (#13536) fix(category_theory/monoidal): improve hygiene in coherence tactic (#13507) feat(src/number_theory/cyclotomic/discriminant): add discr_prime_pow_ne_two (#13465) chore(algebra/group/type_tags): missing simp lemmas (#13553) feat(measure_theory): allow measurability to prove ae_strongly_measurable (#13427) refactor(algebra/hom/group): generalize a few lemmas to `monoid_hom_class` (#13447) chore(data/list/cycle): Add basic `simp` lemmas + minor golfing (#13533) feat(algebra/hom/non_unital_alg): introduce notation for non-unital algebra homomorphisms (#13470) chore(algebra/group/defs): Declare `field_simps` attribute earlier (#13543) feat(analysis/normed/normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556) refactor(analysis/calculus/cont_diff): reorder the file (#13468) move(set_theory/*): Organize in folders (#13530) chore(number_theory/zsqrtd/basic): simplify le_total proof (#13555) feat(group_theory/perm/basic): Iterating a permutation is the same as taking a power (#13554) feat(data/real/sqrt): `sqrt x < y ↔ x < y^2` (#13546) feat(algebra/hom/group and *): introduce `mul_hom M N` notation `M →ₙ* N` (#13526) feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361) feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace (#10372) feat(order/filter/basic): allow functions between different types in lemmas about [co]map by a constant function (#13542) feat(data/finset/basic): simp `to_finset_eq_empty` (#13531) feat(topology/algebra/algebra): ℚ-scalar multiplication is continuous (#13458) chore(model_theory/encoding): Improve the encoding of terms (#13532) feat(topology/separation): Finite sets in T2 spaces (#12845) feat(analysis/inner_product_space/gram_schmidt_ortho): Gram-Schmidt Orthogonalization and Orthonormalization (#12857) chore(algebra/big_operators/fin): golf finset.prod_range (#13535) chore(analysis/normed_space/star): make an argument explicit (#13523) feat(*): `op_op_op_comm` lemmas (#13528) chore(data/real/nnreal): add commuted version of `nnreal.mul_finset_sup` (#13512) chore(*/matrix): order `m` and `n` alphabetically (#13510) feat(analysis/calculus/specific_functions): trivial extra lemmas (#13516) feat(analysis): lemmas about nnnorm and nndist (#13498) feat(data/int/basic): add lemma `int.abs_le_one_iff` (#13513) feat(category_theory/limits): add characteristic predicate for zero objects (#13511) feat(order/filter/n_ary): Add lemma equating map₂ to map on the product (#13490) fix(analysis/locally_convex/balanced_hull_core): minimize import (#13450) feat(order/cover): define `wcovby` (#13424) ...
leanprover-community · Apr 21, 2022 · eb3119e · eb3119e
2 parents 48a671b + 0f9edf9
commit eb3119e
Show file tree

Hide file tree

Showing 731 changed files with 25,631 additions and 9,622 deletions.
diff --git a/README.md b/README.md
@@ -47,6 +47,34 @@ better browsing interface, and to participate in the discussions, we strongly
 suggest joining the chat. Questions from users at all levels of expertise are
 welcomed.
 
+## Contributing
+
+The complete documentation for contributing to ``mathlib`` is located
+[on the community guide contribute to mathlib](https://leanprover-community.github.io/contribute/index.html)
+
+The process is different from other projects where one should not fork the repository.
+Instead write permission for non-master branches should be requested on [Zulip](https://leanprover.zulipchat.com)
+by introducing yourself, providing your GitHub handle and what contribution you are planning on doing.
+
+### Guidelines
+
+Mathlib has the following guidelines and conventions that must be followed
+
+ - The [style guide](https://leanprover-community.github.io/contribute/style.html)
+ - A guide on the [naming convention](https://leanprover-community.github.io/contribute/naming.html)
+ - The [documentation style](https://leanprover-community.github.io/contribute/doc.html)
+ - The [commit naming conventions](https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md)
+
+Note: the title of a PR should follow the commit naming convention.
+
+### Using ``leanproject`` to contribute
+
+Running the ``leanproject get -b mathlib:shiny_lemma`` command will create a new worktree ``mathlib_shiny_lemma``
+with a local branch called ``shiny_lemma`` which has a copy of mathlib to work on.
+
+``leanproject build`` will check that nothing broke.
+Be warned that this will take some time if a fundamental file was changed.
+
 ## Maintainers:
 
 * Anne Baanen (@Vierkantor): algebra, number theory, tactics

diff --git a/archive/100-theorems-list/37_solution_of_cubic.lean b/archive/100-theorems-list/37_solution_of_cubic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Jeoff Lee. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeoff Lee
 -/
-import tactic.basic
+import tactic.linear_combination
 import ring_theory.roots_of_unity
 import ring_theory.polynomial.cyclotomic.basic
 
@@ -46,7 +46,7 @@ variables {ω p q r s t : K}
 
 lemma cube_root_of_unity_sum (hω : is_primitive_root ω 3) : 1 + ω + ω^2 = 0 :=
 begin
-  convert is_root_cyclotomic (nat.succ_pos _) hω,
+  convert hω.is_root_cyclotomic (nat.succ_pos _),
   rw [cyclotomic_eq_geom_sum nat.prime_three, eval_geom_sum],
   simp only [geom_sum_succ, geom_sum_zero],
   ring,
@@ -68,26 +68,18 @@ begin
   have h₁ : ∀ x a₁ a₂ a₃ : K, x = a₁ ∨ x = a₂ ∨ x = a₃ ↔ (x - a₁) * (x - a₂) * (x - a₃) = 0,
   { intros, simp only [mul_eq_zero, sub_eq_zero, or.assoc] },
   rw h₁,
-  suffices : x ^ 3 + 3 * p * x - 2 * q
-    = (x - (s - t)) * (x - (s * ω - t * ω^2)) * (x - (s * ω^2 - t * ω)),
-  { rw this, },
-  have hc : s^3 - t^3 = 2 * q,
-  { have : s ≠ 0 := λ h, by { apply hp_nonzero, rw [h, mul_zero] at ht, exact ht.symm },
-    have h_nonzero: q + r ≠ 0 := by { rw ← hs3, exact pow_ne_zero _ this },
-    have hp3 : p^3 = r^2 - q^2 := by { rw hr, ring },
-    calc    s^3 - t^3
-          = s^3 - p^3/s^3 : by { rw [← ht], field_simp, ring }
-      ... = (q+r) - (r^2-q^2)/(q+r) : by rw [hs3, hp3]
-      ... = (q+r) + (q-r) * ((q+r) / (q+r)) : by ring
-      ... = 2 * q : by { rw div_self h_nonzero, ring } },
-  symmetry,
-  calc (x - (s - t)) * (x - (s * ω - t * ω^2)) * (x - (s * ω^2 - t * ω))
-      = x^3 - (s-t) * (1+ω+ω^2) * x^2
-        + ((s^2+t^2)*ω*(1+ω+ω^2) - s*t*(-3 + 3*(1+ω+ω^2) + ω*(ω^3-1))) * x
-        - (s^3-t^3)*ω^3 + s*t*(s-t)*ω^2*(1+ω+ω^2) : by ring
-  ... = x^3 + 3*(t*s)*x - (s^3-t^3)
-    : by { rw [hω.pow_eq_one, cube_root_of_unity_sum hω], ring }
-  ... = x^3 + 3*p*x - 2*q : by rw [ht, hc]
+  refine eq.congr _ rfl,
+  have hs_nonzero : s ≠ 0,
+  { contrapose! hp_nonzero with hs_nonzero,
+    linear_combination (ht, -1) (hs_nonzero, t) },
+  rw ← mul_left_inj' (pow_ne_zero 3 hs_nonzero),
+  have H := cube_root_of_unity_sum hω,
+  linear_combination
+    (hr, 1)
+    (hs3, - q + r + s ^ 3)
+    (ht, -3 * x * s ^ 3 - (t * s) ^ 2 - (t * s) * p - p ^ 2)
+    (H, (x ^ 2 * (s - t) + x * (- ω * (s ^ 2 + t ^ 2) + s * t * (3 + ω ^ 2 - ω))
+        - (-(s ^ 3 - t ^ 3) * (ω - 1) + s^2 * t * ω ^ 2 - s * t^2 * ω ^ 2)) * s ^ 3),
 end
 
 /-- Roots of a monic cubic whose discriminant is nonzero. -/

diff --git a/archive/100-theorems-list/45_partition.lean b/archive/100-theorems-list/45_partition.lean
@@ -7,6 +7,7 @@ import ring_theory.power_series.basic
 import combinatorics.partition
 import data.nat.parity
 import data.finset.nat_antidiagonal
+import data.fin.tuple.nat_antidiagonal
 import tactic.interval_cases
 import tactic.apply_fun
 
@@ -84,8 +85,8 @@ def partial_distinct_gf (m : ℕ) [comm_semiring α] :=
 /--
 Functions defined only on `s`, which sum to `n`. In other words, a partition of `n` indexed by `s`.
 Every function in here is finitely supported, and the support is a subset of `s`.
-This should be thought of as a generalisation of `finset.nat.antidiagonal`, where
-`antidiagonal n` is the same thing as `cut s n` if `s` has two elements.
+This should be thought of as a generalisation of `finset.nat.antidiagonal_tuple` where
+`antidiagonal_tuple k n` is the same thing as `cut (s : finset.univ (fin k)) n`.
 -/
 def cut {ι : Type*} (s : finset ι) (n : ℕ) : finset (ι → ℕ) :=
 finset.filter (λ f, s.sum f = n) ((s.pi (λ _, range (n+1))).map
@@ -120,6 +121,10 @@ begin
   simp [mem_cut, add_comm],
 end
 
+lemma cut_univ_fin_eq_antidiagonal_tuple (n : ℕ) (k : ℕ) :
+  cut univ n = nat.antidiagonal_tuple k n :=
+by { ext, simp [nat.mem_antidiagonal_tuple, mem_cut] }
+
 /-- There is only one `cut` of 0. -/
 @[simp]
 lemma cut_zero {ι : Type*} (s : finset ι) :
@@ -412,6 +417,7 @@ begin
     rw nat.div_lt_iff_lt_mul _ _ zero_lt_two,
     exact lt_of_le_of_lt hin h },
   { rintro ⟨a, -, rfl⟩,
+    rw even_iff_two_dvd,
     apply nat.two_not_dvd_two_mul_add_one },
 end
 

diff --git a/archive/100-theorems-list/70_perfect_numbers.lean b/archive/100-theorems-list/70_perfect_numbers.lean
@@ -84,6 +84,7 @@ begin
   have hpos := perf.2,
   rcases eq_two_pow_mul_odd hpos with ⟨k, m, rfl, hm⟩,
   use k,
+  rw even_iff_two_dvd at hm,
   rw [perfect_iff_sum_divisors_eq_two_mul hpos, ← sigma_one_apply,
     is_multiplicative_sigma.map_mul_of_coprime (nat.prime_two.coprime_pow_of_not_dvd hm).symm,
     sigma_two_pow_eq_mersenne_succ, ← mul_assoc, ← pow_succ] at perf,
@@ -106,7 +107,7 @@ begin
       { apply hm,
         rw [← jcon2, pow_zero, one_mul, one_mul] at ev,
         rw [← jcon2, one_mul],
-        exact ev },
+        exact even_iff_two_dvd.mp ev },
       apply ne_of_lt _ jcon2,
       rw [mersenne, ← nat.pred_eq_sub_one, lt_pred_iff, ← pow_one (nat.succ 1)],
       apply pow_lt_pow (nat.lt_succ_self 1) (nat.succ_lt_succ (nat.succ_pos k)) },

diff --git a/archive/100-theorems-list/82_cubing_a_cube.lean b/archive/100-theorems-list/82_cubing_a_cube.lean
@@ -7,7 +7,8 @@ import data.fin.tuple
 import data.real.basic
 import data.set.intervals
 import data.set.pairwise
-import set_theory.cardinal
+import set_theory.cardinal.basic
+
 /-!
 Proof that a cube (in dimension n ≥ 3) cannot be cubed:
 There does not exist a partition of a cube into finitely many smaller cubes (at least two)
@@ -509,7 +510,7 @@ omit h
 /-- The infinite sequence of cubes contradicts the finiteness of the family. -/
 theorem not_correct : ¬correct cs :=
 begin
-  intro h, apply not_le_of_lt (lt_omega_iff_fintype.mpr ⟨_inst_1⟩),
+  intro h, apply (lt_omega_of_fintype ι).not_le,
   rw [omega, lift_id], fapply mk_le_of_injective, exact λ n, (sequence_of_cubes h n).1,
   intros n m hnm, apply strict_mono.injective (strict_mono_sequence_of_cubes h),
   dsimp only [decreasing_sequence], rw hnm

diff --git a/archive/imo/imo1994_q1.lean b/archive/imo/imo1994_q1.lean
@@ -35,17 +35,17 @@ open finset
 lemma tedious (m : ℕ) (k : fin (m+1)) : m - (m + (m + 1 - ↑k)) % (m + 1) = ↑k  :=
 begin
   cases k with k hk,
-  rw [nat.lt_succ_iff,le_iff_exists_add] at hk,
+  rw [nat.lt_succ_iff, le_iff_exists_add] at hk,
   rcases hk with ⟨c, rfl⟩,
   have : k + c + (k + c + 1 - k) = c + (k + c + 1),
-  { simp only [add_assoc, add_tsub_cancel_left], ring_nf, },
+  { simp only [add_assoc, add_tsub_cancel_left, add_left_comm] },
   rw [fin.coe_mk, this, nat.add_mod_right, nat.mod_eq_of_lt, nat.add_sub_cancel],
   linarith
 end
 
 theorem imo1994_q1 (n : ℕ) (m : ℕ) (A : finset ℕ) (hm : A.card = m + 1)
   (hrange : ∀ a ∈ A, 0 < a ∧ a ≤ n) (hadd : ∀ (a b ∈ A), a + b ≤ n → a + b ∈ A) :
-  (m+1)*(n+1) ≤ 2*(∑ x in A, x) :=
+  (m + 1) * (n + 1) ≤ 2 * ∑ x in A, x :=
 begin
   set a := order_emb_of_fin A hm,  -- We sort the elements of `A`
   have ha : ∀ i, a i ∈ A := λ i, order_emb_of_fin_mem A hm i,
@@ -64,7 +64,7 @@ begin
   ... = ∑ i : fin (m+1), a i + ∑ i : fin (m+1), a (rev i) : by rw equiv.sum_comp rev
   ... = ∑ i : fin (m+1), (a i + a (rev i))                : sum_add_distrib.symm
   ... ≥ ∑ i : fin (m+1), (n+1)                            : sum_le_sum hpair
-  ... = (m+1) * (n+1)                                     : by simp,
+  ... = (m+1) * (n+1) : by rw [sum_const, card_fin, nat.nsmul_eq_mul],
 
   -- It remains to prove the key inequality, by contradiction
   rintros k -,
@@ -81,20 +81,19 @@ begin
   -- Proof that the `f i` are greater than `a (rev k)` for `i ≤ k`
   have hf : map f (Icc 0 k) ⊆ map a.to_embedding (Ioc (rev k) (fin.last m)),
   { intros x hx,
-    simp at h hx ⊢,
+    simp only [equiv.sub_left_apply] at h,
+    simp only [mem_map, f, mem_Icc, mem_Ioc, fin.zero_le, true_and, equiv.sub_left_apply,
+      function.embedding.coe_fn_mk, exists_prop, rel_embedding.coe_fn_to_embedding] at hx ⊢,
     rcases hx with ⟨i, ⟨hi, rfl⟩⟩,
     have h1 : a i + a (fin.last m - k) ≤ n,
     { linarith only [h, a.monotone hi] },
     have h2 : a i + a (fin.last m - k) ∈ A := hadd _ (ha _) _ (ha _) h1,
     rw [←mem_coe, ←range_order_emb_of_fin A hm, set.mem_range] at h2,
     cases h2 with j hj,
-    use j,
-    refine ⟨⟨_, fin.le_last j⟩, hj⟩,
+    refine ⟨j, ⟨_, fin.le_last j⟩, hj⟩,
     rw [← a.strict_mono.lt_iff_lt, hj],
     simpa using (hrange (a i) (ha i)).1 },
 
   -- A set of size `k+1` embed in one of size `k`, which yields a contradiction
-  have ineq := card_le_of_subset hf,
-  simp [fin.coe_sub, tedious] at ineq,
-  contradiction ,
+  simpa [fin.coe_sub, tedious] using card_le_of_subset hf,
 end
diff --git a/archive/imo/imo2001_q6.lean b/archive/imo/imo2001_q6.lean
@@ -6,7 +6,7 @@ Authors: Sara Díaz Real
 import data.int.basic
 import algebra.associated
 import tactic.linarith
-import tactic.ring
+import tactic.linear_combination
 
 /-!
 # IMO 2001 Q6
@@ -31,22 +31,15 @@ begin
   -- the key step is to show that `a*c + b*d` divides the product `(a*b + c*d) * (a*d + b*c)`
   have dvd_mul : a*c + b*d ∣ (a*b + c*d) * (a*d + b*c),
   { use b^2 + b*d + d^2,
-    have equivalent_sums : a^2 - a*c + c^2 = b^2 + b*d + d^2,
-    { ring_nf at h, nlinarith only [h], },
-    calc  (a * b + c * d) * (a * d + b * c)
-        = a*c * (b^2 + b*d + d^2) + b*d * (a^2 - a*c + c^2) : by ring
-    ... = a*c * (b^2 + b*d + d^2) + b*d * (b^2 + b*d + d^2) : by rw equivalent_sums
-    ... = (a * c + b * d) * (b ^ 2 + b * d + d ^ 2)         : by ring, },
+    linear_combination (h, b*d) },
   -- since `a*b + c*d` is prime (by assumption), it must divide `a*c + b*d` or `a*d + b*c`
   obtain (h1 : a*b + c*d ∣ a*c + b*d) | (h2 : a*c + b*d ∣ a*d + b*c) :=
     h0.left_dvd_or_dvd_right_of_dvd_mul dvd_mul,
   -- in both cases, we derive a contradiction
   { have aux : 0 < a*c + b*d,         { nlinarith only [ha, hb, hc, hd] },
     have : a*b + c*d ≤ a*c + b*d,     { from int.le_of_dvd aux h1 },
-    have : ¬ (a*b + c*d ≤ a*c + b*d), { nlinarith only [hba, hcb, hdc, h] },
-    contradiction, },
+    nlinarith only [hba, hcb, hdc, h, this] },
   { have aux : 0 < a*d + b*c,         { nlinarith only [ha, hb, hc, hd] },
     have : a*c + b*d ≤ a*d + b*c,     { from int.le_of_dvd aux h2 },
-    have : ¬ (a*c + b*d ≤ a*d + b*c), { nlinarith only [hba, hdc, h] },
-    contradiction, },
+    nlinarith only [hba, hdc, h, this] },
 end
diff --git a/archive/imo/imo2005_q3.lean b/archive/imo/imo2005_q3.lean
@@ -20,18 +20,15 @@ and then making use of `xyz ≥ 1` to show `(x^5-x^2)/(x^3*(x^2+y^2+z^2)) ≥ (x
 lemma key_insight (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x*y*z ≥ 1) :
   (x^5-x^2)/(x^5+y^2+z^2) ≥ (x^2-y*z)/(x^2+y^2+z^2) :=
 begin
-  have h₁ : x^5+y^2+z^2 > 0, linarith [pow_pos hx 5, pow_pos hy 2, pow_pos hz 2],
-  have h₂ : x^3 > 0, exact pow_pos hx 3,
-  have h₃ : x^2+y^2+z^2 > 0, linarith [pow_pos hx 2, pow_pos hy 2, pow_pos hz 2],
-  have h₄ : x^3*(x^2+y^2+z^2) > 0, exact mul_pos h₂ h₃,
+  have h₁ : 0 < x^5+y^2+z^2, linarith [pow_pos hx 5, pow_pos hy 2, pow_pos hz 2],
+  have h₂ : 0 < x^3, exact pow_pos hx 3,
+  have h₃ : 0 < x^2+y^2+z^2, linarith [pow_pos hx 2, pow_pos hy 2, pow_pos hz 2],
+  have h₄ : 0 < x^3*(x^2+y^2+z^2), exact mul_pos h₂ h₃,
 
   have key : (x^5-x^2)/(x^5+y^2+z^2) - (x^5-x^2)/(x^3*(x^2+y^2+z^2))
            = ((x^3 - 1)^2*x^2*(y^2 + z^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))),
-  calc  (x^5-x^2)/(x^5+y^2+z^2) - (x^5-x^2)/(x^3*(x^2+y^2+z^2))
-      = ((x^5-x^2)*(x^3*(x^2+y^2+z^2))-(x^5+y^2+z^2)*(x^5-x^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))):
-        by exact div_sub_div _ _ (ne_of_gt h₁) (ne_of_gt h₄)    -- a/b - c/d = (a*d-b*c)/(b*d)
-  ... = ((x^3 - 1)^2*x^2*(y^2 + z^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))) :
-        by ring,
+  { field_simp [h₁.ne', h₄.ne'],
+    ring },
 
   have h₅ : ((x^3 - 1)^2*x^2*(y^2 + z^2))/((x^5+y^2+z^2)*(x^3*(x^2+y^2+z^2))) ≥ 0,
   { refine div_nonneg _ _,
@@ -45,7 +42,7 @@ begin
         by { refine (div_le_div_right h₄).mpr _, simp,
              exact (le_mul_iff_one_le_right (pow_pos hx 2)).mpr h }
   ... = (x^2-y*z)/(x^2+y^2+z^2) :
-        by { field_simp [ne_of_gt h₂, ne_of_gt h₃], ring },
+        by { field_simp [h₂.ne', h₃.ne'], ring },
 end
 
 theorem imo2005_q3 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x*y*z ≥ 1) :
@@ -56,11 +53,10 @@ begin
         by { linarith [key_insight x y z hx hy hz h,
                        key_insight y z x hy hz hx (by linarith [h]),
                        key_insight z x y hz hx hy (by linarith [h])] }
-  ... = (x^2 + y^2 + z^2 - y*z - z*x - x*y) / (x^2+y^2+z^2) :
-        by { have h₁ : y^2+z^2+x^2 = x^2+y^2+z^2, linarith,
-             have h₂ : z^2+x^2+y^2 = x^2+y^2+z^2, linarith,
+  ... = 1/2*( (x-y)^2 + (y-z)^2 + (z-x)^2 ) / (x^2+y^2+z^2) :
+        by { have h₁ : y^2+z^2+x^2 = x^2+y^2+z^2, ring,
+             have h₂ : z^2+x^2+y^2 = x^2+y^2+z^2, ring,
              rw [h₁, h₂], ring }
-  ... = 1/2*( (x-y)^2 + (y-z)^2 + (z-x)^2 ) / (x^2+y^2+z^2) : by ring
   ... ≥ 0 :
         by { exact div_nonneg
                 (by linarith [sq_nonneg (x-y), sq_nonneg (y-z), sq_nonneg (z-x)])

diff --git a/archive/imo/imo2008_q3.lean b/archive/imo/imo2008_q3.lean
@@ -7,7 +7,8 @@ import data.real.basic
 import data.real.sqrt
 import data.nat.prime
 import number_theory.primes_congruent_one
-import number_theory.quadratic_reciprocity
+import number_theory.legendre_symbol.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⟩,