feat: port IMO 2006 Q5 helper results (#3136)

We don't port the IMO proof itself since it seems there's no archive in Mathlib4.

Mathlib 3: leanprover-community/mathlib3#15613



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author: vihdzp

Mathlib/Data/Int/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 
 ! This file was ported from Lean 3 source module data.int.basic
-! leanprover-community/mathlib commit 2196ab363eb097c008d4497125e0dde23fb36db2
+! leanprover-community/mathlib commit 728baa2f54e6062c5879a3e397ac6bac323e506f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -127,6 +127,16 @@ theorem coe_nat_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := ofNat_le.2 (Nat.zero_le _)
 #align int.neg_of_nat_ne_zero Int.negSucc_ne_zero
 #align int.zero_ne_neg_of_nat Int.zero_ne_negSucc
 
+@[simp]
+theorem sign_coe_add_one (n : ℕ) : Int.sign (n + 1) = 1 :=
+  rfl
+#align int.sign_coe_add_one Int.sign_coe_add_one
+
+@[simp]
+theorem sign_negSucc (n : ℕ) : Int.sign -[n+1] = -1 :=
+  rfl
+#align int.sign_neg_succ_of_nat Int.sign_negSucc
+
 /-! ### succ and pred -/
 
 /-- Immediate successor of an integer: `succ n = n + 1` -/

Mathlib/Data/Int/Order/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 
 ! This file was ported from Lean 3 source module data.int.order.basic
-! leanprover-community/mathlib commit bd835ef554f37ef9b804f0903089211f89cb370b
+! leanprover-community/mathlib commit 728baa2f54e6062c5879a3e397ac6bac323e506f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -90,6 +90,13 @@ theorem coe_nat_ne_zero_iff_pos {n : ℕ} : (n : ℤ) ≠ 0 ↔ 0 < n :=
 @[norm_cast] lemma abs_coe_nat (n : ℕ) : |(n : ℤ)| = n := abs_of_nonneg (coe_nat_nonneg n)
 #align int.abs_coe_nat Int.abs_coe_nat
 
+theorem sign_add_eq_of_sign_eq : ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign := by
+  have : (1 : ℤ) ≠ -1 := by decide
+  rintro ((_ | m) | m) ((_ | n) | n) <;> simp [this, this.symm]
+  rw [Int.sign_eq_one_iff_pos]
+  apply Int.add_pos <;> · exact zero_lt_one.trans_le (le_add_of_nonneg_left <| coe_nat_nonneg _)
+#align int.sign_add_eq_of_sign_eq Int.sign_add_eq_of_sign_eq
+
 /-! ### succ and pred -/
 
 

Mathlib/Data/List/Cycle.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yakov Pechersky
 
 ! This file was ported from Lean 3 source module data.list.cycle
-! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab
+! leanprover-community/mathlib commit 728baa2f54e6062c5879a3e397ac6bac323e506f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -745,6 +745,12 @@ theorem map_eq_nil {β : Type _} (f : α → β) (s : Cycle α) : map f s = nil
   Quotient.inductionOn' s (by simp)
 #align cycle.map_eq_nil Cycle.map_eq_nil
 
+@[simp]
+theorem mem_map {β : Type _} {f : α → β} {b : β} {s : Cycle α} :
+    b ∈ s.map f ↔ ∃ a, a ∈ s ∧ f a = b :=
+  Quotient.inductionOn' s (by simp)
+#align cycle.mem_map Cycle.mem_map
+
 /-- The `Multiset` of lists that can make the cycle. -/
 def lists (s : Cycle α) : Multiset (List α) :=
   Quotient.liftOn' s (fun l => (l.cyclicPermutations : Multiset (List α))) fun l₁ l₂ h => by

Mathlib/Data/Polynomial/Degree/Lemmas.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 
 ! This file was ported from Lean 3 source module data.polynomial.degree.lemmas
-! leanprover-community/mathlib commit 302eab4f46abb63de520828de78c04cb0f9b5836
+! leanprover-community/mathlib commit 728baa2f54e6062c5879a3e397ac6bac323e506f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -355,6 +355,14 @@ theorem natDegree_comp : natDegree (p.comp q) = natDegree p * natDegree q := by
       ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), pow_ne_zero, Ne.def, not_false_iff]
 #align polynomial.nat_degree_comp Polynomial.natDegree_comp
 
+@[simp]
+theorem natDegree_iterate_comp (k : ℕ) :
+    ((p.comp^[k]) q).natDegree = p.natDegree ^ k * q.natDegree := by
+  induction' k with k IH
+  · simp
+  · rw [Function.iterate_succ_apply', natDegree_comp, IH, pow_succ, mul_assoc]
+#align polynomial.nat_degree_iterate_comp Polynomial.natDegree_iterate_comp
+
 theorem leadingCoeff_comp (hq : natDegree q ≠ 0) :
     leadingCoeff (p.comp q) = leadingCoeff p * leadingCoeff q ^ natDegree p := by
   rw [← coeff_comp_degree_mul_degree hq, ← natDegree_comp, coeff_natDegree]

Mathlib/Data/Polynomial/Eval.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker
 
 ! This file was ported from Lean 3 source module data.polynomial.eval
-! leanprover-community/mathlib commit e064a7bf82ad94c3c17b5128bbd860d1ec34874e
+! leanprover-community/mathlib commit 728baa2f54e6062c5879a3e397ac6bac323e506f
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -1035,6 +1035,14 @@ theorem eval₂_comp {x : S} : eval₂ f x (p.comp q) = eval₂ f (eval₂ f x q
   rw [comp, p.as_sum_range]; simp [eval₂_finset_sum, eval₂_pow]
 #align polynomial.eval₂_comp Polynomial.eval₂_comp
 
+@[simp]
+theorem iterate_comp_eval₂ (k : ℕ) (t : S) :
+    eval₂ f t ((p.comp^[k]) q) = ((fun x => eval₂ f x p)^[k]) (eval₂ f t q) := by
+  induction' k with k IH
+  · simp
+  · rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]
+#align polynomial.iterate_comp_eval₂ Polynomial.iterate_comp_eval₂
+
 end
 
 section