internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2015A1.final_solution
Proof state before:
case refine_2.inl
F : Type u_1
inst✝ : LinearOrderedField F
a : ℕ → F
h : ∀ (k : ℕ), 0 < a k
h0 : ∀ (k : ℕ), ↑k.succ / a k.succ ≤ a k + ↑k / a k
n : ℕ
h1 : 2 ≤ n
h2 : ↑n ≤ (range n).sum a
h3 : 1 ≤ a n
⊢ ↑n + 1 ≤ ∑ x ∈ range n, a x + a n
Tactic:
exact add_le_add h2 h3
Proof state after:
no goals
Theorem: IMOSL.IMO2009N3.const_of_infinite_map_eq_map_zero
Proof state before:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0 : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b : ℕ
⊢ f b = f 0
Tactic:
obtain ⟨n, h0, h1⟩ := h0 (b + (f 0 - f b).natAbs + 1)
Proof state after:
case intro.intro
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : b + (f 0 - f b).natAbs + 1 ≤ n
h1 : f n = f 0
⊢ f b = f 0
Theorem: IMOSL.IMO2009N3.const_of_infinite_map_eq_map_zero
Proof state before:
case intro.intro
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : b + (f 0 - f b).natAbs + 1 ≤ n
h1 : f n = f 0
⊢ f b = f 0
Tactic:
specialize h n b
Proof state after:
case intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : b + (f 0 - f b).natAbs + 1 ≤ n
h1 : f n = f 0
h : ↑n - ↑b ∣ f n - f b
⊢ f b = f 0
Theorem: IMOSL.IMO2009N3.const_of_infinite_map_eq_map_zero
Proof state before:
case intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : b + (f 0 - f b).natAbs + 1 ≤ n
h1 : f n = f 0
h : ↑n - ↑b ∣ f n - f b
⊢ f b = f 0
Tactic:
rw [Nat.succ_le_iff, lt_iff_exists_add] at h0
Proof state after:
case intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : ∃ c > 0, n = b + (f 0 - f b).natAbs + c
h1 : f n = f 0
h : ↑n - ↑b ∣ f n - f b
⊢ f b = f 0
Theorem: IMOSL.IMO2009N3.const_of_infinite_map_eq_map_zero
Proof state before:
case intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b n : ℕ
h0 : ∃ c > 0, n = b + (f 0 - f b).natAbs + c
h1 : f n = f 0
h : ↑n - ↑b ∣ f n - f b
⊢ f b = f 0
Tactic:
rcases h0 with ⟨C, h0, rfl⟩
Proof state after:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : ↑(b + (f 0 - f b).natAbs + C) - ↑b ∣ f (b + (f 0 - f b).natAbs + C) - f b
⊢ f b = f 0
Theorem: IMOSL.IMO2009N3.const_of_infinite_map_eq_map_zero
Proof state before:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : ↑(b + (f 0 - f b).natAbs + C) - ↑b ∣ f (b + (f 0 - f b).natAbs + C) - f b
⊢ f b = f 0
Tactic:
rw [h1, add_assoc, Nat.cast_add, add_sub_cancel_left, Int.natCast_dvd] at h
Proof state after:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : (f 0 - f b).natAbs + C ∣ (f 0 - f b).natAbs
⊢ f b = f 0
Theorem: IMOSL.IMO2009N3.const_of_infinite_map_eq_map_zero
Proof state before:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : (f 0 - f b).natAbs + C ∣ (f 0 - f b).natAbs
⊢ f b = f 0
Tactic:
have h2 := Nat.eq_zero_of_dvd_of_lt h (Nat.lt_add_of_pos_right h0)
Proof state after:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : (f 0 - f b).natAbs + C ∣ (f 0 - f b).natAbs
h2 : (f 0 - f b).natAbs = 0
⊢ f b = f 0
Theorem: IMOSL.IMO2009N3.const_of_infinite_map_eq_map_zero
Proof state before:
case intro.intro.intro.intro
f : ℕ → ℤ
h0✝ : ∀ (k : ℕ), ∃ n, k ≤ n ∧ f n = f 0
b C : ℕ
h0 : C > 0
h1 : f (b + (f 0 - f b).natAbs + C) = f 0
h : (f 0 - f b).natAbs + C ∣ (f 0 - f b).natAbs
h2 : (f 0 - f b).natAbs = 0
⊢ f b = f 0
Tactic:
rwa [Int.natAbs_eq_zero, sub_eq_zero, eq_comm] at h2
Proof state after:
no goals
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
⊢ ∃ C, f = fun x => C
Tactic:
have h1 : f 0 ≠ 0 := λ h1 ↦ by
  obtain ⟨p, h2, h3⟩ := K.exists_infinite_primes
  exact h2.not_lt (h0 p h3 ⟨0, 0, h1⟩)
