internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2017C1.final_solution
Proof state before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : latticeRect ((0, 0), m, n) = I.disjiUnion (latticeRect ∘ Q) h
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
apply_fun weight at h1
Proof state after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : weight (latticeRect ((0, 0), m, n)) = weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Theorem: IMOSL.IMO2017C1.final_solution
Proof state before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : weight (latticeRect ((0, 0), m, n)) = weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
rw [latticeRect_weight] at h1
Proof state after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 :
  (bif ((0, 0), m, n).2.1.bodd && ((0, 0), m, n).2.2.bodd then (-1) ^ (((0, 0), m, n).1.1 + ((0, 0), m, n).1.2)
    else 0) =
    weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Theorem: IMOSL.IMO2017C1.final_solution
Proof state before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 :
  (bif ((0, 0), m, n).2.1.bodd && ((0, 0), m, n).2.2.bodd then (-1) ^ (((0, 0), m, n).1.1 + ((0, 0), m, n).1.2)
    else 0) =
    weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
simp only at h1
Proof state after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif m.bodd && n.bodd then (-1) ^ (0 + 0) else 0) = weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Theorem: IMOSL.IMO2017C1.final_solution
Proof state before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif m.bodd && n.bodd then (-1) ^ (0 + 0) else 0) = weight (I.disjiUnion (latticeRect ∘ Q) h)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
rw [disjiUnion_weight_eq, Function.comp, h0.1, h0.2, add_zero] at h1
Proof state after:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Theorem: IMOSL.IMO2017C1.final_solution
Proof state before:
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ ∃ i ∈ I, 0 < weight (latticeRect (Q i))
Tactic:
apply exists_lt_of_sum_lt
Proof state after:
case Hlt
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ ∑ i ∈ I, 0 < ∑ i ∈ I, weight (latticeRect (Q i))
Theorem: IMOSL.IMO2017C1.final_solution
Proof state before:
case Hlt
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ ∑ i ∈ I, 0 < ∑ i ∈ I, weight (latticeRect (Q i))
Tactic:
rw [sum_const_zero, ← h1]
Proof state after:
case Hlt
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ 0 < bif true && true then (-1) ^ 0 else 0
Theorem: IMOSL.IMO2017C1.final_solution
Proof state before:
case Hlt
ι : Type u_1
Q : ι → (ℕ × ℕ) × ℕ × ℕ
m n : ℕ
I : Finset ι
h : (↑I).PairwiseDisjoint (latticeRect ∘ Q)
h0 : m.bodd = true ∧ n.bodd = true
h1 : (bif true && true then (-1) ^ 0 else 0) = ∑ i ∈ I, weight ((fun x => latticeRect (Q x)) i)
⊢ 0 < bif true && true then (-1) ^ 0 else 0
Tactic:
exact Int.zero_lt_one
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.dvd_sq_iff_dvd_sq_of_dvd_add
Proof state before:
a b c : ℕ
h : c ∣ a + b
⊢ c ∣ a ^ 2 ↔ c ∣ b ^ 2
Tactic:
have h0 {u v w : ℕ} (h0 : u ∣ v + w) : u ∣ v ^ 2 ↔ u ∣ v * w := by
  apply dvd_iff_of_dvd_add
  rw [sq, ← Nat.mul_add]
  exact h0.mul_left v
