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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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