Proof state after:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
⊢ ∃ C, f = fun x => C
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
⊢ ∃ C, f = fun x => C
Tactic:
refine const_of_infinite_map_eq_map_zero h
  λ k ↦ ⟨(f 0).natAbs * (4 * K.factorial) * k, ?_, ?_⟩
Proof state after:
case refine_1
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
⊢ k ≤ (f 0).natAbs * (4 * K.factorial) * k

case refine_2
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 = 0
⊢ False
Tactic:
obtain ⟨p, h2, h3⟩ := K.exists_infinite_primes
Proof state after:
case intro.intro
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 = 0
p : ℕ
h2 : K ≤ p
h3 : p.Prime
⊢ False
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case intro.intro
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 = 0
p : ℕ
h2 : K ≤ p
h3 : p.Prime
⊢ False
Tactic:
exact h2.not_lt (h0 p h3 ⟨0, 0, h1⟩)
Proof state after:
no goals
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_1
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
⊢ k ≤ (f 0).natAbs * (4 * K.factorial) * k
Tactic:
exact Nat.le_mul_of_pos_left _ <| Nat.mul_pos (Int.natAbs_pos.mpr h1)
  (Nat.mul_pos (Nat.succ_pos 3) K.factorial_pos)
Proof state after:
no goals
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_2
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Tactic:
specialize h ((f 0).natAbs * (4 * K.factorial) * k) 0
Proof state after:
case refine_2
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : ↑((f 0).natAbs * (4 * K.factorial) * k) - ↑0 ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_2
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : ↑((f 0).natAbs * (4 * K.factorial) * k) - ↑0 ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Tactic:
rw [Nat.cast_zero, Int.sub_zero, Nat.cast_mul] at h
Proof state after:
case refine_2
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : ↑((f 0).natAbs * (4 * K.factorial)) * ↑k ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_2
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : ↑((f 0).natAbs * (4 * K.factorial)) * ↑k ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Tactic:
apply (dvd_mul_right _ _).trans at h
Proof state after:
case refine_2
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : ↑((f 0).natAbs * (4 * K.factorial)) ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_2
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : ↑((f 0).natAbs * (4 * K.factorial)) ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Tactic:
rw [Nat.cast_mul, ← abs_dvd, Int.natCast_natAbs,
  abs_mul, abs_abs, ← abs_mul, abs_dvd] at h
Proof state after:
case refine_2
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : f 0 * ↑(4 * K.factorial) ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_2
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : f 0 * ↑(4 * K.factorial) ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Tactic:
obtain ⟨m, h2⟩ := dvd_sub_self_right.mp (dvd_of_mul_right_dvd h)
Proof state after:
case refine_2.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : f 0 * ↑(4 * K.factorial) ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
m : ℤ
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_2.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
h : f 0 * ↑(4 * K.factorial) ∣ f ((f 0).natAbs * (4 * K.factorial) * k) - f 0
m : ℤ
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Tactic:
rw [h2, ← mul_sub_one, mul_dvd_mul_iff_left h1, Int.natCast_dvd] at h
Proof state after:
case refine_2.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_2.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
⊢ f ((f 0).natAbs * (4 * K.factorial) * k) = f 0
Tactic:
rw [h2, mul_right_eq_self₀, or_iff_left h1]
Proof state after:
case refine_2.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
⊢ m = 1
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_2.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
h1 : f 0 ≠ 0
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
⊢ m = 1
Tactic:
clear h1
Proof state after:
case refine_2.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
⊢ m = 1
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case refine_2.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
⊢ m = 1
Tactic:
by_cases h1 : m.natAbs = 1
Proof state after:
case pos
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
h1 : m.natAbs = 1
⊢ m = 1

case neg
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
h1 : ¬m.natAbs = 1
⊢ m = 1
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case pos
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
h1 : m.natAbs = 1
⊢ m = 1
Tactic:
rw [Int.natAbs_eq_iff, Nat.cast_one] at h1
Proof state after:
case pos
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
h1 : m = 1 ∨ m = -1
⊢ m = 1
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case pos
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
h1 : m = 1 ∨ m = -1
⊢ m = 1
Tactic:
exact h1.resolve_right λ h1 ↦ absurd ((dvd_mul_right _ _).trans (h1 ▸ h))
  (Nat.not_dvd_of_pos_of_lt (Nat.succ_pos 1) (Nat.le_succ 3))