Proof state after:
a b c : ℕ
h : c ∣ a + b
h0 : ∀ {u v w : ℕ}, u ∣ v + w → (u ∣ v ^ 2 ↔ u ∣ v * w)
⊢ c ∣ a ^ 2 ↔ c ∣ b ^ 2
Theorem: IMOSL.IMO2019N4.dvd_sq_iff_dvd_sq_of_dvd_add
Proof state before:
a b c : ℕ
h : c ∣ a + b
h0 : ∀ {u v w : ℕ}, u ∣ v + w → (u ∣ v ^ 2 ↔ u ∣ v * w)
⊢ c ∣ a ^ 2 ↔ c ∣ b ^ 2
Tactic:
rw [h0 h, mul_comm, ← h0 (a.add_comm b ▸ h)]
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.dvd_sq_iff_dvd_sq_of_dvd_add
Proof state before:
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v ^ 2 ↔ u ∣ v * w
Tactic:
apply dvd_iff_of_dvd_add
Proof state after:
case h
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v ^ 2 + v * w
Theorem: IMOSL.IMO2019N4.dvd_sq_iff_dvd_sq_of_dvd_add
Proof state before:
case h
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v ^ 2 + v * w
Tactic:
rw [sq, ← Nat.mul_add]
Proof state after:
case h
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v * (v + w)
Theorem: IMOSL.IMO2019N4.dvd_sq_iff_dvd_sq_of_dvd_add
Proof state before:
case h
a b c : ℕ
h : c ∣ a + b
u v w : ℕ
h0 : u ∣ v + w
⊢ u ∣ v * (v + w)
Tactic:
exact h0.mul_left v
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq
Proof state before:
a p : ℕ
h : p.Prime
h0 : a < p
h1 : p + a ∣ p ^ 2
⊢ a = 0
Tactic:
rw [Nat.dvd_prime_pow h] at h1
Proof state after:
a p : ℕ
h : p.Prime
h0 : a < p
h1 : ∃ k ≤ 2, p + a = p ^ k
⊢ a = 0
Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq
Proof state before:
a p : ℕ
h : p.Prime
h0 : a < p
h1 : ∃ k ≤ 2, p + a = p ^ k
⊢ a = 0
Tactic:
rcases h1 with ⟨k, h1, h2⟩
Proof state after:
case intro.intro
a p : ℕ
h : p.Prime
h0 : a < p
k : ℕ
h1 : k ≤ 2
h2 : p + a = p ^ k
⊢ a = 0
Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq
Proof state before:
case intro.intro
a p : ℕ
h : p.Prime
h0 : a < p
k : ℕ
h1 : k ≤ 2
h2 : p + a = p ^ k
⊢ a = 0
Tactic:
rw [Nat.le_add_one_iff, Nat.le_add_one_iff, zero_add, le_zero_iff] at h1
Proof state after:
case intro.intro
a p : ℕ
h : p.Prime
h0 : a < p
k : ℕ
h1 : (k = 0 ∨ k = 1) ∨ k = 1 + 1
h2 : p + a = p ^ k
⊢ a = 0
Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq
Proof state before:
case intro.intro
a p : ℕ
h : p.Prime
h0 : a < p
k : ℕ
h1 : (k = 0 ∨ k = 1) ∨ k = 1 + 1
h2 : p + a = p ^ k
⊢ a = 0
Tactic:
rcases h1 with (rfl | rfl) | rfl
Proof state after:
case intro.intro.inl.inl
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ 0
⊢ a = 0

case intro.intro.inl.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ 1
⊢ a = 0

case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ a = 0
Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq
Proof state before:
case intro.intro.inl.inl
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ 0
⊢ a = 0
Tactic:
exact absurd h2 (h.one_lt.trans_le le_self_add).ne.symm
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq
Proof state before:
case intro.intro.inl.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ 1
⊢ a = 0
Tactic:
rwa [pow_one, add_right_eq_self] at h2
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq
Proof state before:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ a = 0
Tactic:
refine absurd ((add_lt_add_left h0 p).trans_le ?_) h2.not_lt
Proof state after:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ p + p ≤ p ^ (1 + 1)
Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq
Proof state before:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ p + p ≤ p ^ (1 + 1)
Tactic:
rw [sq, ← two_mul]
Proof state after:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ 2 * p ≤ p * p
Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq
Proof state before:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ 2 * p ≤ p * p
Tactic:
exact Nat.mul_le_mul_right p h.two_le
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.linear_is_good
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, Nat.mul_assoc, mul_left_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
⊢ ∃ k, f = fun x => k * x
Tactic:
have h0 {n} (h0 : C < n) : f n ≤ n * f 1 := by
  rw [← Nat.succ_le_succ_iff, Nat.succ_eq_one_add, Nat.succ_eq_one_add]
  exact Nat.le_of_dvd (Nat.add_pos_left Nat.one_pos _)
    (h 1 n <| Nat.lt_one_add_iff.mpr h0.le)
