internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
⊢ ∃ k ≤ f 1, f p = k * p
Tactic:
suffices p ∣ f p ^ 2 by
  rcases h2.dvd_of_dvd_pow this with ⟨k, h3⟩
  exact ⟨k, Nat.le_of_mul_le_mul_left (h3.ge.trans (h0 h1)) h2.pos,
    h3.trans (p.mul_comm k)⟩
Proof state after:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
⊢ p ∣ f p ^ 2
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
⊢ p ∣ f p ^ 2
Tactic:
rcases exists_gt (C + f p) with ⟨n, h3⟩
Proof state after:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n : ℕ
h3 : C + f p < n
⊢ p ∣ f p ^ 2
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n : ℕ
h3 : C + f p < n
⊢ p ∣ f p ^ 2
Tactic:
replace h3 := Nat.exists_eq_add_of_le <|
  h3.le.trans (Nat.le_mul_of_pos_right _ h2.pos)
Proof state after:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n : ℕ
h3 : ∃ k, n * p = C + f p + k
⊢ p ∣ f p ^ 2
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n : ℕ
h3 : ∃ k, n * p = C + f p + k
⊢ p ∣ f p ^ 2
Tactic:
rcases h3 with ⟨a, h3⟩
Proof state after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + f p + a
⊢ p ∣ f p ^ 2
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + f p + a
⊢ p ∣ f p ^ 2
Tactic:
rw [add_right_comm] at h3
Proof state after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + a + f p
⊢ p ∣ f p ^ 2
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + a + f p
⊢ p ∣ f p ^ 2
Tactic:
specialize h (C + a) p <|
  (C.le_add_right a).trans_lt (Nat.lt_add_of_pos_right h2.pos)
Proof state after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + a + f p
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
⊢ p ∣ f p ^ 2
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h3 : n * p = C + a + f p
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
⊢ p ∣ f p ^ 2
Tactic:
replace h3 : p ∣ C + a + f p := ⟨n, h3.symm.trans (n.mul_comm p)⟩
Proof state after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
h3 : p ∣ C + a + f p
⊢ p ∣ f p ^ 2
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
h3 : p ∣ C + a + f p
⊢ p ∣ f p ^ 2
Tactic:
rw [← dvd_sq_iff_dvd_sq_of_dvd_add h3, dvd_iff_of_dvd_add (h3.trans h)]
Proof state after:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
h3 : p ∣ C + a + f p
⊢ p ∣ p * f (C + a)
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
n a : ℕ
h : C + a + f p ∣ (C + a) ^ 2 + p * f (C + a)
h3 : p ∣ C + a + f p
⊢ p ∣ p * f (C + a)
Tactic:
exact p.dvd_mul_right _
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
this : p ∣ f p ^ 2
⊢ ∃ k ≤ f 1, f p = k * p
Tactic:
rcases h2.dvd_of_dvd_pow this with ⟨k, h3⟩
Proof state after:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
this : p ∣ f p ^ 2
k : ℕ
h3 : f p = p * k
⊢ ∃ k ≤ f 1, f p = k * p
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
p : ℕ
h1 : C < p
h2 : p.Prime
this : p ∣ f p ^ 2
k : ℕ
h3 : f p = p * k
⊢ ∃ k ≤ f 1, f p = k * p
Tactic:
exact ⟨k, Nat.le_of_mul_le_mul_left (h3.ge.trans (h0 h1)) h2.pos,
  h3.trans (p.mul_comm k)⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x : ℕ
⊢ ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
Tactic:
refine ⟨max C (max (f x) (max (x * f 1) (x ^ 2))), λ p h2 h3 ↦ ?_⟩
Proof state after:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
h3 : max C (max (f x) (max (x * f 1) (x ^ 2))) < p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
h3 : max C (max (f x) (max (x * f 1) (x ^ 2))) < p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Tactic:
rw [max_lt_iff, max_lt_iff, max_lt_iff] at h3
Proof state after:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
h3 : C < p ∧ f x < p ∧ x * f 1 < p ∧ x ^ 2 < p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
h3 : C < p ∧ f x < p ∧ x * f 1 < p ∧ x ^ 2 < p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Tactic:
rcases h3 with ⟨hp1, hp2, hp3, hp4⟩
Proof state after:
case intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Tactic:
rcases h1 hp1 h2 with ⟨k, h3, h4⟩
Proof state after:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
⊢ ∃ k, f p = k * p ∧ f x = k * x
Tactic:
refine ⟨k, h4, ?_⟩
Proof state after:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
⊢ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
⊢ f x = k * x
Tactic:
rcases (f x).eq_zero_or_pos with h5 | h5
Proof state after:
case intro.intro.intro.intro.intro.inl
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
⊢ f x = k * x

case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
⊢ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inl
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
⊢ f x = k * x
Tactic:
rcases k.eq_zero_or_pos with rfl | h6
Proof state after:
case intro.intro.intro.intro.intro.inl.inl
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
h5 : f x = 0
h3 : 0 ≤ f 1
h4 : f p = 0 * p
⊢ f x = 0 * x