Proof state after:
no goals
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case neg
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
h1 : ¬m.natAbs = 1
⊢ m = 1
Tactic:
apply Nat.exists_prime_and_dvd at h1
Proof state after:
case neg
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
h1 : ∃ p, p.Prime ∧ p ∣ m.natAbs
⊢ m = 1
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case neg
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
h1 : ∃ p, p.Prime ∧ p ∣ m.natAbs
⊢ m = 1
Tactic:
rcases h1 with ⟨p, h1, h3⟩
Proof state after:
case neg.intro.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
p : ℕ
h1 : p.Prime
h3 : p ∣ m.natAbs
⊢ m = 1
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case neg.intro.intro
f : ℕ → ℤ
K : ℕ
h0 : ∀ (p : ℕ), p.Prime → (∃ c, ↑p ∣ f c) → p < K
k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
p : ℕ
h1 : p.Prime
h3 : p ∣ m.natAbs
⊢ m = 1
Tactic:
specialize h0 p h1 ⟨(f 0).natAbs * (4 * Nat.factorial K) * k,
  h2 ▸ dvd_mul_of_dvd_right (Int.natCast_dvd.mpr h3) _⟩
Proof state after:
case neg.intro.intro
f : ℕ → ℤ
K k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
p : ℕ
h1 : p.Prime
h3 : p ∣ m.natAbs
h0 : p < K
⊢ m = 1
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case neg.intro.intro
f : ℕ → ℤ
K k : ℕ
m : ℤ
h : 4 * K.factorial ∣ (m - 1).natAbs
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
p : ℕ
h1 : p.Prime
h3 : p ∣ m.natAbs
h0 : p < K
⊢ m = 1
Tactic:
replace h := (Nat.dvd_factorial h1.pos h0.le).trans (dvd_of_mul_left_dvd h)
Proof state after:
case neg.intro.intro
f : ℕ → ℤ
K k : ℕ
m : ℤ
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
p : ℕ
h1 : p.Prime
h3 : p ∣ m.natAbs
h0 : p < K
h : p ∣ (m - 1).natAbs
⊢ m = 1
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case neg.intro.intro
f : ℕ → ℤ
K k : ℕ
m : ℤ
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
p : ℕ
h1 : p.Prime
h3 : p ∣ m.natAbs
h0 : p < K
h : p ∣ (m - 1).natAbs
⊢ m = 1
Tactic:
rw [← Int.natCast_dvd] at h h3
Proof state after:
case neg.intro.intro
f : ℕ → ℤ
K k : ℕ
m : ℤ
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
p : ℕ
h1 : p.Prime
h3 : ↑p ∣ m
h0 : p < K
h : ↑p ∣ m - 1
⊢ m = 1
Theorem: IMOSL.IMO2009N3.const_of_finite_prime_divisor
Proof state before:
case neg.intro.intro
f : ℕ → ℤ
K k : ℕ
m : ℤ
h2 : f ((f 0).natAbs * (4 * K.factorial) * k) = f 0 * m
p : ℕ
h1 : p.Prime
h3 : ↑p ∣ m
h0 : p < K
h : ↑p ∣ m - 1
⊢ m = 1
Tactic:
exact absurd (Int.natCast_dvd.mp <|
  (Int.dvd_iff_dvd_of_dvd_sub h).mp h3) h1.not_dvd_one