Proof state after:
C : ℕ
f : ℕ → ℕ
h : good C f
h0 : ∀ {n : ℕ}, C < n → f n ≤ n * f 1
⊢ ∃ k, f = fun 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
⊢ ∃ k, f = fun x => k * x
Tactic:
have h1 {p} (h1 : C < p) (h2 : p.Prime) : ∃ k ≤ f 1, f p = k * p := by
  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)⟩
  rcases exists_gt (C + f p) with ⟨n, h3⟩
  replace h3 := Nat.exists_eq_add_of_le <|
    h3.le.trans (Nat.le_mul_of_pos_right _ h2.pos)
  rcases h3 with ⟨a, h3⟩; rw [add_right_comm] at h3
  specialize h (C + a) p <|
    (C.le_add_right a).trans_lt (Nat.lt_add_of_pos_right h2.pos)
  replace h3 : p ∣ C + a + f p := ⟨n, h3.symm.trans (n.mul_comm p)⟩
  rw [← dvd_sq_iff_dvd_sq_of_dvd_add h3, dvd_iff_of_dvd_add (h3.trans h)]
  exact p.dvd_mul_right _
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
⊢ ∃ k, f = fun 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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
⊢ ∃ k, f = fun x => k * x
Tactic:
rcases C.succ.exists_infinite_primes with ⟨p, (h3 : C < p), h4⟩
Proof state after:
case 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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
⊢ ∃ k, f = fun x => k * x
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
h1 : ∀ {p : ℕ}, C < p → p.Prime → ∃ k ≤ f 1, f p = k * p
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
⊢ ∃ k, f = fun x => k * x
Tactic:
rcases h1 h3 h4 with ⟨k, -, h5⟩
Proof state after:
case 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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
⊢ ∃ k, f = fun x => k * x
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case 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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
⊢ ∃ k, f = fun x => k * x
Tactic:
refine ⟨k, funext λ n ↦ ?_⟩
Proof state after:
case 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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n : ℕ
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case 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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n : ℕ
⊢ f n = k * n
Tactic:
rcases h2 p with ⟨Bp, hp⟩
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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
⊢ f n = k * n
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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
⊢ f n = k * n
Tactic:
rcases h2 n with ⟨Bn, hn⟩
Proof state after:
case intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
⊢ f n = k * n
Tactic:
rcases (max Bp Bn).succ.exists_infinite_primes with ⟨q, h6, h7⟩
Proof state after:
case intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : (max Bp Bn).succ ≤ q
h7 : q.Prime
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : (max Bp Bn).succ ≤ q
h7 : q.Prime
⊢ f n = k * n
Tactic:
rw [Nat.succ_le_iff, max_lt_iff] at h6
Proof state after:
case intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp : ℕ
hp : ∀ (p_1 : ℕ), p_1.Prime → Bp < p_1 → ∃ k, f p_1 = k * p_1 ∧ f p = k * p
Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
⊢ f n = k * n
Tactic:
specialize hp q h7 h6.1
Proof state after:
case intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
hp : ∃ k, f q = k * q ∧ f p = k * p
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
hp : ∃ k, f q = k * q ∧ f p = k * p
⊢ f n = k * n
Tactic:
rcases hp with ⟨kp, h8, h9⟩
Proof state after:
case intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : f p = kp * p
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : f p = kp * p
⊢ f n = k * n
Tactic:
rw [h5, Nat.mul_left_inj h4.ne_zero] at h9
Proof state after:
case intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn : ℕ
hn : ∀ (p : ℕ), p.Prime → Bn < p → ∃ k, f p = k * p ∧ f n = k * n
q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
⊢ f n = k * n
Tactic:
specialize hn q h7 h6.2
Proof state after:
case intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
hn : ∃ k, f q = k * q ∧ f n = k * n
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
hn : ∃ k, f q = k * q ∧ f n = k * n
⊢ f n = k * n
Tactic:
rcases hn with ⟨kn, h10, h11⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
kn : ℕ
h10 : f q = kn * q
h11 : f n = kn * n
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
kn : ℕ
h10 : f q = kn * q
h11 : f n = kn * n
⊢ f n = k * n
Tactic:
rw [h8, Nat.mul_left_inj h7.ne_zero] at h10
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
kn : ℕ
h10 : kp = kn
h11 : f n = kn * n
⊢ f n = k * n
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.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
h2 : ∀ (x : ℕ), ∃ B, ∀ (p : ℕ), p.Prime → B < p → ∃ k, f p = k * p ∧ f x = k * x
p : ℕ
h3 : C < p
h4 : p.Prime
k : ℕ
h5 : f p = k * p
n Bp Bn q : ℕ
h6 : Bp < q ∧ Bn < q
h7 : q.Prime
kp : ℕ
h8 : f q = kp * q
h9 : k = kp
kn : ℕ
h10 : kp = kn
h11 : f n = kn * n
⊢ f n = k * n
Tactic:
rw [h11, ← h10, ← h9]
Proof state after:
no goals
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
n : ℕ
h0 : C < n
⊢ f n ≤ n * f 1
Tactic:
rw [← Nat.succ_le_succ_iff, Nat.succ_eq_one_add, Nat.succ_eq_one_add]
Proof state after:
C : ℕ
f : ℕ → ℕ
h : good C f
n : ℕ
h0 : C < n
⊢ 1 + f n ≤ 1 + n * f 1
Theorem: IMOSL.IMO2019N4.good_is_linear
Proof state before:
C : ℕ
f : ℕ → ℕ
h : good C f
n : ℕ
h0 : C < n
⊢ 1 + f n ≤ 1 + n * f 1
Tactic:
exact Nat.le_of_dvd (Nat.add_pos_left Nat.one_pos _)
  (h 1 n <| Nat.lt_one_add_iff.mpr h0.le)
Proof state after:
no goals