case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
⊢ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inl.inl
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
h5 : f x = 0
h3 : 0 ≤ f 1
h4 : f p = 0 * p
⊢ f x = 0 * x
Tactic:
rw [h5, zero_mul]
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
⊢ f x = k * x
Tactic:
suffices x ^ 2 = 0 by rw [h5, pow_eq_zero this, mul_zero]
Proof state after:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
⊢ x ^ 2 = 0
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
⊢ x ^ 2 = 0
Tactic:
specialize h x p (Nat.lt_add_left x hp1)
Proof state after:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
h : x + f p ∣ x ^ 2 + p * f x
⊢ x ^ 2 = 0
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
h : x + f p ∣ x ^ 2 + p * f x
⊢ x ^ 2 = 0
Tactic:
rw [h5, mul_zero, add_zero, h4] at h
Proof state after:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
h : x + k * p ∣ x ^ 2
⊢ x ^ 2 = 0
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inl.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
h : x + k * p ∣ x ^ 2
⊢ x ^ 2 = 0
Tactic:
exact Nat.eq_zero_of_dvd_of_lt h <|
  Nat.lt_add_left x (lt_mul_of_one_le_of_lt h6 hp4)
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x = 0
h6 : k > 0
this : x ^ 2 = 0
⊢ f x = k * x
Tactic:
rw [h5, pow_eq_zero this, mul_zero]
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
⊢ f x = k * x
Tactic:
specialize h p x (Nat.lt_add_right x hp1)
Proof state after:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ f x = k * x
Tactic:
have h6 : (p + f x).Coprime p := by
  rw [Nat.coprime_self_add_left, Nat.coprime_comm, h2.coprime_iff_not_dvd]
  exact Nat.not_dvd_of_pos_of_lt h5 hp2
Proof state after:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
h6 : (p + f x).Coprime p
⊢ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
h6 : (p + f x).Coprime p
⊢ f x = k * x
Tactic:
rw [sq, h4, ← mul_assoc, ← add_mul, h6.dvd_mul_right] at h
Proof state after:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p + x * k
h6 : (p + f x).Coprime p
⊢ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p + x * k
h6 : (p + f x).Coprime p
⊢ f x = k * x
Tactic:
clear h6
Proof state after:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p + x * k
⊢ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p + x * k
⊢ f x = k * x
Tactic:
rcases h with ⟨_ | _ | t, h⟩
Proof state after:
case intro.intro.intro.intro.intro.inr.intro.zero
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + x * k = (p + f x) * 0
⊢ f x = k * x

case intro.intro.intro.intro.intro.inr.intro.succ.zero
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + x * k = (p + f x) * (0 + 1)
⊢ f x = k * x

case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * (t + 1 + 1)
⊢ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ (p + f x).Coprime p
Tactic:
rw [Nat.coprime_self_add_left, Nat.coprime_comm, h2.coprime_iff_not_dvd]
Proof state after:
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ ¬p ∣ f x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + f x ∣ p ^ 2 + x * f p
⊢ ¬p ∣ f x
Tactic:
exact Nat.not_dvd_of_pos_of_lt h5 hp2
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.zero
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + x * k = (p + f x) * 0
⊢ f x = k * x
Tactic:
exact h.not_gt.elim (Nat.lt_add_right _ h2.pos)
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.succ.zero
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
h : p + x * k = (p + f x) * (0 + 1)
⊢ f x = k * x
Tactic:
rwa [Nat.mul_one, add_right_inj, eq_comm, mul_comm] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * (t + 1 + 1)
⊢ f x = k * x
Tactic:
rw [add_assoc, mul_add, add_mul _ _ 2] at h
Proof state after:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ f x = k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ f x = k * x
Tactic:
refine h.not_lt.elim (Nat.lt_add_left _ (Nat.lt_add_right _ ?_))
Proof state after:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ p + x * k < p * 2
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ p + x * k < p * 2
Tactic:
rw [mul_two, add_lt_add_iff_left]
Proof state after:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ x * k < p
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.inr.intro.succ.succ
C : ℕ
f : ℕ → ℕ
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
x p : ℕ
h2 : p.Prime
hp1 : C < p
hp2 : f x < p
hp3 : x * f 1 < p
hp4 : x ^ 2 < p
k : ℕ
h3 : k ≤ f 1
h4 : f p = k * p
h5 : f x > 0
t : ℕ
h : p + x * k = (p + f x) * t + (p * 2 + f x * 2)
⊢ x * k < p
Tactic:
exact hp3.trans_le' (Nat.mul_le_mul_left x h3)
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.linear_is_goodPNat
Proof state before:
C k a b : ℕ+
x✝ : C < a + b
⊢ a ^ 2 + b * (fun x => k * x) a = (a + (fun x => k * x) b) * a
Tactic:
rw [sq, add_mul, mul_assoc, mul_left_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.goodPNat_is_linear
Proof state before:
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
⊢ ∃ k, f = fun x => k * x
Tactic:
let g : ℕ → ℕ := λ n ↦ dite (0 < n) (λ h ↦ f ⟨n, h⟩) (λ _ ↦ 0)
Proof state after:
C : ℕ+
f : ℕ+ → ℕ+
h : goodPNat C f
g : ℕ → ℕ := fun n => if h : 0 < n then ↑(f ⟨n, h⟩) else 0
⊢ ∃ k, f = fun x => k * x