Proof state after:
no goals
Theorem: IMOSL.IMO2009N3.final_solution
Proof state before:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0 : ∀ (C : ℤ), ∃ b, f b ≠ C
K : ℕ
⊢ ∃ p, K ≤ p ∧ p.Prime ∧ ∃ c, ↑p ∣ f c
Tactic:
refine by_contra λ h1 ↦ absurd h0 (not_forall.mpr ⟨f 0, ?_⟩)
Proof state after:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0 : ∀ (C : ℤ), ∃ b, f b ≠ C
K : ℕ
h1 : ¬∃ p, K ≤ p ∧ p.Prime ∧ ∃ c, ↑p ∣ f c
⊢ ¬∃ b, f b ≠ f 0
Theorem: IMOSL.IMO2009N3.final_solution
Proof state before:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0 : ∀ (C : ℤ), ∃ b, f b ≠ C
K : ℕ
h1 : ¬∃ p, K ≤ p ∧ p.Prime ∧ ∃ c, ↑p ∣ f c
⊢ ¬∃ b, f b ≠ f 0
Tactic:
rw [← not_forall, not_not]
Proof state after:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0 : ∀ (C : ℤ), ∃ b, f b ≠ C
K : ℕ
h1 : ¬∃ p, K ≤ p ∧ p.Prime ∧ ∃ c, ↑p ∣ f c
⊢ ∀ (x : ℕ), f x = f 0
Theorem: IMOSL.IMO2009N3.final_solution
Proof state before:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0 : ∀ (C : ℤ), ∃ b, f b ≠ C
K : ℕ
h1 : ¬∃ p, K ≤ p ∧ p.Prime ∧ ∃ c, ↑p ∣ f c
⊢ ∀ (x : ℕ), f x = f 0
Tactic:
suffices ∃ C, f = λ _ ↦ C from this.elim λ C this ↦ this ▸ λ x ↦ rfl
Proof state after:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0 : ∀ (C : ℤ), ∃ b, f b ≠ C
K : ℕ
h1 : ¬∃ p, K ≤ p ∧ p.Prime ∧ ∃ c, ↑p ∣ f c
⊢ ∃ C, f = fun x => C
Theorem: IMOSL.IMO2009N3.final_solution
Proof state before:
f : ℕ → ℤ
h : ∀ (a b : ℕ), ↑a - ↑b ∣ f a - f b
h0 : ∀ (C : ℤ), ∃ b, f b ≠ C
K : ℕ
h1 : ¬∃ p, K ≤ p ∧ p.Prime ∧ ∃ c, ↑p ∣ f c
⊢ ∃ C, f = fun x => C
Tactic:
exact const_of_finite_prime_divisor h (K := K)
  λ p h2 h3 ↦ lt_of_not_le λ h4 ↦ not_exists.mp h1 p ⟨h4, h2, h3⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2015N1.main_claim
Proof state before:
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
⊢ 2 * (2 * c) ∣ m - 3
Tactic:
by_cases h1 : c = 0
Proof state after:
case pos
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
h1 : c = 0
⊢ 2 * (2 * c) ∣ m - 3

case neg
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
⊢ 2 * (2 * c) ∣ m - 3
Theorem: IMOSL.IMO2015N1.main_claim
Proof state before:
case pos
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
h1 : c = 0
⊢ 2 * (2 * c) ∣ m - 3
Tactic:
rwa [h1, mul_zero, ← h1]
Proof state after:
no goals
Theorem: IMOSL.IMO2015N1.main_claim
Proof state before:
case neg
c m : ℤ
h : 2 * c ∣ m - 3
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
⊢ 2 * (2 * c) ∣ m - 3
Tactic:
rcases h with ⟨d, h⟩
Proof state after:
case neg.intro
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 * (2 * c) ∣ m - 3
Theorem: IMOSL.IMO2015N1.main_claim
Proof state before:
case neg.intro
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 * (2 * c) ∣ m - 3
Tactic:
rw [h, mul_comm]
Proof state after:
case neg.intro
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 * c * 2 ∣ 2 * c * d
Theorem: IMOSL.IMO2015N1.main_claim
Proof state before:
case neg.intro
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 * c * 2 ∣ 2 * c * d
Tactic:
apply mul_dvd_mul_left
Proof state after:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 ∣ d
Theorem: IMOSL.IMO2015N1.main_claim
Proof state before:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
⊢ 2 ∣ d
Tactic:
have X : (2 : ℤ) ≠ 0 := two_ne_zero
Proof state after:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
X : 2 ≠ 0
⊢ 2 ∣ d
Theorem: IMOSL.IMO2015N1.main_claim
Proof state before:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
X : 2 ≠ 0
⊢ 2 ∣ d
Tactic:
have X0 : (3 / 2 : ℤ) = 1 := rfl
Proof state after:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
X : 2 ≠ 0
X0 : 3 / 2 = 1
⊢ 2 ∣ d
Theorem: IMOSL.IMO2015N1.main_claim
Proof state before:
case neg.intro.h
c m : ℤ
h0 : 2 * c ∣ f m - 3
h1 : ¬c = 0
d : ℤ
h : m - 3 = 2 * c * d
X : 2 ≠ 0
X0 : 3 / 2 = 1
⊢ 2 ∣ d
Tactic:
rw [f, eq_add_of_sub_eq h, add_mul, add_sub_assoc, mul_assoc, ← mul_sub_one,
  dvd_add_right ⟨_, rfl⟩, mul_assoc, add_comm, Int.add_mul_ediv_left _ _ X,
  X0, add_sub_cancel_left, ← two_add_one_eq_three, add_one_mul (α := ℤ),
  ← mul_assoc, dvd_add_right ⟨_, rfl⟩, mul_comm] at h0
