Theorem: IMOSL.IMO2009N3.final_solution (IMOSLLean4/IMO2009/N3/N3.lean)

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, ?_⟩)
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

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]
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

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
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

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⟩
State after:
no goals