Proof state after:
case neg.intro.h
c m : ℤ
h1 : ¬c = 0
d : ℤ
h0 : c * 2 ∣ c * d
h : m - 3 = 2 * c * d
X : 2 ≠ 0
X0 : 3 / 2 = 1
⊢ 2 ∣ d
Theorem: IMOSL.IMO2015N1.main_claim
Proof state before:
case neg.intro.h
c m : ℤ
h1 : ¬c = 0
d : ℤ
h0 : c * 2 ∣ c * d
h : m - 3 = 2 * c * d
X : 2 ≠ 0
X0 : 3 / 2 = 1
⊢ 2 ∣ d
Tactic:
exact Int.dvd_of_mul_dvd_mul_left h1 h0
Proof state after:
no goals
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
M : ℤ
⊢ (∃ k, 2 ∣ f^[k] M) ↔ M ≠ 3
Tactic:
rw [iff_not_comm, not_exists]
Proof state after:
M : ℤ
⊢ M = 3 ↔ ∀ (x : ℕ), ¬2 ∣ f^[x] M
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
M : ℤ
⊢ M = 3 ↔ ∀ (x : ℕ), ¬2 ∣ f^[x] M
Tactic:
refine ⟨λ h n ↦ ?_, λ h ↦ ?_⟩
Proof state after:
case refine_1
M : ℤ
h : M = 3
n : ℕ
⊢ ¬2 ∣ f^[n] M

case refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
⊢ M = 3
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
⊢ M = 3
Tactic:
suffices h0 : ∀ n k, 2 ^ (n + 1) ∣ f^[k] M - 3 by
  let K := (M - 3).natAbs
  refine eq_of_sub_eq_zero <| Int.eq_zero_of_abs_lt_dvd (h0 K 0) <| ?_
  rw [← Int.natCast_natAbs, ← Nat.cast_ofNat (n := 2), ← Int.natCast_pow]
  exact Int.ofNat_lt.mpr (K.lt_succ_self.trans K.succ.lt_two_pow)
Proof state after:
case refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
⊢ ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
⊢ ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
Tactic:
refine Nat.rec (λ k ↦ ?_) (λ n h0 k ↦ ?_)
Proof state after:
case refine_2.refine_1
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
k : ℕ
⊢ 2 ^ (Nat.zero + 1) ∣ f^[k] M - 3

case refine_2.refine_2
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
n : ℕ
h0 : ∀ (k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
k : ℕ
⊢ 2 ^ (n.succ + 1) ∣ f^[k] M - 3
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_1
M : ℤ
h : M = 3
n : ℕ
⊢ ¬2 ∣ f^[n] M
Tactic:
have h0 : f 3 = 3 := rfl
Proof state after:
case refine_1
M : ℤ
h : M = 3
n : ℕ
h0 : f 3 = 3
⊢ ¬2 ∣ f^[n] M
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_1
M : ℤ
h : M = 3
n : ℕ
h0 : f 3 = 3
⊢ ¬2 ∣ f^[n] M
Tactic:
rw [h, Function.iterate_fixed h0, ← two_add_one_eq_three]
Proof state after:
case refine_1
M : ℤ
h : M = 3
n : ℕ
h0 : f 3 = 3
⊢ ¬2 ∣ 2 + 1
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
case refine_1
M : ℤ
h : M = 3
n : ℕ
h0 : f 3 = 3
⊢ ¬2 ∣ 2 + 1
Tactic:
exact Int.two_not_dvd_two_mul_add_one 1
Proof state after:
no goals
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
⊢ M = 3
Tactic:
let K := (M - 3).natAbs
Proof state after:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ M = 3
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ M = 3
Tactic:
refine eq_of_sub_eq_zero <| Int.eq_zero_of_abs_lt_dvd (h0 K 0) <| ?_
Proof state after:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ |M - 3| < 2 ^ (K + 1)
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ |M - 3| < 2 ^ (K + 1)
Tactic:
rw [← Int.natCast_natAbs, ← Nat.cast_ofNat (n := 2), ← Int.natCast_pow]
Proof state after:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ ↑(M - 3).natAbs < ↑(OfNat.ofNat 2 ^ (K + 1))
Theorem: IMOSL.IMO2015N1.final_solution
Proof state before:
M : ℤ
h : ∀ (x : ℕ), ¬2 ∣ f^[x] M
h0 : ∀ (n k : ℕ), 2 ^ (n + 1) ∣ f^[k] M - 3
K : ℕ := (M - 3).natAbs
⊢ ↑(M - 3).natAbs < ↑(OfNat.ofNat 2 ^ (K + 1))
Tactic:
exact Int.ofNat_lt.mpr (K.lt_succ_self.trans K.succ.lt_two_pow)
Proof state after:
no goals